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

 Having thought some more, I feel like there is potential weirdness with
 the changes I mentioned earlier, even if it works nicely for some simple
 examples. For instance, consider:

 {{{
 u : a -> a -> a

 f : some a b. a -> a -> b
 f x y = u (g x y) (h x y)

 g : some c b. forall a. c -> a -> b
 g x y = f x y

 h : some c b. forall a. c -> a -> b
 h x y = f x y
 }}}

 Now, since `f` takes two arguments of the same type, this requires each of
 `g` and `h` to do the same. But, to ensure `g` and `h` are sufficiently
 polymorphic, we need to skolemize. These skolems then flow into the `c`
 unification variables, which in turn are unified due to `f`. So this will
 cause a skolem mismatch.

 So, I'm not sure it's a good idea for these sorts of examples to work,
 even if they could in some cases. It seems like it could easily be
 confusing when similar examples happen to work or not work depending on
 where skolems flow. So I guess I'm back to thinking that it's better for
 your G example to not check:

 {{{
 u : a -> a -> T

 g : some c. forall k. c -> k -> T
 g x y = u x y
 }}}

 simply because it's due to a less confusing rule.

 Ermine has, of course, always generalized ''unification variables'' that
 are still free after this process; that is what is expected for types. I
 think it's handy for kinds as well (probably excepting the 'bad
 polymorophism' examples).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9200#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler