another interesting improvement in confluence, not related to FDs: the old CHR translation generated proof obligations for superclass contexts via propagation rules, which (similar to the propagation rules for instance improvement) might be in conflict with the instance simplification rules, jeopardizing confluence unless existence of superclass instances is checked separately (as currently required in Haskell). by putting superclass constraints as proof obligations on par with instance inference and FD-based improvement in the new CHR translation, we have ensured that the CHR will be confluent even if the superclass check is omitted. take example 28 from "theory of overloading": class E t instance E t => E [t] instance E Int class E t => O t instance O [t] which generates these CHR (I switched the implementation from TH to HSX as a frontend, to avoid GHC's built-in checks): /* one constraint, two roles + superclasses */ e(T) <=> infer_e(T), memo_e(T), true. /* instance inference: */ infer_e(list(T)) <=> e(T). /* instance inference: */ infer_e(int) <=> true. /* one constraint, two roles + superclasses */ o(T) <=> infer_o(T), memo_o(T), e(T). /* instance inference: */ infer_o(list(T)) <=> true. consider the problematic constraint, and we see that there is not even room for initial divergence, as the proof obligation for the superclass constraint is established before inference for o can even begin: o(list(U)) <=> infer_o(list(U)), memo_u(list(U)), e(list(U)) <=> memo_u(list(U)), e(list(U)) <=> memo_u(list(U)), infer_e(list(U)), memo_e(list(U)) (note the outstanding proof obligation infer_e(list(U)) ). this means that we could remove the early superclass constraint check from Haskell, and the resulting uglinesses: - superclass instances have to be visible at subclass instance declaration time, not at subclass constraint usage time (this is really weird) - lack of superclass instances causes compilation to fail, instead of just causing unusability of subclass instances - superclass contexts cannot be used to abstract out common contexts from methods/instances/goals, because superclass contexts behave differently from other contexts what do you think about this suggestion? cheers, claus ps that example 28 is interesting for another reason, too: the missing instance is "instance E t", but GHC will _not_ accept the program if you add that instance, unless we specify allow-incoherent-instances! Hugs will accept it, but its behaviour is that of GHC's "bad" flag (always select the most general instance).. the error message given by GHC, without that flag, is the interesting bit: even though we have instances of E for any type, GHC can't determine that (it would require a differentiation by cases)!