Note [Unify only if the rewriter set is empty]

GHC/Tc/Solver/Equality.hs:2858 compiler

Consider
    co (rewriters = {co1,co2}) :: alpha ~# blah
If we unify before solving `co1` and `co2` (which might well be insoluble)
we destroy the careful tracking of Note [Wanteds rewrite Wanteds] in
GHC.Tc.Types.Constraint.  So we decline to unify any equality with a
non-empty rewriter set: see (REWRITERS) in Note [Unification preconditions]
in GHC.Tc.Utils.

Wrinkles:

(URW1) We may, however, be willing to /default/ such an equality; see
   (DE6) in Note [Defaulting equalities] in GHC.Tc.Solver.Default.

(URW2) If we have `co` in the inert set, and we solve `co1` and `co2`,
   we should kick out `co` so that we can now unify it, which might
   unlock other stuff.  See `kickOutAfterFillingCoercionHole` in
   GHC.Tc.Solver.Monad.

   However the solver prioritises equalities with an empty rewriter
   set, to try to avoid unnecessary kick-out.  See GHC.Tc.Types.Constraint
   Note [Prioritise Wanteds with empty RewriterSet] esp (PER1)

References 4

Referenced by 4