Philip K.F. H??lzenspies wrote: [snip]
{- begin -} {-# OPTIONS -fglasgow-exts #-}
data Z -- Zero data S x -- Successor of x
class Add a b c | a b -> c instance Add Z q q instance Add p q r => (S p) q (S r)
{- end -}
[snip]
The coverage condition. For each functional dependency, tvc_left -> tvs_right, of the class, every type variable in S(tvs_right) must appear in S(tvs_left), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration.
In my mind, in this case: tvs_left = {a,b} tvs_right = {c} S(tvs_left) = {p,q} S(tvs_right) = {r}
What "occur in" means (mappings of type variables occurring in mappings of other type variables), I really don't quite understand. The example in the manual under 7.4.4.2, viz:
It's subset check. S(tvs_right) must be a subset of S(tvs_left) which is clearly not the case. The condition is sufficient (but not necessary) to let type checking terminate.
The suggested flag to "allow undecidable instances" is throwing me off, since it seems very unambiguously decidable to me.
Ambiguity is not the issue here, ensuring termination is. The consequence of using -fundecidable-instances is that there is no a priori guarantee that type checking will terminate. [*] If it does terminate, the final result will be correct. HTH, Bertram [*] In your particular example termination will probably be guaranteed by a structural property: In deriving Add (S x) y (S z) the compiler will look for an instance Add x y z where all three type terms are smaller. The nice thing about the coverage condition is save and can be checked easily per instance.