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.