#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): This example: {{{ foo :: forall f a. f a -> f a foo = ... where g :: f Int -> Int }}} just seems like bad policy to me. The top signature is a partial signature, the missing pieces (the kinds) should be solved, and it is not sufficient to only look at the signature of `foo` to do that solving. I can construct similar examples in Ermine, although it is a bit convoluted due to our currently meager tooling: {{{ :type let { f : forall f a. f a -> f a ; f x = x } in f forall {k} (f : k -> *) (a : k). f a -> f a }}} {{{ :type let { f : forall f a. f a -> f a ; f x = x where { z = g x ; g : some f a b. f a -> f b -> b ; g _ _ = "" } } in f forall (f : * -> *) (a : *). f a -> f a }}} Effectively, this signature is the same as (for us) {{{ some k1 k2. forall (f : k1) (a : k2). f a -> f a }}} although we don't currently handle some-bound kinds; unspecified kinds act similarly, though. The problem with this example seems to be deciding on things too early, not generalizing. For instance, doesn't PARTIAL error if you apply the same kind of policy to: {{{ foo :: forall f a. f a -> f a foo = ... where g :: f Maybe -> f Maybe }}} `f` will be defaulted to `* -> *`, but that is wrong for application to `Maybe`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler