The Paterson Conditions for Type Checking in Haskell

Question

Could someone please explain (or give me some examples or the process) on why are these conditions necessary for the termination of the instance resolution process in Haskell? Or at least a link where this algorithm is described.

For example, I tried to find some lecture about it, but I only can find stuff about type inference and not this instance resolution process.

I quote from Haskell User Guide

The rules are these:

1. The Paterson Conditions: for each class constraint (C t1 ... tn) in the context
   1. No type variable has more occurrences in the constraint than in the head
   2. The constraint has fewer constructors and variables (taken together and counting repetitions) than the head
   3. The constraint mentions no type functions. A type function application can in principle expand to a type of arbitrary size, and so are rejected out of hand
2. The Coverage Condition. For each functional dependency, ⟨tvs⟩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 head.

Answer 1

The so-called 'Paterson Conditions', used to guarantee that instance resolution terminates under the FlexibleInstances extension, are fully documented in Chapter 5 of the paper Understanding Functional Dependencies via Constraint Handling Rules. Unfortunately, the discussion is quite technical and dense.

We could do with some gentler explanation giving an intuition as to what instances are legal; I've been trying to get my head around it for some time with no success.