fundeps help

[Simon Peyton-Jones]

| Is it really a good idea to permit a type signature to include
| equality constraints among unifiable types?  Does the above type
| signature mean something different from a ->a?  Does the type signature:
|      foo :: (a~Bar b) => a -> Bar b
| mean something different from:
|      foo :: Bar b -> Bar b
| ?  I know that System FC is designed to let us write stuff like:
|      foo :: (Bar a ~ Baz b) => Bar a -> Baz b
| Which is of course what we need for relating type functions.  But I'm
| wondering if there's a subtlety of using an equality constraint vs
| just substitution that I've missed

No, you didn't miss anything.  I wouldn't expect anyone to write these types directly.  But it can happen:
        class C a b | a->b
        instance C Int Bool

        class D x where
          op :: forall y. C x y => x -> y

        instance D Int where
          op = ...

In the (D Int) instance, what's the type of op?  Well, it must be
        op :: forall y. C Int y => Int -> y

And here we know that y=Bool; yet since we don't write the type sig directly we can't say it.  So GHC's implementation of fundeps rejects this program; again it can't be translated into System F.

Simon