#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