FDs and confluence

[Martin Sulzmann]

Ross Paterson writes:
 > (see the FunctionalDependencies page for background omitted here)
 > 
 > 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)
           ^^^^^
should be  B a b


 > The proposed solution was to tighten the restrictions on instances to
 > forbid those like the above one for C.  However there may be another
 > way out.
 > 
 > The consistency condition implies that there cannot be another
 > instance C [t1] t2 t3: a substitution unifying a and t1 need not
 > unify b and t2.  Thus we could either
 > 
 > 1) consider the two constraint sets equivalent, since they describe
 >    the same set of ground instances, or
 > 

That's troublesome for (complete) type inference.
Two constraint stores are equivalent if they are equivalent
for any satisfying ground instance? How to check that?

 > 2) enhance the instance improvement rule: in the above example, we
 >    must have d = Bool in both cases, so both reduce to
 > 
 > 	c = b, d = Bool, B a b
 > 
 >    More precisely, given a dependency X -> Y and an instance C t, if
 >    tY is not covered by tX, then for any constraint C s with sX = S tX
 >    for some substitution S, we can unify s with S t.
 > 

I'm not following you here, you're saying?

rule C [a] b d ==> d=Bool

Are you sure that you're not introducing further "critical pairs"?

 >    We would need a restriction on instances to guarantee termination:
 >    each argument of the instance must either be covered by tX or be
 >    a single variable.  That is less restrictive (and simpler) than
 >    the previous proposal, however.
 > 
 > Underlying this is an imbalance between the two restrictions on instances.
 > In the original version, neither took any account of the context of the
 > instance declaration.  The implementations change this for the coverage
 > condition but not the consistency condition.  Indeed the original form of
 > the consistency condition is necessary for the instance improvement rule.
 > 

Maybe, you found a "simple" solution (that would be great)
but I'not 100% convinced yet.


The problem you're addressing only arises for non-full FDs.
Aren't such cases very rare in practice?

Martin