By "global" I really meant "throughout the scope of the type variable concerned.
Nevertheless, the program you give is rejected, even though the scope is global:
class FD a b | a -> b
f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = y
Both GHC and Hugs erroneously reject the program,
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?
The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) isn't up to the job.
Interesting. When the FD-via-CHR discussion started, I toyed with the idea of writing an instance inference engine based on CHR (since CHR happen to be a variant of CPN - Coloured Petri Nets -, I happened to have an implementation at hand;-). But once I noticed the difficulties of managing local constraint stores (and exchanging some, but not all inferred information with the global constraint store), I abandoned the idea. Ever since then I've been wondering how GHC handles that!-)
That is what we are fixing with type functions. I do not know how to fix it for FDs (except by way of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language. This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to.
Since FDs constrain the set of valid instances, I had been wondering whether one could apply the FD-based refinements/substitutions to the code obtained (just as they are applied to the class constraints) while keeping a typed intermediate language. Claus