#13742: Code using ConstraintKinds needs explicit kind signature with GHC 8.2.1 -------------------------------------+------------------------------------- Reporter: albertov | Owner: (none) Type: bug | Status: new Priority: normal | 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: | -------------------------------------+------------------------------------- Changes (by albertov): * Attachment "CKBug.hs" added. This module reproduces the bug without third-party dependencies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13742 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 Iceland_jack): Replying to [comment:5 goldfire]:

A fix would be to parameterize `(,)` by a `Constraintiness` parameter, as discussed [https://github.com/ghc-proposals/ghc-proposals/pull/32 here].

Any idea how much work adding it is? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13742#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): A bit more detail.... It's all a result of the ambiguity between tuples and constraints. * `A`, `B`, `C`, and `D` are all mutually recursive * When inferring the kind for them, they get initial kinds {{{ A :: k1 -> k2 B :: k3 -> k4 C :: k5 -> Constraint D :: k5 -> Constraint }}} where the `ki` are kind unification variables * Then we happen visit them in order `C` (and `D`), `B`, `A`. * So when kind-checking `B` we have not yet figured out `A`'s kind * And becuase of the tuple/constraint ambiguity, we prematurely choose that the tuple `(A l, A l)` will be a `BoxedTuple` not a `ConstraintTuple`. Something rather similar comes up with the empty tuple; we have an open ticket for that, #9547 (maybe others). What we really want, of course, is to defer the choice until we have worked out the kinds of `A`, `B`, `C`, and `D`; and there is no difficulty in principle with doing that. But it's tricky at the moment because we use one piece of code (`TcHsType.tc_hs_type`) for both kind checking (working out what the kinds of each type constructor are) and desugaring (producing a `Type` from a `HsType`. In the first of these steps we don't need to aggressively commit to which kind of tuple we want; in the latter step we do. This will become straightforward when we adopt #13737. Meanwhile, there's a decent workaround, so I'll park this one for now. I don't think there is an easy solution in the current setup. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13742#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13742: Code using ConstraintKinds needs explicit kind signature with GHC 8.2.1 -------------------------------------+------------------------------------- Reporter: albertov | Owner: (none) Type: bug | Status: new Priority: normal | 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: #11621 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * related: => #11621 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13742#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13742: Code using ConstraintKinds needs explicit kind signature with GHC 8.2.1 -------------------------------------+------------------------------------- Reporter: albertov | Owner: (none) Type: bug | Status: new Priority: normal | 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: #11621, #11715, | Differential Rev(s): #16139, #16148 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #11621, #11715 => #11621, #11715, #16139, #16148 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13742#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler