#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): Replying to [comment:23 dolio]:
Is the entire problem closed, partially annotated type families that are non-parametric, and therefore act like GADT definitions and lack principal types?
Not just these. Also partially annotated datatypes and classes will lack principal kinds. Here is the example: {{{ data W f (a :: k) where MkW :: W Maybe Int -> W f a }}} Do we have `W :: (k -> *) -> k -> *` or `W :: (* -> *) -> k -> *`, among others? Both seem reasonable, though the latter is certainly easier to infer. To eliminate ambiguity, we have to add the restriction to (PARGEN). This makes it clear that the second kind is the only allowable one.
And is the motivation to then have a uniform rule for both these and everything else that doesn't require detecting situations that would fail to have a principal type?
Yes, that's my understanding.
You (goldfire) and I discussed what we're doing in Ermine, which is now
quite a lot like the (original) PARGEN strategy. From my understanding, your original implementation was like (PARGEN) + side condition. Only after discussing did you (effectively) remove the side condition.
It seems to work for the sort of partially specified type signatures we have, and it works for polymorphic recursion, including polymorphic recursion with partial signatures. For instance:
{{{ let { u : a -> a -> a ; u x _ = x ; f : some b c. forall a. a -> b -> c ; f x y = let { z = u x y } in g x y ; g _ y = f () y } in f }}}
Without the signature on `f` the inferred type is `() -> () -> c`, but with it the inferred type is `b -> b -> c`.
I believe the original (PARGEN) "works", in that it is sound, for an appropriate definition of sound. However, it can infer non-principal types, which seems bad. I don't think it's very wrong for Ermine to adopt (PARGEN) - side condition, but I have to say I don't think it's very right, either. I believe that the example you give has a principal type, which is inferred correctly.
Anyhow, I'm not particularly adamant about your choice of (original)
PARGEN vs. NEWCUSK. But I'd like to understand what exactly the objections were, and whether they're tied to GADTs and type families. I would say that the problems are wholly independent of GADTs and type families. There is a problem with closed type families that is closely related, but the fundamental problem is independent. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler