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

 Replying to [comment:8 simonpj]:
 > 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.

 Yes, precisely. There's no real technical challenge here. I just want an
 easy way for the user to say what they mean: inference or specification.

 The problem with the CUSK rules as they are is that sometimes you've
 written a CUSK when you don't mean to. For example

 {{{
 data T (a :: Proxy k) where ...
 }}}

 According to the rules, this declaration has a CUSK. But suppose I want
 `k`'s kind to be inferred. The only way to do so is to write

 {{{
 data T :: Proxy k -> Type where ...
 }}}

 This form is a CUSK with `-XNoTypeInType` but is ''not'' a CUSK with
 `-XTypeInType`. The reason for the extra rule with `-XTypeInType` is to
 support this case, where the user wants inference. (Note that with
 `-XNoTypeInType`, `k`'s kind will always by `Type`, and so the issue of
 inference doesn't arise.)

 This particular problem is worse for closed type families and for classes,
 where there is no alternate syntax available if the user does not want a
 CUSK.

 The intent of my proposal is to make all of this simpler: the user simply
 says whether they want inference (no kind sig) or specification (kind
 sig). No fiddly rules. No exceptions.

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