# clarification re Note [Deeper level on the left]

Simon Peyton Jones simonpj at microsoft.com
Thu May 16 08:05:54 UTC 2019

```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.

Consider our example

forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]

If we leave the Given oriented as it is, the (beta~a) constraint cannot float, because it mentions a, which is bound by the forall

If we swizzle the Given we get this:

forall a[2]. a[2] ~ b[1] => beta[1] ~ a[2]

Now we’ll use that Given to rewrite the Wanted, to get this:

forall a[2]. a[2] ~ b[1] => beta[1] ~ b[1]

Now the Wanted can float – it no longer mentions a.

But wait!  There’s a second thing that prevents floating: we never float out of an implication that binds Given equalities.   But not quite: the Note [Let-bound skolems] explains that we don’t treat as “binding a Given equality” an equality whose LHS is one of the skolems bound by this very implication.  And lo!  in the implication

forall a[2]. a[2] ~ b[1] => beta[1] ~ b[1]

the a[2] on the LHS is indeed bound by this implication.  So we do not disable floating (despite the apparent Given equality), and can float to give

beta[1] ~ b[1],  (forall a[2]. a[2] ~ b[1] => <empty>)

Does that help explain? If so, might you update the Note(s) so they are clearer?

Thanks

Simon

rom: Nicolas Frisby <nicolas.frisby at gmail.com>
Sent: 16 May 2019 06:03
Cc: Richard Eisenberg <rae at cs.brynmawr.edu>; Simon Peyton Jones <simonpj at microsoft.com>
Subject: clarification re Note [Deeper level on the left]

```

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.

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...