Note [Types for coercions, predicates, and evidence]

A "predicate" or "predicate type",
    type synonym `PredType`
    returns True to `isPredTy`
is any type of kind (CONSTRAINT r) for some `r`.

  (a) A "class predicate" (aka dictionary type) is the type of a (boxed)
      type-class dictionary
        Test: isDictTy
        Binders: DictIds
        Kind: Constraint
        Examples: (Eq a), and (a ~ b)

  (b) An "equality predicate" is a primitive, unboxed equalities
        Test: isEqPred
        Binders: CoVars (can appear in coercions)
        Kind: CONSTRAINT (TupleRep [])
        Examples: (t1 ~# t2) or (t1 ~R# t2)

  (c) A "simple predicate type" is either a class predicate or an equality predicate
        Test: isSimplePredTy
        Kind: Constraint or CONSTRAINT (TupleRep [])
        Examples: all coercion types and dictionary types

  (d) A "forall-predicate" is the type of a possibly-polymorphic function
      returning a predicate; e.g.
           forall a. Eq a => Eq [a]

  (e) An "irred predicate" is any other type of kind (CONSTRAINT r),
      typically something like `c` or `c Int`, for some suitably-kinded `c`


* Predicates are classified by `classifyPredType`.

* Equality types and dictionary types are mutually exclusive.

* Predicates are the things solved by the constraint solver; and
  /evidence terms/ witness those solutions.  An /evidence variable/
  (or EvId) has a type that is a PredType.

* Generally speaking, the /type/ of a predicate determines its /value/;
  that is, predicates are singleton types.  The big exception is implicit
  parameters.  See Note [Type determines value]

* In a FunTy { ft_af = af }, where af = FTF_C_T or FTF_C_C,
  the argument type is always a Predicate type.