Note [Paterson conditions]

The Paterson Conditions ensure termination of instance resolution.
Given an instance declaration
   instance (..., C t1.. tn, ...) => D s1 .. sm

we check that each constraint in the context of the instance is
"Paterson-smaller" than the instance head.  The underlying idea of
Paterson-smaller is that

    For any ground substitution S, for each constraint P in the
    context, S(P) has fewer type constructors, counting repetitions,
    than the head S(H)

We implement this check by checking the following syntactic conditions:

(PC1) No type variable has more (shallow) occurrences in P than in H.

      (If not, a substitution that replaces that variable with a big type
      would make P have many more type constructors than H. Side note: we
      could in principle skip this test for a variable of kind Bool,
      since there are no big ground types we can substitute for it.)

(PC2) The constraint P has fewer constructors and variables (taken
      together and counting repetitions) than the head H.  This size
      metric is computed by sizeType.

      (A substitution that replaces each variable with Int demonstrates
      the need.)

(PC3) The constraint P 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.  See #15172.)

(See Section 5 of "Understanding functional dependencies via Constraint
Handling Rules", JFP Jan 2007; and the user manual section "Instance
termination rules".)

We measure "size" with the data type PatersonSize, in GHC.Tc.Utils.TcType.
  data PatersonSize
    = PS_TyFam TyCon
    | PS_Vanilla { ps_tvs :: [TyVar]  -- Free tyvars, including repetitions;
                 , ps_size :: Int}    -- Number of type constructors and variables

* ps_tvs deals with (PC1)
* ps_size deals with (PC2)
* PS_TyFam deals with (PC3)