Note [Canonical equalities]

An EqCt is a canonical equality constraint, one that can live in the inert set,
and that can be used to rewrite other constraints. It satisfies these invariants:

  * (TyEq:OC) lhs does not occur in rhs (occurs check)
              Note [EqCt occurs check]

  * (TyEq:F) rhs has no foralls
      (this avoids substituting a forall for the tyvar in other types)

  * (TyEq:K) typeKind lhs `tcEqKind` typeKind rhs; Note [Ct kind invariant]

  * (TyEq:N) If the equality is representational, rhs is not headed by a saturated
    application of a newtype TyCon. See GHC.Tc.Solver.Equality
    Note [No top-level newtypes on RHS of representational equalities].
    (Applies only when constructor of newtype is in scope.)

  * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we
    will not form an EqCt (a ~ ty).

  * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up
    a hetero-kinded equality.  See Note [Equalities with heterogeneous kinds] in
    GHC.Tc.Solver.Equality, wrinkle (EIK2)

These invariants ensure that the EqCts in inert_eqs constitute a terminating
generalised substitution. See Note [inert_eqs: the inert equalities]
in GHC.Tc.Solver.InertSet for what these words mean!