Note [Deeper level on the left]
The most important thing is that we want to put tyvars with
the deepest level on the left. The reason to do so differs for
Wanteds and Givens, but either way, deepest wins! Simple.
* Wanteds. Putting the deepest variable on the left maximise the
chances that it's a touchable meta-tyvar which can be solved.
* Givens. Suppose we have something like
forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]
If we orient the Given a[2] on the left, we'll rewrite the Wanted to
(beta[1] ~ b[1]), and that can float out of the implication.
Otherwise it can't. By putting the deepest variable on the left
we maximise our changes of eliminating skolem capture.
See also GHC.Tc.Solver.InertSet Note [Let-bound skolems] for another reason
to orient with the deepest skolem on the left.
IMPORTANT NOTE: this test does a level-number comparison on
skolems, so it's important that skolems have (accurate) level
numbers.
See #15009 for an further analysis of why "deepest on the left"
is a good plan. References 1
- Let-bound skolems GHC.Tc.Solver.InertSet
Referenced by 3
- Let-bound skolems GHC.Tc.Solver.InertSet
- GHC.Tc.Utils.TcType call site
- TyVar/TyVar orientation GHC.Tc.Utils.Unify