[GHC] #9200: Milner-Mycroft failure at the kind level

[GHC]

#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