[GHC] #9200: Milner-Mycroft failure at the kind level
GHC
ghc-devs at haskell.org
Thu Jun 19 17:54:51 UTC 2014
#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
More information about the ghc-tickets
mailing list