Note [Extending the inert equalities]

Main Theorem [Stability under extension]
   GIVEN a "work item" [lhs_w -fw-> rhs_w]
         and a terminating generalised substitution S,

   SUCH THAT
      (T1) S(fw,lhs_w) = lhs_w   -- LHS of work-item is a fixpoint of S(fw,_)
      (T2) S(fw,rhs_w) = rhs_w   -- RHS of work-item is a fixpoint of S(fw,_)
      (T3) lhs_w not in rhs_w    -- No occurs check in the work item
             If lhs is a type family application, we require only that
             lhs is not *rewritable* in rhs_w. See Note [Rewritable] and
             Note [EqCt occurs check] in GHC.Tc.Types.Constraint.
      (T4) no [lhs_s -fs-> rhs_s] in S meets [The KickOut Criteria]
           (i.e. we already kicked any such items out!)

   THEN the extended substitution T = S+(lhs_w -fw-> rhs_w)
        is a terminating generalised substitution

How do we establish these conditions?

  * (T1) and (T2) are guaranteed by exhaustively rewriting the work-item
    with S(fw,_).

  * (T3) is guaranteed by an occurs-check on the work item.
    This is done during canonicalisation, in checkTypeEq; invariant
    (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint.

  * (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable.  If the inert
    set contains a triple that meets the KickOut Criteria, we kick it out and
    add it to the work list for later re-examination.  See
    Note [The KickOut Criteria]

Theorem: T (defined in "THEN" above) is a generalised substitution;
  that is, it satisfies (WF1)-(WF3)
Proof:
  (WF1) Suppose we are adding [lhs_w -fw-> rhs_w], and [lhs_s -fs-> rhs_s] is in S.
        Then:
          - by (T1)  if fs>=fw, lhs_s does not occur within lhs_w.
          - by (KK1) if fw>=fs, lhs_w is not rewritable in lhs_s, or we'd have
            kicked out the stable constraint.

  (WF2) is directly guaranteed by (T3)

  (WF3) No lhs_s in S is rewritable in rhs_w at all, because of (T2)
        And (KK2) guarantees that lhs_w is not rewritable under a type
        family in rhs_s