Note [Improvement orientation]
See also Note [Fundeps with instances, and equality orientation], which describes the Exact Same Problem, with the same solution, but for functional dependencies. A very delicate point is the orientation of equalities arising from injectivity improvement (#12522). Suppose we have type family F x = t | t -> x type instance F (a, Int) = (Int, G a) where G is injective; and wanted constraints [W] F (alpha, beta) ~ (Int, <some type>) The injectivity will give rise to constraints [W] gamma1 ~ alpha [W] Int ~ beta The fresh unification variable gamma1 comes from the fact that we can only do "partial improvement" here; see Section 5.2 of "Injective type families for Haskell" (HS'15). Now, it's very important to orient the equations this way round, so that the fresh unification variable will be eliminated in favour of alpha. If we instead had [W] alpha ~ gamma1 then we would unify alpha := gamma1; and kick out the wanted constraint. But when we substitute it back in, it'd look like [W] F (gamma1, beta) ~ fuv and exactly the same thing would happen again! Infinite loop. This all seems fragile, and it might seem more robust to avoid introducing gamma1 in the first place, in the case where the actual argument (alpha, beta) partly matches the improvement template. But that's a bit tricky, esp when we remember that the kinds much match too; so it's easier to let the normal machinery handle it. Instead we are careful to orient the new equality with the template on the left. Delicate, but it works.
References 1
- Fundeps with instances, and equality orientation GHC.Tc.Solver.Dict
Referenced by 5
- Fundeps with instances, and equality orientation GHC.Tc.Solver.Dict ×2
- Kind Equality Orientation GHC.Tc.Solver.Equality
- GHC.Tc.Solver.Equality call site
- unifyFunDeps GHC.Tc.Solver.Monad