On Mon, 10 Apr 2006, Claus Reinke wrote:

...

(see the FunctionalDependencies page for background omitted here)

which seems to ignore much of the discussion of confluence we had here some weeks ago? I thought this list was for communication with the committee, and since the ticket exists, I had been hoping that the type class subcommittee would ensure that the wiki would be updated. but it seems I have been talking to myself..

Yes, I wondered what had happened to your previous argument for the memo constraint.

...

One of the problems with the relaxed coverage condition implemented by GHC and Hugs is a loss of confluence. Here is a slightly cut-down version of Ex. 18 from the FD-CHR paper:

class B a b | a -> b class C a b c | a -> b

instance B a b => C [a] b Bool

Starting from a constraint set C [a] b Bool, C [a] c d, we have two possible reductions:

1) C [a] b Bool, C [a] c d => c = b, C [a] b Bool, C [a] b d (use FD on C) => c = b, B a b, C [a] b d (reduce instance)

2) C [a] b Bool, C [a] c d => C a b, C [a] c d (reduce instance)

CHR-alt:

B a b <=> infer_B a b, memo_B a b. memo_B a b1, memo_B a b2 ==>b1=b2.

C a b c <=> infer_C a b c, memo_C a b c. memo_C a b1 c1, memo_C a b2 c2 ==> b1=b2. infer_C [a] b Bool <=> B a b. memo_C [a] b' c' ==> b'=b.

What's this last rule for? It mentions a b that does not appear in the head of the rule. If you mean the rule memo_C [a] b c, memo_C [a] b' c' ==> b = b'. then it is already subsumed by the more general memo_C a b1 c1, memo_C a b2 c2 ==> b1=b2. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be