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