Note [Kind Equality Orientation]
While in theory [W] x ~ y and [W] y ~ x ought to give us the same behaviour, in practice it does not. See Note [Fundeps with instances, and equality orientation] where this is discussed at length. As a rule of thumb: we keep the newest unification variables on the left of the equality. See also Note [Improvement orientation]. In particular, `canEqCanLHSHetero` produces the following constraint equalities [X] (xi1 :: ki1) ~ (xi2 :: ki2) > [X] kco :: ki1 ~ ki2 [X] co : xi1 :: ki1 ~ (xi2 |> sym kco) :: ki1 Note that the types in the LHS of the new constraints are the ones that were on the LHS of the original constraint. Historical note --- We prevously used to flip the kco to avoid using a sym in the cast [X] (xi1 :: ki1) ~ (xi2 :: ki2) > [X] kco :: ki2 ~ ki1 [X] co : xi1 :: ki1 ~ (xi2 |> kco) :: ki1 But this sent solver in an infinite loop (see #19415). End of historical note --
References 1
- Improvement orientation GHC.Tc.Solver.Equality
Referenced by 2
- GHC.Tc.Solver.Equality call site
- GHC.Tc.Utils.Unify call site