clarification re Note [Deeper level on the left]

[Simon Peyton Jones]

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
To: ghc-devs at haskell.org
Cc: Richard Eisenberg <rae at cs.brynmawr.edu>; Simon Peyton Jones <simonpj at microsoft.com>
Subject: clarification re Note [Deeper level on the left]

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