+Note [Efficient Orientation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+There are two cases where we have to be careful about
+orienting equalities to get better efficiency.
+
+Case 2: In Rewriting Equalities (function rewriteEqLHS)
+
+ When rewriting two equalities with the same LHS:
+ (a) (tv ~ xi1)
+ (b) (tv ~ xi2)
+ We have a choice of producing work (xi1 ~ xi2) (up-to the
+ canonicalization invariants) However, to prevent the inert items
+ from getting kicked out of the inerts first, we prefer to
+ canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
+ ~ xi1) if (a) comes from the inert set.
+
+ This choice is implemented using the WhichComesFromInert flag.
+
+Case 2: In Spontaneous Solving
+ Example 2a:
+ Inerts: [w1] : D alpha
+ [w2] : C beta
+ [w3] : F alpha ~ Int
+ [w4] : H beta ~ Int
+ Untouchables = [beta]
+ Then a wanted (beta ~ alpha) comes along.
+ 1) While interacting with the inerts it is going to kick w2,w4
+ out of the inerts
+ 2) Then, it will spontaneoulsy be solved by (alpha := beta)
+ 3) Now (and here is the tricky part), to add him back as
+ solved (alpha ~ beta) is no good because, in the next
+ iteration, it will kick out w1,w3 as well so we will end up
+ with *all* the inert equalities back in the worklist!
+
+ So it is tempting to just add (beta ~ alpha) instead, that is,
+ maintain the original orietnation of the constraint.
+
+ But that does not work very well, because it may cause the
+ "double unification problem" (See Note [Avoid double unifications]).
+ For instance:
+
+ Example 2b:
+ [w1] : fsk1 ~ alpha
+ [w2] : fsk2 ~ alpha
+ ---
+ At the end of the interaction suppose we spontaneously solve alpha := fsk1
+ but keep [Given] fsk1 ~ alpha. Then, the second time around we see the
+ constraint (fsk2 ~ alpha), and we unify *again* alpha := fsk2, which is wrong.
+
+ Our conclusion is that, while in some cases (Example 2a), it makes sense to
+ preserve the original orientation, it is hard to do this in a sound way.
+ So we *don't* do this for now, @solveWithIdentity@ outputs a constraint that
+ is oriented with the unified variable on the left.
+
+Case 3: Functional Dependencies and IP improvement work
+ TODO. Optimisation not yet implemented there.
+