Note [The KickOut Criteria]

Kicking out is a Bad Thing:
* It means we have to re-process a constraint.  The less we kick out, the better.
* In the limit, kicking can lead to non-termination: imagine that we /always/
  kick out the entire inert set!
* Because (mid 2024) we don't support sharing in constraints, excessive kicking out
  can lead to exponentially big constraints (#24984).

So we seek to do as little kicking out as possible.  For example, consider this,
which happens a lot:

   Inert:  g1: a ~ Maybe b
   Work:   g2: b ~ Int

We do /not/ kick out g1 when adding g2.  The new substitution S' = {g1,g2} is still
/terminating/ but it is not /idmempotent/.  To apply S' to, say, (Tree a), we may
need to apply it twice:  Tree a --> Tree (Maybe b) --> Tree (Maybe Int)

Here are the KickOut Criteria:

    When adding [lhs_w -fw-> rhs_w] to a well-formed terminating substitution S,
    element [lhs_s -fs-> rhs_s] in S meets the KickOut Criteria if:

    (KK0) fw >= fs    AND   any of (KK1), (KK2) or (KK3) hold

    * (KK1: satisfy WF1) `lhs_w` is rewritable in `lhs_s`.

    * (KK2: termination) `lhs_w` is rewritable in `rhs_s` in these positions:
        If not(fs>=fw)
        then (KK2a) anywhere
        else (KK2b) look only in the argument of type family applications,
                    whose type family heads some LHS in `S`

    * (KK3: completeness)
      If not(fs >= fw)   -- If fs can rewrite fw, kick-out is redundant/harmful
      * (KK3a) If the role of `fs` is Nominal:
           kick out if `rhs_s = lhs_w`
      * (KK3b) If the role of `fs` is Representational:
           kick out if `rhs_s` is of form `(lhs_w t1 .. tn)`

Rationale

* (KK0) kick out only if `fw` can rewrite `fs`.
  Reason: suppose we kick out (lhs1 -fs-> s), and add (lhs -fw-> t) to the ineart
  set. The latter can't rewrite the former, so the kick-out achieved nothing

* (KK1) `lhs_w` is rewritable in `lhs_s`.
  Reason: needed to guarantee (WF1).  See Theorem: T is well formed

* (KK2) see Note [KK2: termination of the extended substitution]

* (KK3) see Note [KK3: completeness of solving]

The above story is a bit vague wrt roles, but the code is not.
See Note [Flavours with roles]