Make kick-out more selective

This MR revised the crucial kick-out criteria in the constraint solver.

Ticket #24984 showed an example in which
 * We were kicking out unnecessarily
 * That gave rise to extra work, of course
 * But it /also/ led to exponentially-sized coercions due to lack
   of sharing in coercions (something we want to fix separately #20264)

This MR sharpens up the kick-out criteria; specifially in (KK2) we look
only under type family applications if (fs>=fw).

This forced me to understand the existing kick-out story, and I ended
up rewriting many of the careful Notes in GHC.Tc.Solver.InertSet.
Especially look at the new `Note [The KickOut Criteria]`

The proof of termination is not air-tight, but it is better than before,
and both Richard and I think it's correct :-).