| 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