clarification re Note [Deeper level on the left]

[Nicolas Frisby]

https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcUnify.hs#L1754
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190515/3e437d89/attachment.html>