Note [KK2: termination of the extended substitution]

Proving termination of the extended substitution T is surprisingly tricky.

* Reason for (KK2a).  Consider
      Work:  [G] b ~ a
      Inert: [W] a ~ b
  If we don't kick out the inert, then we get a loop on e.g. [W] a ~ Int.
  But if both were Wanted we really should not kick out (the substitution does not
  have to be idempotent). So we only look everywhere for the `lhs_w` if
  not (fs>=fw), that is the inert item cannot rewrite the work item.  So in the
  above example we will kick out; but if both were Wanted we won't.

* Reason for (KK2b).  Consider the case where (fs >= fw)
      Work:  [G] a ~ Int
      Inert: [G] F Int ~ F a
  If we just added the work item, the substitution would loop on type (F Int).
  So we must kick out the inert item, even though (fs>=fw). (KK2b) does this
  by looking for lhs_w under type family applications in rhs_s.

  (KK2b) makes kick-out less aggressive by looking only under type-family applications,
  in the case where (fs >= fw), and that made a /huge/ difference to #24944.

Tricky examples in: #19042, #17672, #24984. The last (#24984) is particular subtle:

  Inert:   [W] g1: F a0 ~ F a1
           [W] g2: F a2 ~ F a1
           [W] g3: F a3 ~ F a1

Now we add [W] g4: F a1 ~ F a7.  Should we kick out g1,g2,g3?  No!  The
substitution doesn't need to be idempotent, merely terminating.  And in #24984
it turned out that we kept adding one new constraint and kicking out all the
previous inert ones (and that rewriting led to exponentially big constraints due
to lack of contraint sharing.)  So we only want to look /under/ type family applications.

The proof is hard. We start by ignoring flavours. Suppose that:
* We are adding [lhs_w -fw-> rhs_w] to a well-formed, terminating substitution S.
* None of the constraints in S meet the KickOut Criteria.
* Define T = S+[lhs_w -fw-> rhs_w]
* `f` is an arbitrary flavour

Lemma 1: for any lhs_s in S, T*(f,lhs_s) terminates.
  Proof.
  * We know that r1 = S*(f,lhs_s) terminates.
  * Moreover, we know there are no occurrences of lhs_w under a type family (which
    is the head of a LHS) in r1 (KK2)+(WF3).  We need (WF3) because you might wonder
    what if rhs_s is (F a), and [a --> lhs_w] was in S.  But (WF3) prevents that.
  * Define r2 = r1{rhs_w/lhs_w}.  We know that rhs_w has no occurrences of any lhs in S,
    nor of lhs_w.
  * Since any occurrence of lhs_w does not occur under a type family, the substitution
    won't make any F t1..tn ~ s in S match.
  * So r2 is a fixed point of T.

Lemma 2: T*(f,lhs_w) teminates.
  Proof: no occurrences of any LHS in rhs_w.

Theorem. For any type r, T*(r) terminates.
  Proof:
  1. Consider any sub-term of r, which is a LHS of T.
     - Rewrite it with T*; this terminates (Lemma 1).
     - Do this simultaneously to all sub-terms that match a LHS of T, yielding r1.
  2. Could this new r1 have a sub-term that is an LHS of T?  Yes, but only if r has a
     sub-term F w, and w rewrote in Step 1 to w' and F w' matches a LHS in T.
  3. Very well: apply step 1 again, but note that /doing so consumes one of the family
     applications in the original r/.
  4. After Step 1 either we have reached a fixed point, or we repeat Step 1 consuming at
     least one family application of r.
  5. There are only a finite number of family applications in r, so this process terminates.

Example:

Inert set:   gs : F Int ~ b
Work item:   gw : b ~ Int

F (F (F b)) --[gw]--> F (F (F Int)) --[gs]--> F (F b)
            [gw]--> F (F Int)     --[gs]--> F b
            [gw]--> F Int         --[gs]--> b
            [gw]--> Int

Notice that each iteration of Step 1 strips off one of the layers of F, all
of which were in the original r.

The argument is even more tricky when flavours are involved, and we have not
fleshed it out in detail.