#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