Note [KK3: completeness of solving]

(KK3) is not necessary for the extended substitution
to be terminating.  In fact (KK0) could be made stronger by saying
   ... then (not (fw >= fs) or not (fs >= fs))
But it's not enough for S to be /terminating/; we also want /completeness/.
That is, we want to be able to solve all soluble wanted equalities.
Suppose we have
   work-item   b -G-> a
   inert-item  a -W-> b
Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
so we could extend the inerts, thus:
   inert-items   b -G-> a
                 a -W-> b
But if we kicked-out the inert item, we'd get
   work-item     a -W-> b
   inert-item    b -G-> a

Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
So we add one more clause (KK3) to the kick-out criteria:

    * (KK3: completeness)
      If not(fs >= fw)   (KK3a)
      * (KK3b) If the role of `fs` is Nominal:
           kick out if `rhs_s = lhs_w`
      * (KK3c) If the role of `fs` is Representational:
           kick out if `rhs_s` is of form `(lhs_w t1 .. tn)`

Wrinkles:

* (KK3a) All this can only happen if the work-item can rewrite the inert
  one, /but not vice versa/; that is not(fs >= fw).  It is useless to kick
  out if (fs >= fw) becuase then the work-item is already fully rewritten
  by the inert item.  And too much kick-out is positively harmful.
  (Historical example #14363.)

* (KK3b) addresses teh main example above for KK3. Another way to understand
  (KK3b) is that we treat an inert item
        a -f-> b
  in the same way as
        b -f-> a
  So if we kick out one, we should kick out the other.  The orientation
  is somewhat accidental.

* (KK3c) When considering roles, we also need the second clause (KK3b). Consider
      work-item    c -G/N-> a
      inert-item   a -W/R-> b c
  The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
  But we don't kick out the inert item because not (W/R >= W/R).  So we just
  add the work item. But then, consider if we hit the following:
      work-item    b -G/N-> Id
      inert-items  a -W/R-> b c
                 c -G/N-> a
    where
      newtype Id x = Id x

  For similar reasons, if we only had (KK3a), we wouldn't kick the
  representational inert out. And then, we'd miss solving the inert, which now
  reduced to reflexivity.

  The solution here is to kick out representational inerts whenever the lhs of a
  work item is "exposed", where exposed means being at the head of the top-level
  application chain (lhs t1 .. tn).  See head_is_new_lhs. This is encoded in
  (KK3c)).