| ... |
... |
@@ -365,33 +365,70 @@ Note [Shadowing in Core] |
|
365
|
365
|
You might wonder if there is an invariant that a Core expression has no
|
|
366
|
366
|
"shadowing". For example, is this illegal?
|
|
367
|
367
|
\x. \x. blah -- x is shadowed
|
|
368
|
|
-Answer; no! Core does /not/ have a no-shadowing invariant.
|
|
369
|
368
|
|
|
370
|
|
-Neither the simplifier nor any other pass GUARANTEES that shadowing is
|
|
371
|
|
-avoided. Thus, all passes SHOULD work fine even in the presence of
|
|
372
|
|
-arbitrary shadowing in their inputs.
|
|
|
369
|
+Answer:
|
|
|
370
|
+* No! Core does /not/ have a no-shadowing invariant;
|
|
|
371
|
+ That is, we allow (\x. (x, \x. x))
|
|
|
372
|
+ See the rest of this note
|
|
373
|
373
|
|
|
374
|
|
-So the Unique in a Var is not really unique at all. Still, it's very
|
|
375
|
|
-useful to give a constant-time equality/ordering for Vars, and to give
|
|
376
|
|
-a key that can be used to make sets of Vars (VarSet), or mappings from
|
|
377
|
|
-Vars to other things (VarEnv). Moreover, if you do want to eliminate
|
|
378
|
|
-shadowing, you can give a new Unique to an Id without changing its
|
|
379
|
|
-printable name, which makes debugging easier.
|
|
|
374
|
+* But Core /does/ have a no-type-shadowing invariant;
|
|
|
375
|
+ See Note [No type-shadowing in Core]
|
|
380
|
376
|
|
|
381
|
377
|
It would in many ways be easier to have a no-shadowing invariant. And the
|
|
382
|
378
|
Simplifier does its best to clone variables that are shadowed. But it is
|
|
383
|
379
|
extremely difficult to GUARANTEE it:
|
|
384
|
380
|
|
|
385
|
|
-* We use `GHC.Types.Id.mkTemplateLocal` to make up local binders, with uniques
|
|
386
|
|
- that are locally-unique (enough for the purpose) but not globally unique.
|
|
387
|
|
- It is convenient not to have to plumb a unique supply to these functions.
|
|
|
381
|
+ * We use `GHC.Types.Id.mkTemplateLocal` to make up local binders, with uniques
|
|
|
382
|
+ that are locally-unique (enough for the purpose) but not globally unique.
|
|
|
383
|
+ It is convenient not to have to plumb a unique supply to these functions.
|
|
388
|
384
|
|
|
389
|
|
-* It is very difficult for the Simplifier to gurantee a no-shadowing result.
|
|
390
|
|
- See Note [Shadowing in the Simplifier] in GHC.Core.Opt.Simplify.Iteration.
|
|
|
385
|
+ * It is very difficult for the Simplifier to gurantee a no-shadowing result.
|
|
|
386
|
+ See Note [Shadowing in the Simplifier] in GHC.Core.Opt.Simplify.Iteration.
|
|
391
|
387
|
|
|
392
|
|
-* See Note [Shadowing in CSE] in GHC.Core.Opt.CSE
|
|
|
388
|
+ * See Note [Shadowing in CSE] in GHC.Core.Opt.CSE
|
|
393
|
389
|
|
|
394
|
|
-* See Note [Shadowing in SpecConstr] in GHC.Core.Opt.SpecContr
|
|
|
390
|
+ * See Note [Shadowing in SpecConstr] in GHC.Core.Opt.SpecContr
|
|
|
391
|
+
|
|
|
392
|
+TL;DR: neither the simplifier nor any other pass GUARANTEES that shadowing is
|
|
|
393
|
+avoided. Thus, all passes MUST work fine even in the presence of arbitrary
|
|
|
394
|
+shadowing in their inputs.
|
|
|
395
|
+
|
|
|
396
|
+So the Unique in a Var is not really unique at all. Still, it's very useful to
|
|
|
397
|
+give a constant-time equality/ordering for Vars, and to give a key that can be
|
|
|
398
|
+used to make sets of Vars (VarSet), or mappings from Vars to other things
|
|
|
399
|
+(VarEnv). Moreover, if you do want to eliminate shadowing, you can give a new
|
|
|
400
|
+Unique to an Id without changing its printable name, which makes debugging
|
|
|
401
|
+easier.
|
|
|
402
|
+
|
|
|
403
|
+Note [No type-shadowing in Core]
|
|
|
404
|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
405
|
+Consider applying `exprType` to this term:
|
|
|
406
|
+
|
|
|
407
|
+ /\a. \(x::[a]). /\a. \(y::a). (x,y)
|
|
|
408
|
+
|
|
|
409
|
+where we have genuine shadowing: both lambdas bind the same a. Remember: every
|
|
|
410
|
+occurrence of `x` is just a copy of the binder (x::[a]), and ditto `y`.
|
|
|
411
|
+
|
|
|
412
|
+Now what does `exprType` return for that term? It will return the bogus type
|
|
|
413
|
+
|
|
|
414
|
+ forall a. [a] -> forall a. a -> ([a],a)
|
|
|
415
|
+
|
|
|
416
|
+whereas the correct type is: forall a. [a] -> forall b. b -> ([a],b)
|
|
|
417
|
+where we rename the inner forall.
|
|
|
418
|
+
|
|
|
419
|
+It would be /possible/ to make `exprType` more complicated, so that it does
|
|
|
420
|
+renaming on the fly. But instead we impose the no-type-shadowing invariant on
|
|
|
421
|
+Core: the variable free in an Id's type must be in scope at all that Id's
|
|
|
422
|
+occurrences. In type-system terms:
|
|
|
423
|
+
|
|
|
424
|
+ fv(t) are not bound in G2
|
|
|
425
|
+ -------------------------
|
|
|
426
|
+ G1, x:t, G2 |- x : t
|
|
|
427
|
+
|
|
|
428
|
+How do we guarntee this invariant? The main thing that might disturb it is
|
|
|
429
|
+/substitution/.
|
|
|
430
|
+
|
|
|
431
|
+ ... TODO say more here ...
|
|
395
|
432
|
|
|
396
|
433
|
Note [Core letrec invariant]
|
|
397
|
434
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|