[still talking to myself..?]
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.
I should have mentioned that the improved confluence obtained by separating the dimensions of FD-based improvement and instance inference buys us a lot more than just permitting more valid programs (compared to the original, incomplete CHR): - separating the two dimensions of inference and improvement leads to better confluence (implementations are no longer forced to iterate improvement before continuing inference; fewer conservative restrictions are needed in the static semantics of TC; more valid code can be accepted) - better confluence guarantees that all improvement rules that apply will be run eventually, which means that the new CHR is self-checking wrt FD consistency! [if consistency is violated, there are at least two instances with different FD range types for the same FD domain types; that means there will be two instance improvement rules with the same lhs, but different equations on their rhs; if any constraint arises that would run into the FD inconsistency by using one of those improvement rules, the other will cause the derivation to fail] we can see this in action by looking at the relevant example of the FD-CHR paper (last revised Feb2006), section 5.1 Confluence, example 5: class Mul a b c | a b -> c instance Mul Int Float Float instance Mul Int Float Int the old CHR for this example (which violates FD consistency) is not confluent, allowing derivation of both c=Float and c=Int for the constraint Mul Int Float c. the revised paper still claims that consistency is "inuitively necessary" to guarantee confluence (it also still claims that it isn't sufficient, referring to the example we dealt with in the previous email). but if we apply the new Tc2CHR translation, we obtain a confluent CHR for the same example (there doesn't appear to be a way to switch off the consistency check in GHC, so I had to translate the two instances separately..): mul(A,B,C) <=> infer_mul(A,B,C), memo_mul(A,B,C). /* functional dependencies */ memo_mul(A,B,C1), memo_mul(A,B,C2) ==> C1=C2. /* instance inference: */ infer_mul(int,float,float) <=> true. infer_mul(int,float,int) <=> true. /* instance improvements: */ memo_mul(int,float,C) ==> C=float. memo_mul(int,float,C) ==> C=int. now, if we consider the problematic constraint again, and its two initially diverging derivations, we see that the derivations can be rejoined, exposing the inconsistency: mul(int,float,C) <=> infer_mul(int,float,C), memo_mul(int,float,C) [ ==> infer_mul(int,float,C), memo_mul(int,float,C), C=float <=> true, memo_mul(int,float,float), C=float ==> memo_mul(int,float,float), C=float, float=int | ==> infer_mul(int,float,C), memo_mul(int,float,C), C=int <=> true, memo_mul(int,float,int), C=int ==> memo_mul(int,float,int), C=int, int=float ] <=> fail this dynamic safety does not mean that we should drop the consistency check in the static semantics completely! but whereas the old CHR translation _depends_ on the consistency check for safety, and is therefore stuck with it, the new translation gives us some manouvering space when we try to relax that check to account for the combination of overlap resolution and FDs. cheers, claus