#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 dolio): This example: {{{ data W f (a :: k) where MkW :: W Maybe Int -> W f a }}} is just another Milner-Mycroft problem. The inferred kind is `(* -> *) -> k -> *`. The principal kind is `k0 -> k -> *`, but it can't be inferred. Just like {{{ data W f a = W (W Maybe Int) }}} will have inferred kind `(* -> *) -> * -> *`, even though `k0 -> k -> *` is valid and strictly more general.
From my understanding, your original implementation was like (PARGEN) + side condition. Only after discussing did you (effectively) remove the side condition.
Yes, but this is because we were using skolem variables, which can lead to confusing rejection of partially annotated mutual definitions. When we started basing our algorithm on something closer to GHC, using what I think you called SigTvs, plus a per-signature distinctness check, that objection was no longer valid.
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.
Hindley-Milner infers non-principal types (so does GHC, of course).
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 still don't think we have an example that doesn't involve GADTs or type families. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler