#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