[GHC] #15273: Datatypes with CUSKs should quantify over unknown kinds

[GHC]

#15273: Datatypes with CUSKs should quantify over unknown kinds
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):  Phab:D4845     |         Wiki Page:
-------------------------------------+-------------------------------------
 In [https://github.com/ghc-proposals/ghc-proposals/pull/54 the future], we
 will be able to give full kind signatures to datatype declarations. But in
 the present, we use CUSKs to write kind signatures.

 However, consider

 {{{#!hs
 data T (a :: Proxy k)
 }}}

 That has a CUSK, according to the CUSK rules. Yet we don't know the kind
 of `k`. Currently, this definition is rejected, accusing the user of lying
 about having a complete kind. However, let's instead pretend the user had
 written

 {{{#!hs
 type T :: Proxy k -> Type
 data T a
 }}}

 After all, that's what the CUSK is shorthand for. In this case, it's clear
 that we should infer `T :: forall k1 (k :: k1). Proxy k -> Type`, just the
 way we would do with a term-level type signature.

 This turns out to be quite easy. See Phab:D4845.

 This change allows strictly more programs to be accepted, and I think it
 falls under the threshold for requiring a proposal.

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