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

 Ermine's algorithm for this effectively has an additional quantifier,
 some. Your `G` definition is effectively equivalent to:

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

 g : some a. forall b. a -> b -> T
 g x y = u x y
 }}}

 'some' is effectively a quantifier for unification variables. So for
 instance, if I wrote:

 {{{
 h : some a b. a -> b -> T
 h x y = u x y
 }}}

 checking would succeed, with `h : a -> a -> T`. Also, some cannot occur
 arbitrarily in a type. It can only occur outer-most in a type ascription.

 The reason ermine rejects `g` right now is that the metavariable `a` is at
 an outer level of binding. They cannot be generalized over until the
 entire SCC is done being checked, while `g` is expecting to be polymorphic
 in `b`. This is the kind of check that would fail for an example like:

 {{{
 g : some a. forall b. a -> b -> T
 g x y = h x y

 h y x = g x y
 }}}

 We could try to be more intelligent, and do additional generalization as
 long as skolems wouldn't flow into other types in the binding group, or
 something, but we haven't gotten that fancy yet.

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