#13761: Can't create poly-kinded GADT with TypeInType enabled, but can without -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType 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 goldfire): A separate kind signature will be understood independent of the type definition -- much like how type signatures on functions are understood (and kind-generalized) independently of the body. For example, consider {{{ data Proxy (a :: k) = P data S :: Proxy k -> Type where MkS :: S (P :: Proxy Maybe) }}} What's the type of `k`? Taking the definition into account, we can see that `k :: Type -> Type`. But if we must take the definition into account, then we don't have a CUSK, by definition. Currently, the declaration above causes GHC to complain that `Type -> Type` does not match `k`, as we're using `S` at a different instantiation in its body than in its head (i.e. using polymorphic recursion). Change to {{{ data S :: forall k. Proxy k -> Type where ... }}} and now we get {{{ You have written a *complete user-suppled kind signature*, but the following variable is undetermined: k0 :: * Perhaps add a kind signature. }}} This is quite correct. The declaration looks like it has a CUSK, but really it doesn't. Instead, we can write {{{ data S :: forall (k :: Type -> Type). Proxy k -> Type where ... }}} or {{{ data S :: forall (kk :: Type) (k :: kk). Proxy k -> Type where ... }}} both of which are accepted. Note that these define ''different'' types: the second defines a kind-indexed GADT. The point of all this is that it's incredibly confusing. Much better would be (*) A definition can use polymorphic recursion if it has a standalone type/kind signature. Simple! It works for types and terms. And it's exactly what happens for terms today. Under (*), all the declarations for `S` would be rejected, as none of them have a standalone kind signature. (The proposal will also describe `-XCUSKs`, on by default, that retains the current behavior. This extension will be off by default and deprecated in due course.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13761#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler