[Haskell-cafe] RE: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]

[Simon Peyton-Jones]

| 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