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

 Just a thought, in our compiler for Ermine we use a strategy very close to
 Mark P Jones' strategy with CUSKs.

 However when we have a type that is not fully what you'd call a CUSK
 because at least one of the type variables are unannotated we actually
 allow it to participate in a binding group SCC like any other type.

 We instantiate '''just''' those unannotated positions in the type with
 fresh kind variables not all.

 Then we run through the binding group checking subsumption for each,
 letting those checks accrete constraints on the unannotated types before
 we generalize over the whole SCC.

 A universe level down the code looks like:

 https://github.com/ermine-
 language/ermine/blob/master/src/Ermine/Inference/Type.hs#L150

 At the kind level the code is in a local branch and I'll push it out to
 github soon.

 This lets us fit somewhere in the middle between Mark P Jones' strategy
 and Richard's.

 Unannotated variables participate in cycles and unify out to whatever they
 must, while kind variables supplied explicitly annotated types can't be
 forced to unify with them without yielding skolem escapes.

 The rule then becomes that if you annotate some types with a kind
 involving explicit kind variable in a class declaration all kinds that
 unify with that kind variable will need to be annotated, but other kinds
 can be left untouched.

 In exchange you don't get more specific kinds than you ask for #9201, we
 can handle partially annotated polymorphic recursion like occurs here, and
 existing code so long as it doesn't rely on #9201 would still typecheck.

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