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