#9200: Milner-Mycroft failure at the kind level ----------------------------------------------+---------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by goldfire): Yes, this absolutely should be able to work but it currently doesn't, perhaps by design. Happily, I believe this one is actually quite easy to solve. See [https://github.com/ghc/ghc/blob/master/compiler/typecheck/TcHsType.lhs#L917 this comment]. I believe if we changed the kind-checking strategy for classes from `ParametricKinds` to `NonParametricKinds`, this problem would be solved. I also believe that this change would allow only ''more'' programs to type-check, and would thus be fully backward compatible. Indeed, in my branch where I'm implementing a merged type/kind language, I've gotten rid of `ParametricKinds`. Tracing this design through history, I think it came from work on the patch described in #6093. There, Simon proposed (and heard no complaints about) allowing polymorphic recursion if and only if a "complete user- supplied kind signature" ("cusk") is given. See [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind- polymorphism.html section 7.8.3] of the manual. However, a cusk is ''not possible'' for classes, giving Edward no way to proceed here. At the end of the comment trail of #6093, Simon asks for a better design. Here goes: allow recursive instantiations of a kind variable to vary if and only if that kind variable is ''mentioned'' in a type. I'm being quite literal here in my meaning of ''mentioned'' -- the kind variable must simply appear syntactically in the code. By appearing in the source, GHC can know to generalize over the kind variable "early on" and then can deal with the polymorphic recursion. With this design, the need for cusks goes away. I think the initial reason that cusks came about in the first place is from a perceived need to either allow polymorphic recursion or to disallow it. In terms, this is straightforward: there is either a type signature or there isn't. In types, however, Haskell syntax allows for various forms of partial kind signatures. But, we had the desire for a simple "yes" or "no" answer about polymorphic recursion, and so the cusk was born. What I'm proposing here is to embrace the gray area between "yes" and "no" and permit ''some'' polymorphic recursion -- specifically, over those kind variables that are mentioned in the source. Is this history accurate, from those involved (that is, mostly, Simon)? Do we see code that would be accepted under my proposal that would be surprising to users? Happily, implementing my proposal is dead easy -- just twiddle kind-inference strategies, as my proposal is called `NonParametricKinds` there. As some context, here is an example from closed type families (the one place where `NonParametricKinds` is used) that ''is'' confusing: {{{ type family LooksLikeId (x :: k) :: k where LooksLikeId x = Bool LooksLikeId x = Maybe }}} The kind of `LooksLikeId` surely looks like that of an identity function: `k -> k`. But, because type families are ''not'' parametric (hence the name `NonParametricKinds`), we can inspect the kind and branch on it. Note that the equations above ''do not'' overlap, as they are distinguished by their kind parameters. The definition above would fail to type-check without the `k` annotation, as that is necessary for GHC to know to generalize over the kind instead of just solve for it. Thoughts on any of this? Am I deeply misunderstanding some properties of type inference here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler