Einar Good question. This is a more subtle form of the same problem as I described in my last message. In fact, it's what Martin Sulzmann calls "the critical example". Here is a boiled down version, much simpler to understand. module Proxy where class Dep a b | a -> b instance Dep Char Bool foo :: forall a. a -> (forall b. Dep a b => a -> b) -> Int foo x f = error "urk" bar :: (Char -> Bool) -> Int bar g = foo 'c' g You would think this should be legal, since bar is just an instantation of foo, with a=Char and b=Bool. But GHC rejects it. Why? GHC looks at the call to foo (in bar's RHS), and instantiates it with a=Char. That tells it that the second argument should have type (forall b. Dep Char b => Char -> b) But it doesn't! It has type (Char -> Bool). And to GHC these are not the same types. You may say that they *should* be the same types. The crispest way I know to explain why it arguably should be rejected is to try translating the program into System F (which is what GHC actually does). Then the RHS of bar looks like bar (g::Char->Bool) = foo {Char} 'c' (...???...) The {Char} is the type argument to foo. But what can we pass for (...???...)?. We must pass a polymorphic function, with type forall b. Dep Char b -> Char -> b But all we have is g::Char->Bool. And System F has no way to connect the two. Well, that's the problem anyway. I can think of three "solutions": - Reject such programs (GHC's current solution) - Abandon compilation via System F - Extend System F I'm working on the third of these, with Martin, Manuel, and Stephanie. Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of | Einar Karttunen | Sent: 15 July 2005 13:48 | To: haskell-cafe@haskell.org | Subject: [Haskell-cafe] Functional dependencies and type inference | | Hello | | I am having problems with GHC infering functional dependencies related | types in a too conservative fashion. | | > class Imp2 a b | a -> b | > instance Imp2 (Foo a) (Wrap a) | > | > | > newtype Wrap a = Wrap { unWrap :: a } | > data Foo a = Foo | > data Proxy (cxt :: * -> *) | > | > foo :: Imp2 (ctx c) d => Proxy ctx -> (forall a b. (Imp2 (ctx a) b) => a -> b) -> c -> d | > foo p f x = f x | | The type of "foo (undefined :: Proxy Foo)" is inferred as | "forall c. (forall a b. (Imp2 (Foo a) b) => a -> b) -> c -> Wrap c" | which shows the outmost functional dependence is working fine. ctx | is carried to the inner Imp2. | | However "foo (undefined :: Proxy Foo) Wrap" will fail complaining that | | Couldn't match the rigid variable `b' against `Wrap a' | `b' is bound by the polymorphic type `forall a b. (Imp2 (ctx a) b) => a -> b' | at <interactive>:1:0-32 | Expected type: a -> b | Inferred type: a -> Wrap a | In the second argument of `foo', namely `Wrap' | | My guess is that GHC cannot see that the functional dependency | guarantees that there are no instances which make the inferred | type invalid. Any solutions to this problem? | | | - Einar Karttunen