Need help understanding the Coverage Condition

[Bertram Felgenhauer]

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.