there is no implication that d=Bool (you could add: 'instance B a b => C [a] b Char' without violating FD consistency).
These instances (alpha-renamed): instance B a1 b1 => C [a1] b1 Bool instance B a2 b2 => C [a2] b2 Char
violate the consistency condition: a substitution that unifies a1 and a2 need not unify b1 and b2, because the consistency condition makes no mention of the contexts. (If it did, the instance improvement rule would be invalid.)
?? the consistency condition does mention b1 and b2 as t_b and s_b, so any substitution that unifies a1 and a2 (t_a and s_a) needs to unify b1 and b2, independent of context. note also that we are talking about different things here: I am talking about FD consistency, you are talking about the FD consistency condition. let's be concrete: class B a b | a -> b class C a b c | a -> b instance B a1 b1 => C [a1] b1 Bool instance B a2 b2 => C [a2] b2 Char with these declarations, you are concerned about constraints C [a] b Bool,C [a] c Char, which you claim are substitution instances of these declaration heads even if b and c differ. but the class instances of class C are constrained by an FD, and if b and c differ, these two constraints are _not_ substitution instances under that FD. they would be substitution instances if that FD wasn't there (*). the FD consistency condition is an approximation of FD consistency, and it is a strange approximation at that, because it is neither sufficient nor necessary (with the alternative CHR translation) for consistency: - if all instance declarations fulfill the FD consistency condition, the constraint store may still be inconsistent, because it may represent an inconsistent query; so the condition is not sufficient - one of the bonuses of a confluent CHR is that deductions on inconsistent stores will not terminate successfully (if they terminate, they are certain to fail), so the condition is not necessary, either [it was with the old translation, though] as this example shows once again, there are instance declarations for which the FD consistency condition, as currently interpreted by Hugs, fails, even though no inconsistent constraints are implied. so I fail to see the point of continuing to require the FD consistency condition in unrevised form. but my point was that there is no confluence problem. everything else, with the exception of termination, follows from there. cheers, claus (*) this is similar to patterns and guards in the expression language, for instance: f a = .. -- some function c [a1] b1 Bool | b1 == f [a1] = b a1 b1 c [a2] b2 Char | b2 == f [a2] = b a2 b2 now, c [a] b1 Bool and c [a] b2 Char are defined if (b1==f [a]) and (b2==f [a]) and if b a b1 and b a b2 are defined as well. c [a] d Bool with (d/=f[a]) matches the pattern, but fails the guard, so it is not a substitution instance of c's left hand sides under the guard.