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

[Martin Sulzmann]

Simon Peyton-Jones writes:
 > | 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)?
 > 

Fullness (B) is a necessary condition to guarantee that the constraint
solver (aka CHR solver) derived from the type class program is confluent.

Here's an example (taken from the paper).

  class F a b c | a->b
  instance F Int Bool Char
  instance F a b Bool => F [a] [b] Bool

The FD is not full because the class parameter c is not involved in
the FD. We will show now that the CHR solver is not confluent.

Here is the translation to CHRs (see the paper for details)

  rule F a b1 c, F a b2 d  ==> b1=b2      -- (FD)
  rule F Int Bool Char    <==> True       -- (Inst1)
  rule F Int a b           ==> a=Bool     -- (Imp1)
  rule F [a] [b] Bool     <==> F a b Bool -- (Inst2)
  rule F [a] c d           ==> c=[b]      -- (Imp2)  


The above CHRs are not confluent. For example,
there are two possible CHR derivations for the initial
constraint store F [a] [b] Bool, F [a] b2 d

    F [a] [b] Bool, F [a] b2 d 
-->_FD (means apply the FD rule)
    F [a] [b] Bool, F [a] [b] d , b2=[b]
--> Inst2 
    F a b Bool, F [a] [b] d , b_2=[b]         (*)


Here's the second CHR derivation

    F [a] [b] Bool, F [a] b2 d 
-->_Inst2 
    F a b Bool, F [a] b2 d 
-->_Imp2 
    F a b Bool, F [a] [c] d, b2=[c]           (**) 


(*) and (**) are final stores (ie no further CHR are applicable).
Unfortunately, they are not logically equivalent (one store says
b2=[b] whereas the other store says b2=[c]).

To conclude, fullness is a necessary condition to establish confluence
of the CHR solver. Confluence is vital to guarantee completeness of
type inference.


I don't think that fullness is an onerous condition.

Martin