Note [Prioritise equalities]

GHC/Tc/Solver/InertSet.hs:103 compiler 1 ticket

It's very important to process equalities over class constraints:

* (Efficiency)  The general reason to do so is that if we process a
  class constraint first, we may end up putting it into the inert set
  and then kicking it out later.  That's extra work compared to just
  doing the equality first.

* (Avoiding fundep iteration) As #14723 showed, it's possible to
  get non-termination if we
      - Emit the fundep equalities for a class constraint,
        generating some fresh unification variables.
      - That leads to some unification
      - Which kicks out the class constraint
      - Which isn't solved (because there are still some more
        equalities in the work-list), but generates yet more fundeps
  Solution: prioritise equalities over class constraints

* (Class equalities) We need to prioritise equalities even if they
  are hidden inside a class constraint; see Note [Prioritise class equalities]

* (Kick-out) We want to apply this priority scheme to kicked-out
  constraints too (see the call to extendWorkListCt in kick_out_rewritable)
  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
  homo-kinded when kicked out, and hence we want to prioritise it.

Further refinements:

* Among the equalities we prioritise ones with an empty rewriter set;
  see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint, wrinkle (W1).

* Among equalities with an empty rewriter set, we prioritise nominal equalities.
   * They have more rewriting power, so doing them first is better.
   * Prioritising them ameliorates the incompleteness of newtype
     solving: see (Ex2) in Note [Decomposing newtype equalities] in
     GHC.Tc.Solver.Equality.

References 3

Referenced by 4