| while both GHC and Hugs accept this variation: | | class FD a b | a -> b | f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 | f x y = undefined | | and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'. | | So they use the FD globally (when checking use of 'f'), but not locally | (when checking the definition of 'f'). Is that interpretation correct, or is | there another bug involved? No, by "globally" I meant "throughout the scope of a type variable". I'm surprised GHC accepts the program you give, because it should unify two skolems. With a minor change it fails f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = y As I say, GHC's implementation of FDs is flaky and inconsistent; and that is not just because I'm lazy but because it is hard to know just what to do, most especially in situations like this when there is no System F translation. That is why I've been working so hard on FC. Simon