[GHC] #9017: Confusing error message with PolyKinds
#9017: Confusing error message with PolyKinds ------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Consider the following example code: {{{ import Control.Arrow foo :: a b (m b) foo = arr return }}} if we typecheck this we rightly get two errors about missing instances (Arrow a, Monad m). However, if we enable `PolyKinds` we get the following error message: {{{ T.hs:4:7: Kind incompatibility when matching types: a0 :: * -> * -> * a :: k1 -> k -> * Expected type: a b (m b) Actual type: a0 b0 (m0 b0) Relevant bindings include foo :: a b (m b) (bound at T.hs:4:1) In the expression: arr return In an equation for ‘foo’: foo = arr return }}} I can ''sort of'' see where this is coming from if I think really hard :), so perhaps it's not a bug per se, but it's definitely confusing; and it's a pity that a type error (forgotten type qualifier) is reported as a kind error. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9017> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9017: Confusing error message with PolyKinds -------------------------------------+------------------------------------ Reporter: edsko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): I agree that this is bad. We really want more information about what goes wrong with the kind equality. At the moment, when we get a kind-incompatible type equality, such as `a:k ~ b:*`, we generate a "derived" kind equality `k ~ *`. In this case `k` is a skolem constant, so the constraint is insoluble. But derived constraints are discarded before error message generation (for good reason) so we only see the type-equality problem. We could instead generate a "wanted" kind equality; that would not be discarded, and we'd get a better error message: {{{ T9017.hs:8:7: Couldn't match kind `k1' with `*' `k1' is a rigid type variable bound by the type signature for foo :: a b (m b) at T9017.hs:7:8 When matching types a0 :: * -> * -> * a :: k1 -> k -> * Expected type: a b (m b) Actual type: a0 b0 (m0 b0) Relevant bindings include foo :: a b (m b) (bound at T9017.hs:8:1) In the expression: arr return In an equation for `foo': foo = arr return }}} Could still do with improvement (the foralls in the "bound by" message are invisible), but better. Sadly, a new wanted constraint should be used to solve the constraint that gave rise to it, otherwise we generate the same wanted constraint many times. And that is what happens here: we get two copies of the same error messages. With some faff we could elimate the dup, but I think it'd better to wait for Richard's upcoming work in which he gives us full-on kind equalities. Now we can use the kind equality to solve the type equality and all will be well. Meanwhile I attach my diff. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9017#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9017: Confusing error message with PolyKinds -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by thomie): * cc: goldfire (added) * component: Compiler => Compiler (Type checker) Comment:
I think it'd better to wait for Richard's upcoming work in which he gives us full-on kind equalities. Now we can use the kind equality to solve the type equality and all will be well.
-- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9017#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9017: Confusing error message with PolyKinds -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): -------------------------------------+------------------------------------- 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/9017#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9017: Confusing error message with PolyKinds -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T9017 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => polykinds/T9017 * status: new => closed * resolution: => fixed Comment: This test case still produces a suboptimal message: {{{ T9017.hs:8:7: error: • Couldn't match kind ‘k’ with ‘*’ ‘k’ is a rigid type variable bound by the type signature for: foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k). a b (m b) at T9017.hs:7:8 When matching the kind of ‘a’ • In the expression: arr return In an equation for ‘foo’: foo = arr return • Relevant bindings include foo :: a b (m b) (bound at T9017.hs:8:1) T9017.hs:8:7: error: • Couldn't match kind ‘k1’ with ‘*’ ‘k1’ is a rigid type variable bound by the type signature for: foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k). a b (m b) at T9017.hs:7:8 When matching the kind of ‘a’ • In the expression: arr return In an equation for ‘foo’: foo = arr return • Relevant bindings include foo :: a b (m b) (bound at T9017.hs:8:1) }}} We get two duplicate messages, and it's still quite hard to see what's going on. Actually, a little more thought tells me the messages aren't quite duplicates: the kind-generalized type signature contains two different kind variables, both of which are distinct from `*`. With the type signature given, I think it's OK. I'm going to accept this output, but shout if you see a way to improve. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9017#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9017: Confusing error message with PolyKinds -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T9017 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <eir@…>): In [changeset:"779dfea1d9cc713d9b1e26bb559e8da309b2aeec/ghc" 779dfea1/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="779dfea1d9cc713d9b1e26bb559e8da309b2aeec" Test #9017 in polykinds/T9017 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9017#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC