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