Commit a9e9d18f authored by Simon Peyton Jones's avatar Simon Peyton Jones

De-duplicate overlapping Notes

Documentation only.  Fixes #17827
parent 6c2585e0
......@@ -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)
......
......@@ -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
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment