[Haskell-cafe] Functional dependencies and type inference

[Einar Karttunen]

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