a second oversight, in variation B: CHR rules are selected by matching, not by unification (which is quite essential to modelling the way type class inference works). this means that the idea of generating memo_ constraints for the instance fdis and relying on the clas fdi rules to use that information is not going to work directly. however, we can look at the intended composition of those fdi instance rules with the fdi class rules, and specialize the latter when applied to the rhs of the former (assuming unification while doing so). !! the nice thing about this is that variation B now looks very much like the original translation, differing only in the splitting of roles, without any other tricks merged in. that means it should now be more obvious why variation B is a modification of the original translation with better confluence properties. all confluence problems in the FD-CHR paper, as far as they were not due to instances inconsistent with the FDs, seem to be due to conflicts between improvement and inference rules. we restore confluence by splitting these two constraint roles, letting inference and improvements work on constraints in separate roles, thus removing the conflicts. ============= Tc2CHR alternative, with separated roles class C => TC a1..an | fd1,..,fdm where fdi is of the form: ai1..aik -> ai0 -> TC a b <=> infer_TC a b, memo_TC a b, C. (two roles +superclasses) -> memo_TC a1..an, memo_TC th(b1)..th(bn) => ai0=bi0. (fdi) where th(bij) | j>0 = aij th(bl) | not (exists j>0. l==ij) = bl ============= Variation B (separate instance inference/FD improvement): instance C => TC t1..tn -> infer_TC t1..tn <=> C. (instance inference) -> memo_TC th(b1)..th(bn) => ti0=bi0. (fdi instance improvement) where th(bij) | j>0 = tij th(bl) | not (exists j>0. l==ij) = bl ============================================= in particular, the new CHRs for examples 14 and 18 (coverage violations, hence not variable-restricted, hence confluence proof doesn't apply) should now be confluent, because even after simplification, we can still use the class FDs for improvement. here are the relevant rules for example 14: /* one constraint, two roles + superclasses */ eval(Env,Exp,T) <=> infer_eval(Env,Exp,T), memo_eval(Env,Exp,T), true. /* functional dependencies */ memo_eval(Env,Exp,T1), memo_eval(Env,Exp,T2) ==> T1=T2. /* instance inference: */ infer_eval(Env,expAbs(X, Exp),to(V1, V2)) <=> eval(cons((X, V1), Env), Exp, V2). /* instance improvements: */ memo_eval(Env_,Exp_,T_) ==> T_=to(V1, V2). and the troublesome example constraints: eval(Env,expAbs(X,Exp),T1), eval(Env,expAbs(X,Exp),T2). -> infer_eval(Env,expAbs(X,Exp),T1), infer_eval(Env,expAbs(X,Exp),T2), memo_eval(Env,expAbs(X,Exp),T1), memo_eval(Env,expAbs(X,Exp),T2). [ -> [class FD first] infer_eval(Env,expAbs(X,Exp),T2), memo_eval(Env,expAbs(X,Exp),T2), T1=T2. | -> [instance improvement and simplification first] eval(cons((X,V11),Env),Exp,V12), eval(cons((X,V21),Env),Exp,V22), memo_eval(Env,expAbs(X,Exp),T1), memo_eval(Env,expAbs(X,Exp),T2), T1=to(V11,V12), T2=to(V21,V22). ] -> [rejoin inferences] eval(cons((X,V21),Env),Exp,V22), memo_eval(Env,expAbs(X,Exp),T2), T1=T2, T2=to(V21,V22). -> .. cheers, claus ps I've only listed the updated variation B here, to limit confusion. if you want the updated code and full text, you should be able to use darcs get http://www.cs.kent.ac.uk/~cr3/chr/