[GHC] #11197: Overeager deferred type errors
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.11 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- With `TypeInType`, the solver now works in terms of unlifted equality. The only place this matters is in deferred type errors, which now are more eager than they were before. For example: {{{ {-# OPTIONS_GHC -fdefer-type-errors #-} module Main where main = do putStrLn "Hi there." putStrLn True }}} This used to print {{{ Hi there. Defer: Defer.hs:7:12: error: ... }}} Now it prints {{{ Defer: Defer.hs:7:12: error: ... }}} No more `Hi there.`. Thinking about Core, this change should be expected. GHC puts all evidence bindings for `main` at the top, and with unlifted equality in the solver, these bindings now contain `case typeError ... of ...`, which forces the type error eagerly. Previously, there was a lazy binding for a lifted equality witness, unpacked only at the last moment by magic in the desugarer, thus the lazier warning. Simon has proposed customizing the !FloatIn pass to deal with this scenario. I do believe this would work nicely, but I have not yet implemented it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This regression affects test cases `Defer02` and `T7861`. I'm less concerned about the latter, as it requires `ImpredicativeTypes`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone: 8.0.1
Component: Compiler | Version: 7.11
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.11 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.11 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): See also #2988, which discusses other improvements to floating-in. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone: 8.0.1
Component: Compiler (Type | Version: 7.11
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thoughtpolice): * milestone: 8.0.1 => 8.0.2 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): It looks like this is already affecting users: https://github.com/CRogers /should-not-typecheck/pull/6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The commentary on the PR linked to in comment:8 contains a workaround in that case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.0.2 => 8.2.1 Comment: This won't happen for 8.0.2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by sighingnow): When `-fdefer-type-errors` is enabled, the program {{{#!hs main = do putStrLn "Hi there." putStrLn 1 }}} works well. However the program {{{#!hs main = do putStrLn "Hi there." putStrLn True }}} emits the deferred type error message eagerly and doesn't execute `putStrLn "Hi there."`. In the first case, the type error is `EvVarDest evar`: {{{ Wanted = WC {wc_simple = [WD] $dNum_a1zB {0}:: Num String (CDictCan(psc))} }}} However in the second case, the type error is `HoleDest hole`: {{{ Wanted = WC {wc_simple = [WD] hole{co_a1zO} {0}:: (Bool :: *) GHC.Prim.~# ([Char] :: *)} }}} Seems that the coercion hole is placed at wrong place. This ticket may related to Trac #14584. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here's what is happening. In the former case we get {{{ main = let { $dNum_a1d8 :: Num String [LclId] $dNum_a1d8 = Control.Exception.Base.typeError @ 'GHC.Types.LiftedRep @ (Num String) "blah blah blah } in let { $dMonad_axl :: Monad IO [LclId] $dMonad_axl = GHC.Base.$fMonadIO } in letrec { main_a1da :: IO () [LclId] main_a1da = >> @ IO $dMonad_axl @ () @ () (putStrLn (GHC.CString.unpackCString# "Hi there."#)) (putStrLn (fromInteger @ String $dNum_a1d8 1)); } in main_a1da }}} and the binding for `dNum_a1d8` can float inwards/be inlined. In the latter case we get {{{ main = case Control.Exception.Base.typeError @ ('GHC.Types.TupleRep '[]) @ ((Bool :: *) GHC.Prim.~# ([Char] :: *)) "blah blah blah" of co_a11b { __DEFAULT -> >> @ IO GHC.Base.$fMonadIO @ () @ () (putStrLn (GHC.CString.unpackCString# "Hi there."#)) (putStrLn (GHC.Types.True `cast` (Sub co_a11b :: (Bool :: *) ~R# ([Char] :: *)))) } }}} and the simplifier does not float in arbitrary case-expressions, for fear of changing error/termination behaviour. What do to? All I can think of is to make a special case for coercions, and be willing to float them in, on the grounds that evidence bindings are added by the compiler and should have as narrow scope as possible. Any objections? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | DeferredErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeInType => TypeInType, DeferredErrors -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | DeferredErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Does `-fdefer-type-errors` pull its weight as a compiler feature? The package mentioned above (`should-not-typecheck`) could arguably be improved by using GHCi instead. I think it makes sense to at least ''consider'' the alternative of ripping out the feature instead of jumping through hoops to fix it. It strikes me as complicated, intrusive, and (to my mind) not very useful. But it would be nice to hear whether people find it useful for writing programs or for teaching Haskell to beginners. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | DeferredErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | DeferredErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, I'd be very interested to know how useful people find `-fdefer-type- errors`. But in fact it's extraordinarily simple to implement, albeit with some wrinkles around the edges like this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | DeferredErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): #15624 is another example: {{{#!hs {-# OPTIONS_GHC -fdefer-type-errors #-} x = const True ('a' + 'a') y = const True (not 'a') }}} `x` is `True`, but `y` is `<<error>>`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11197: Overeager deferred type errors -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | DeferredErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
comment:14 All I can think of is to make a special case for coercions, and be willing to float them in, on the grounds that evidence bindings are added by the compiler and should have as narrow scope as possible.
This would be very easy to try, if anyone feels inclined. I could advise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11197#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC