Note [Unify only if the rewriter set is empty]
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
- Defaulting equalities GHC.Tc.Solver.Default
- Prioritise Wanteds with empty RewriterSet GHC.Tc.Types.Constraint
- Wanteds rewrite Wanteds GHC.Tc.Types.Constraint
- Unification preconditions GHC.Tc.Utils.Unify
Referenced by 4
- Defaulting equalities GHC.Tc.Solver.Default
- GHC.Tc.Solver.Equality call site
- Equalities with heterogeneous kinds GHC.Tc.Solver.Equality
- GHC.Tc.Solver.Monad call site