[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 about this some, I realized that there's no reason to fail
 due to skolems 'escaping' into other types of the binding group, since
 we're about to generalize all the types anyway. So I've tweaked our
 algorithm to not care about that. Now the equivalent of your G example
 checks, and so does my example above:

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

 {{{
 g : forall b. b -> b -> T
 h : forall b. b -> b -> T
 }}}

 This seems sensible to me, and sounds like your proposal.

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