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