[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 simonpj):

 I'm only questioning whether we need new syntax.

 Let me re-state what I think you are saying.

 * The kind of a type constructor can be ''inferred'' from its definition,
 or ''specified'' by a CUSK.

 * A CUSK ''specifies'' the kind of a type constructor, fully.  No need to
 look at any other definitions etc; it all comes from the CUSK.

 * In type declarations you can add kind signatures but they merely specify
 additional constraints that may guide the inference process.  For example
 {{{
 data T (a :: k -> *) = ...
 }}}
   constraints `a` to have a kind of the specified form, but it does no
 more than that.

 The thing you say is "incredibly confusing" is that the switch from
 inferred to specified is based on some fairly subtle syntactic rules, and
 you'd like to have a clearer syntactic distinction.  It's a software
 engineering issue, not a technical one.

 Separate kind signatures would be one solution.

 Simplifying the CUSK rules might be another.  The
 [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html
 #complete-user-supplied-kind-signatures-and-polymorphic-recursion existing
 rules] are not bad, actually, except for the mysterious second bullet
 which depends on explicit quantification of kind variables.  Otherwise the
 rule is ''it has a CUSK if every argument variable, and result kind have
 explicit signatures''.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13761#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler