[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 <eir@…>): In [changeset:"6746549772c5cc0ac66c0fce562f297f4d4b80a2/ghc" 67465497/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6746549772c5cc0ac66c0fce562f297f4d4b80a2" Add kind equalities to GHC. This implements the ideas originally put forward in "System FC with Explicit Kind Equality" (ICFP'13). There are several noteworthy changes with this patch: * We now have casts in types. These change the kind of a type. See new constructor `CastTy`. * All types and all constructors can be promoted. This includes GADT constructors. GADT pattern matches take place in type family equations. In Core, types can now be applied to coercions via the `CoercionTy` constructor. * Coercions can now be heterogeneous, relating types of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2` proves both that `t1` and `t2` are the same and also that `k1` and `k2` are the same. * The `Coercion` type has been significantly enhanced. The documentation in `docs/core-spec/core-spec.pdf` reflects the new reality. * The type of `*` is now `*`. No more `BOX`. * Users can write explicit kind variables in their code, anywhere they can write type variables. For backward compatibility, automatic inference of kind-variable binding is still permitted. * The new extension `TypeInType` turns on the new user-facing features. * Type families and synonyms are now promoted to kinds. This causes trouble with parsing `*`, leading to the somewhat awkward new `HsAppsTy` constructor for `HsType`. This is dispatched with in the renamer, where the kind `*` can be told apart from a type-level multiplication operator. Without `-XTypeInType` the old behavior persists. With `-XTypeInType`, you need to import `Data.Kind` to get `*`, also known as `Type`. * The kind-checking algorithms in TcHsType have been significantly rewritten to allow for enhanced kinds. * The new features are still quite experimental and may be in flux. * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203. * TODO: Update user manual. Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142. Updates Haddock submodule. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11197#comment:2> 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: | -------------------------------------+------------------------------------- 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 <ben@…>): In [changeset:"aa611746aa860e1884c9ad623d6939791f2645ff/ghc" aa61174/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="aa611746aa860e1884c9ad623d6939791f2645ff" users-guide: Add references to various issues in bugs section Test Plan: Read it Reviewers: austin Reviewed By: austin Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D2052 GHC Trac Issues: #7411, #11197, #11554, #11715 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11197#comment:6> 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: | -------------------------------------+------------------------------------- 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