Inconsistent tidying of implications

Consider this program (tcfail013)

f [] = 1
f True = 2

We get the unsolved implication

  Wanted: WC {wc_impl =
                Implic {
                  TcLevel = 1
                  Skolems = a_aur[sk:1] a_axQ[sk:1]
                  Given-eqs = NoGivenEqs
                  Status = Insoluble
                  Given =
                  Wanted =
                    WC {wc_simple =
                          [WD] hole{co_axS} {0}:: Bool ~# [a_aur[sk:1]] (CIrredCan(shape))
                          [WD] $dNum_axR {0}:: Num a_axQ[sk:1] (CDictCan(psc))}
                  Binds = EvBindsVar<axY>
                  the inferred type of f :: [a_aur[sk:1]] -> a_axQ[sk:1] }}

Note that the two skolems have the same OccName, namely a. (They both started life as unification variablex, which we generalised.)

When we tidy the skolems we get

reportImplic
  Implic {
    TcLevel = 1
    Skolems = a_auG[sk:1] a1_ay2[sk:1]
    Given-eqs = NoGivenEqs
    Status = Insoluble
    Given =
    Wanted =
      WC {wc_simple =
            [WD] hole{co_ay4} {0}:: Bool
                                    GHC.Prim.~# [a_auG[sk:1]] (CIrredCan(shape))
            [WD] $dNum_ay3 {0}:: Num a_ay2[sk:1] (CDictCan(psc))}
    Binds = EvBindsVar<ay9>
    the inferred type of f :: [a_auG[sk:1]] -> a1_ay2[sk:1] }

We have tidied one a to a, and the other to a1. This flat-out contradicts Note [Tidying multiple names at once] in GHC.Types.Names.Occurrence in GHC.Types.Names.Occurrence, where we say that we should not accidentally privilege one of these 'a's over the others.

The reason we don't follow the standard guidance is that in reportImplic we have

    (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
                   scopedSort tvs

If instead we had

    (env1, tvs') = tidyVarBndrs (cec_tidy ctxt) $
                   scopedSort tvs

then tidyVarBndrs would do the symmetric thing. In our example we'd tidy to a1 and a2.

I think we should do the symmetric thing. But we get a couple of dozen regression failures, as error messages wibble around. Task: make the change, check the changes, and accept them.

The status quo seems wrong to me.