Need help understanding the Coverage Condition

[Philip K.F. Hölzenspies]

L.S.,

I have difficulty understanding the Coverage Condition. Hopefully,
someone has the time and is willing to explain this to me. Obviously,
I went ahead and hacked together something horribly entangled, but I
found a small example that already shows the behaviour I do not
understand.

Type-level addition of Church numerals:

{- 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 -}

The error GHCi produces is:

    Illegal instance declaration for `Add (S x) y (S z)'
        (the Coverage Condition fails for one of the functional
dependencies;
         Use -fallow-undecidable-instances to permit this)
    In the instance declaration for `Add (S x) y (S z)'
Failed, modules loaded: none.


I checked the user guide (7.4.4.1) for criteria for functional
dependencies and checked that I do not violate the assertions. I don't
violate assertions 1a and 1b, but assertion 2 (the coverage condition)
I have trouble reading:

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:

instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v

seams related, but unfortunately is not elaborated upon beyond "[it]
does not obey the coverage condition"

The suggested flag to "allow undecidable instances" is throwing me
off, since it seems very unambiguously decidable to me.

Regards,
Philip