Note [Kind Equality Orientation]

GHC/Tc/Solver/Equality.hs:1642 compiler 1 ticket

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

Referenced by 2