<div dir="ltr"><div dir="ltr"><a href="https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcUnify.hs#L1754">https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcUnify.hs#L1754</a> contains</div><div dir="ltr"><br></div><div dir="ltr"><pre class="gmail-code gmail-highlight" lang="haskell"><span id="gmail-LC1754" class="gmail-line gmail-hll" lang="haskell"><span class="gmail-cm">```
Note [Deeper level on the left]</span></span>
<span id="gmail-LC1755" class="gmail-line" lang="haskell"><span class="gmail-cm">~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~</span></span>
<span id="gmail-LC1756" class="gmail-line" lang="haskell"><span class="gmail-cm">The most important thing is that we want to put tyvars with</span></span>
<span id="gmail-LC1757" class="gmail-line" lang="haskell"><span class="gmail-cm">the deepest level on the left.  The reason to do so differs for</span></span>
<span id="gmail-LC1758" class="gmail-line" lang="haskell"><span class="gmail-cm">Wanteds and Givens, but either way, deepest wins!  Simple.</span></span>
<span id="gmail-LC1759" class="gmail-line" lang="haskell"></span>
<span id="gmail-LC1760" class="gmail-line" lang="haskell"><span class="gmail-cm">* Wanteds.  Putting the deepest variable on the left maximise the</span></span>
<span id="gmail-LC1761" class="gmail-line" lang="haskell"><span class="gmail-cm">  chances that it's a touchable meta-tyvar which can be solved.</span></span>
<span id="gmail-LC1762" class="gmail-line" lang="haskell"></span>
<span id="gmail-LC1763" class="gmail-line" lang="haskell"><span class="gmail-cm">* Givens. Suppose we have something like</span></span>
<span id="gmail-LC1764" class="gmail-line" lang="haskell"><span class="gmail-cm">     forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]</span></span>
<span id="gmail-LC1765" class="gmail-line" lang="haskell"></span>
<span id="gmail-LC1766" class="gmail-line" lang="haskell"><span class="gmail-cm">  If we orient the Given a[2] on the left, we'll rewrite the Wanted to</span></span>
<span id="gmail-LC1767" class="gmail-line" lang="haskell"><span class="gmail-cm">  (beta[1] ~ b[1]), and that can float out of the implication.</span></span>
<span id="gmail-LC1768" class="gmail-line" lang="haskell"><span class="gmail-cm">  Otherwise it can't.  By putting the deepest variable on the left</span></span>
<span id="gmail-LC1769" class="gmail-line" lang="haskell"><span class="gmail-cm">  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.
<pre class="gmail-code gmail-highlight" lang="haskell"><span id="gmail-LC1774" class="gmail-line" lang="haskell"><span class="gmail-cm">  IMPORTANT NOTE: this test does a level-number comparison on</span></span>
<span id="gmail-LC1775" class="gmail-line" lang="haskell"><span class="gmail-cm">  skolems, so it's important that skolems have (accurate) level</span></span>
<span id="gmail-LC1776" class="gmail-line" lang="haskell"><span class="gmail-cm">  numbers.</span></span>
<span id="gmail-LC1777" class="gmail-line" lang="haskell"></span>
<span id="gmail-LC1778" class="gmail-line" lang="haskell"><span class="gmail-cm">See #15009 for an further analysis of why "deepest on the left"</span></span>
<span id="gmail-LC1779" class="gmail-line" lang="haskell"><span class="gmail-cm">is a good plan.
</span></span>```</pre></span></span>
<div style="font-family:Arial,Helvetica,sans-serif;white-space:normal">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.</div><div style="font-family:Arial,Helvetica,sans-serif;white-space:normal"><br></div><div style="font-family:Arial,Helvetica,sans-serif;white-space:normal">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.<br><br>Thanks. -Nick<br></div></pre></div></div>