#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 some more, I feel like there is potential weirdness with the changes I mentioned earlier, even if it works nicely for some simple examples. For instance, consider: {{{ u : a -> a -> a f : some a b. a -> a -> b f x y = u (g x y) (h x y) g : some c b. forall a. c -> a -> b g x y = f x y h : some c b. forall a. c -> a -> b h x y = f x y }}} Now, since `f` takes two arguments of the same type, this requires each of `g` and `h` to do the same. But, to ensure `g` and `h` are sufficiently polymorphic, we need to skolemize. These skolems then flow into the `c` unification variables, which in turn are unified due to `f`. So this will cause a skolem mismatch. So, I'm not sure it's a good idea for these sorts of examples to work, even if they could in some cases. It seems like it could easily be confusing when similar examples happen to work or not work depending on where skolems flow. So I guess I'm back to thinking that it's better for your G example to not check: {{{ u : a -> a -> T g : some c. forall k. c -> k -> T g x y = u x y }}} simply because it's due to a less confusing rule. Ermine has, of course, always generalized ''unification variables'' that are still free after this process; that is what is expected for types. I think it's handy for kinds as well (probably excepting the 'bad polymorophism' examples). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler