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