De-duplicate overlapping Noteswip/T17827

Documentation only.  Fixes #17827

2 files changed, 26 insertions, 44 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 96f4b3fa0d..982a4fc395 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -2152,36 +2152,8 @@ canEqReflexive ev eq_rel ty
                                mkTcReflCo (eqRelRole eq_rel) ty)
        ; stopWith ev "Solved by reflexivity" }
 
-{-
-Note [Canonical orientation for tyvar/tyvar equality constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
-round should be oriented in the CTyEqCan?  The rules, implemented by
-canEqTyVarTyVar, are these
-
- * If either is a flatten-meta-variables, it goes on the left.
-
- * Put a meta-tyvar on the left if possible
-       alpha[3] ~ r
-
- * If both are meta-tyvars, put the more touchable one (deepest level
-   number) on the left, so there is the best chance of unifying it
-        alpha[3] ~ beta[2]
-
- * If both are meta-tyvars and both at the same level, put a TyVarTv
-   on the right if possible
-        alpha[2] ~ beta[2](sig-tv)
-   That way, when we unify alpha := beta, we don't lose the TyVarTv flag.
-
- * Put a meta-tv with a System Name on the left if possible so it
-   gets eliminated (improves error messages)
-
- * If one is a flatten-skolem, put it on the left so that it is
-   substituted out  Note [Eliminate flat-skols] in TcUinfy
-        fsk ~ a
-
-Note [Equalities with incompatible kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Equalities with incompatible kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 What do we do when we have an equality
 
   (tv :: k1) ~ (rhs :: k2)
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index b5bffb3bf2..371cb9e108 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1768,6 +1768,10 @@ lhsPriority tv
 Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)?
 This is a surprisingly tricky question!
 
+The question is answered by swapOverTyVars, which is use
+  - in the eager unifier, in TcUnify.uUnfilledVar1
+  - in the constraint solver, in TcCanonical.canEqTyVarHomo
+
 First note: only swap if you have to!
    See Note [Avoid unnecessary swaps]
 
@@ -1777,25 +1781,31 @@ So we look for a positive reason to swap, using a three-step test:
   put 'a' on the left.  See Note [Deeper level on the left]
 
 * Priority.  If the levels are the same, look at what kind of
-  type variable it is, using 'lhsPriority'
+  type variable it is, using 'lhsPriority'.
+
+  Generally speaking we always try to put a MetaTv on the left
+  in preference to SkolemTv or RuntimeUnkTv:
+     a) Because the MetaTv may be touchable and can be unified
+     b) Even if it's not touchable, TcSimplify.floatEqualities
+        looks for meta tyvars on the left
 
-  - FlatMetaTv: Always put on the left.
-    See Note [Fmv Orientation Invariant]
-    NB: FlatMetaTvs always have the current level, never an
-        outer one.  So nothing can be deeper than a FlatMetaTv
+  Tie-breaking rules for MetaTvs:
+  - FlatMetaTv = 4: always put on the left.
+        See Note [Fmv Orientation Invariant]
 
+        NB: FlatMetaTvs always have the current level, never an
+        outer one.  So nothing can be deeper than a FlatMetaTv.
 
-  - TyVarTv/TauTv: if we have  tyv_tv ~ tau_tv, put tau_tv
-                   on the left because there are fewer
-                   restrictions on updating TauTvs
+  - TauTv = 3: if we have  tyv_tv ~ tau_tv,
+       put tau_tv on the left because there are fewer
+       restrictions on updating TauTvs.  Or to say it another
+       way, then we won't lose the TyVarTv flag
 
-  - TyVarTv/TauTv:  put on the left either
-     a) Because it's touchable and can be unified, or
-     b) Even if it's not touchable, TcSimplify.floatEqualities
-        looks for meta tyvars on the left
+  - TyVarTv = 2: remember, flat-skols are *only* updated by
+       the unflattener, never unified, so TyVarTvs come next
 
-  - FlatSkolTv: Put on the left in preference to a SkolemTv
-                See Note [Eliminate flat-skols]
+  - FlatSkolTv = 1: put on the left in preference to a SkolemTv.
+       See Note [Eliminate flat-skols]
 
 * Names. If the level and priority comparisons are all
   equal, try to eliminate a TyVars with a System Name in