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
Sent: 16 May 2019 06:03
To: ghc-devs@haskell.org
Cc: Richard Eisenberg ; Simon Peyton Jones
Subject: clarification re Note [Deeper level on the left]
https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcUnify.hs...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fblob%2Fmaster%2Fcompiler%2Ftypecheck%2FTcUnify.hs%23L1754&data=02%7C01%7Csimonpj%40microsoft.com%7Cfd5cf759668242dc797f08d6d9bbddb8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636935798235607415&sdata=cRksGeyxgGtNkWOf7nuF42BruMVyK8JyqbbAZC02DJM%3D&reserved=0 contains
```
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.
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
