| I believe that this "weak coverage condition" (which is also called | "the dependency condition" somewhere on the wiki) is exactly what GHC | 6.4 used to implement but than in 6.6 this changed. According to | Simon's comments on the trac ticket, this rule requires FDs to be | "full" to preserve the confluence of the system that is described in | the "Understanding Fds via CHRs" paper. I have looked at the paper | many times, and I am very unclear on this point, any enlightenment | would be most appreciated. Right. In the language of http://hackage.haskell.org/trac/ghc/ticket/1241, last comment (date 10/17/07), it would be *great* to replace the Coverage Condition (CC) with the Weak Coverage Condition (WCC) as Mark suggests. BUT to retain soundness we can only replace CC with WCC + B WCC alone without (B) threatens soundness. To retain termination as well (surely desirable) we must have WCC + B + C (You'll have to look at the ticket to see what B,C are.) And since A+B+C are somewhat onerous, we probably want to have CC or (WCC + B + C) At least we know of nothing else weaker that will do (apart from CC of course). Like you, Iavor, I find it very hard to internalise just why (B) and (C) are important. But I believe the paper gives examples of why they are, and Martin is getting good at explaining it. Martin: can you give an example, once more, of the importance of (B) (=fullness)? Anyway that's why I have been moving slowly in "fixing" GHC: the rule CC or (WCC + B + C) just seems too baroque. Simon