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

 I think Simon got one key detail in (RICHARD) wrong: I ''do'' propose to
 generalize after kind-checking all the declarations, not defaulting to
 `*`.

 The way I see it is this: there is "good" polymorphism and "bad"
 polymorphism.

 Here is "good":

 {{{
 type family IsJust x where
   IsJust Nothing = False
   IsJust (Just x) = True
 }}}

 Without any annotation, I would want to infer `forall k. Maybe k -> *` as
 the kind for `IsJust`. This goes against Simon's conclusion that all kind
 polymorphism should be annotated. I actually would argue that the genie
 about this sort of polymorphism is out of the bottle, and that Simon's
 proposal would be too big a breaking change.

 Here is "bad" polymorphism:

 {{{
 type family F x where
   F Bool = True
   F Maybe = False
 }}}

 It is perfectly reasonable to infer `forall k. k -> *` for the kind of
 `F`. Indeed, this could even be implemented without too much trouble. (I
 think I ''did'' implement this behavior along the way to the current
 behavior for closed type families!) But, I think most users would prefer
 to get a kind error in this case. If they want this polymorphism, use an
 annotation.

 What's the difference between "good" and "bad" polymorphism? "Good" is
 parametric and "bad" is non-parametric. Hence the name
 `NonParametricKinds`.

 The examples above come from type families. Extending these ideas to
 datatypes is awkward because datatypes don't (currently) support kind-
 indexing (essentially, being GADT-like in kind parameters) in the right
 way. The closest we can really get is to think about polymorphic
 recursion, which is where this all started. Thus, in the context of
 datatypes and classes, I agree that the name `NonParametricKinds` is
 bogus.

 What this all leads to is this: we want to allow "good" polymorphism
 without an annotation but to allow "bad" polymorphism only if specifically
 requested. This is exactly the story with closed type families today. And,
 if I'm understanding all the details correctly, in the datatype/class
 world, this means that we get non-polymorphic recursion to work all the
 time, but polymorphic recursion only when requested. After all, if you
 cross your eyes, polymorphic recursion can look a little like non-
 parametric polymorphism: both are cases when a type parameter is used
 inconsistently in a definition.

 I think the strategy I'm outlining is not unlike the behavior Edward
 describes in Ermine. The only difference I can spot is that my strategy
 allows unification variables to unify with skolems, where Ermine's seems
 to avoid this. For example:

 {{{
 type family G x (y :: k) :: Constraint where
   G x y = (x ~ y)
 }}}

 Here, the kind of `x` must be `k`, but that's acceptable. Would that fail
 in Ermine? I could certainly see that failure here could be reasonable.

 As a small aside, I wonder how any of this interacts with the coming
 partial type signatures at the term level. How do those interact with
 polymorphic recursion?

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