#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 (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 ): 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: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): 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