Note [Prioritise equalities]
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
- Decomposing newtype equalities GHC.Tc.Solver.Equality
- Prioritise class equalities GHC.Tc.Solver.InertSet
- Wanteds rewrite Wanteds GHC.Tc.Types.Constraint
Referenced by 4
- Decomposing newtype equalities GHC.Tc.Solver.Equality
- WorkList priorities GHC.Tc.Solver.InertSet
- GHC.Tc.Solver.InertSet call site
- GHC.Tc.Solver.Monad call site