#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