https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcUnify.hs... contains ``` Note [Deeper level on the left]~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~The most important thing is that we want to put tyvars withthe deepest level on the left. The reason to do so differs forWanteds 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 TcSMonad 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.``` I'm wondering about the claim "and that can float out of the implication". The Note does go on to mention #15009 --- and I understand how that Wanted floats *with* #15009 --- but as written, it sounds like the Wanted could float even without #15009. Am I missing something? Roughly: I'm asking because I need to decide if there's a reason for my typechecker plugin to bother with "eliminating skolem capture" when #15009 does *not* apply. Thanks. -Nick