#13742: Code using ConstraintKinds needs explicit kind signature with GHC 8.2.1 -------------------------------------+------------------------------------- Reporter: albertov | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.2.1-rc2 checker) | Keywords: Resolution: | ConstraintKinds, KindSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): So, the proximal cause of the error is that we're kind-checking A, B, C and D in one SCC where 8.0 wasn't previously, but one might imagine kind inference should still have come up with the correct kinds. We have a problem with the fact that `( A l, A l )` is overloaded: GHC doesn't know whether or not this is `Constraint -> Constraint -> Constraint`, or `* -> * -> *`. It decides the latter, and then you get a type error. Here's a relevant note from GHC source code: {{{ Note [Inferring tuple kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple, we try to figure out whether it's a tuple of kind * or Constraint. Step 1: look at the expected kind Step 2: infer argument kinds If after Step 2 it's not clear from the arguments that it's Constraint, then it must be *. Once having decided that we re-check the Check the arguments again to give good error messages in eg. `(Maybe, Maybe)` Note that we will still fail to infer the correct kind in this case: type T a = ((a,a), D a) type family D :: Constraint -> Constraint While kind checking T, we do not yet know the kind of D, so we will default the kind of T to * -> *. It works if we annotate `a` with kind `Constraint`. }}} This is a pretty similar situation. In the old world order, we first added a provisional kind for `D` to the environment before computing the kinds for type synonyms, which is why `A l` was correctly kinded. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13742#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler