I want to use functional dependencies in a way I've not yet seen: to enforce commutativity. I define class Mul a b c | a b -> c, b a -> c where mul :: a -> b -> c I want instance (Mul a b c) => Mul b a c where mul x y = mul y x do what I expect: if I can multiply a and b, then I can multiply b and a _and always have the same type_. In a sense, this makes multiplication commute (in the land of types). For a whole variety of reasons, the many (4 or 5 now) ways I've tried to make this work have failed, both using Hugs and GHC. I mentioned I wanted typed multiplication to commute. Let me explain more thoroughly: suppose I had data Unit u v = Unit u v I want (Unit u1 value1) `mul` (Unit u2 value2) to have the same type as (Unit u2 value2) `mul` (Unit u1 value1). So say u1 :: Int, u2 :: Float, then (Unit u1 value1) `mul` (Unit u2 value2) :: (Unit Int (Unit Float blah)) and (Unit u2 value2) `mul` (Unit u1 value1) :: (Unit Int (Unit Float blah)) I don't care if the result type is Unit Int ... or Unit Float ..., as long as it is a) consistent and b) inferred and c) enforced. So far, no luck. A few other questions: What happenned to +m in Hugs? In general, if I wanted a fundep to specify that a pair (a, b) determined c _regardless of the order of a and b_, how could it be done? Why doesn't a b -> c, b a -> c do this? What I mean is that if I have one of a, b and Int (say) and c a Float, then I could infer the other of a, b once I have a single instance. And a 'bug' report: in the overlapping instance one-liner above, the Mul a b c => Mul b a c, I can have this in place and write contradictory instances that violate the fundeps that are not caught in GHC. (Hugs does not allow the overlapping instances to begin with, even worse.) Well, that became a clearinghouse for the frustrations of the last several days. Sorry. Thanks, Nick