inference with functional dependencies

[Avi Pfeffer]

Inferring equality between types when there are functional dependencies
seems to be less powerful than I expected.  Here's a simple example:

class Eq b => C a b | a -> b

data T a = forall b . C a b => T b
data U a = forall b . C a b => U b

compare :: T a -> U a -> Bool
compare (T x) (U y) = x == y

I expected the compiler (GHC) would be able to deduce that the b type in
the representation of T a and U a must be the same, since both stand in a
C a b relationship, and a functionally determines b in that
relationship.  Instead I get the message:

    Inferred type is less polymorphic than expected
	Quantified type variable `b1' is unified with `b'
    When checking a pattern that binds
	x :: b
	y :: b1
    In an equation for function `Test.compare':
	Test.compare (T x) (U y) = x == y

Is this expected behavior?  Is there a way for me to provide the necessary
hints so that code like this could be accepted?

Thanks,
  Avi Pfeffer
--
Avi Pfeffer    avi@eecs.harvard.edu     www.eecs.harvard.edu/~avi
Maxwell Dworkin 251
Division of Engineering and Applied Sciences  Tel: (617) 496-1876
Harvard University                            Fax: (617) 496-1066