
#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