[GHC] #13761: Can't create poly-kinded GADT with TypeInType enabled, but can without

[GHC]

#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