Note [Put touchable variables on the left]
Ticket #10009, a very nasty example: f :: (UnF (F b) ~ b) => F b -> () g :: forall a. (UnF (F a) ~ a) => a -> () g _ = f (undefined :: F a) For g we get [G] g1 : UnF (F a) ~ a [W] w1 : UnF (F beta) ~ beta [W] w2 : F a ~ F beta g1 is canonical (CEqCan). It is oriented as above because a is not touchable. See canEqTyVarFunEq. w1 is similarly canonical, though the occurs-check in canEqTyVarFunEq is key here. w2 is canonical. But which way should it be oriented? As written, we'll be stuck. When w2 is added to the inert set, nothing gets kicked out: g1 is a Given (and Wanteds don't rewrite Givens), and w2 doesn't mention the LHS of w2. We'll thus lose. But if w2 is swapped around, to [W] w3 : F beta ~ F a then we'll kick w1 out of the inert set (it mentions the LHS of w3). We then rewrite w1 to [W] w4 : UnF (F a) ~ beta and then, using g1, to [W] w5 : a ~ beta at which point we can unify and go on to glory. (This rewriting actually happens all at once, in the call to rewrite during canonicalisation.) But what about the new LHS makes it better? It mentions a variable (beta) that can appear in a Wanted -- a touchable metavariable never appears in a Given. On the other hand, the original LHS mentioned only variables that appear in Givens. We thus choose to put variables that can appear in Wanteds on the left. Ticket #12526 is another good example of this in action.
References 0
This Note does not link to any other.
Referenced by 2
- GHC.Tc.Solver.Equality call site
- Orienting TyFamLHS/TyFamLHS GHC.Tc.Solver.Equality