Ha! That comment is out of date. More up to date is Note [The substitution invariant] in TyCoRep. I've updated it (and will commit in a moment) to say the stuff below.
Does that answer the question?
Simon
{- Note [The substitution invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When calling (substTy subst ty) it should be the case that
the in-scope set in the substitution is a superset of both:
(SIa) The free vars of the range of the substitution
(SIb) The free vars of ty minus the domain of the substitution
The same rules apply to other substitutions (notably CoreSubst.Subst)
* Reason for (SIa). Consider
substTy [a :-> Maybe b] (forall b. b->a)
we must rename the forall b, to get
forall b2. b2 -> Maybe b
Making 'b' part of the in-scope set forces this renaming to
take place.
* Reason for (SIb). Consider
substTy [a :-> Maybe b] (forall b. (a,b,x))
Then if we use the in-scope set {b}, satisfying (SIa), there is
a danger we will rename the forall'd variable to 'x' by mistake,
getting this:
forall x. (List b, x, x)
Breaking (SIb) caused the bug from #11371.
Note: if the free vars of the range of the substution are freshly created,
then the problems of (SIa) can't happen, and so it would be sound to
ignore (SIa).
| -----Original Message-----
| From: ghc-devs On Behalf Of Joachim
| Breitner
| Sent: 24 May 2018 13:22
| To: ghc-devs@haskell.org
| Subject: Inconsistency in CoreSubst invariant
|
| Hi,
|
| Stephanie stumbled on this apparent inconsistency in CoreSubst, about
| what ought to be in the in_scope_set of a Subst.
|
| On the one hand, the file specifies
|
| #in_scope_invariant# The in-scope set contains at least those 'Id's
| and 'TyVar's that will be in scope /after/ applying the
| substitution
| to a term. Precisely, the in-scope set must be a superset of the
| free vars of the substitution range that might possibly clash with
| locally-bound variables in the thing being substituted in.
|
| Note that the first sentence does not actually imply the second
| (unless you replace “Precisely” with “In particular”). But the comment
| even explicitly states:
|
| Make it empty, if you know that all the free vars of the
| substitution are fresh, and hence can't possibly clash
|
|
|
| Looking at the code I see that lookupIdSubst indeed expects all
| variables in either the actual substitution or in the in_scope_set:
|
| lookupIdSubst :: SDoc -> Subst -> Id -> CoreExpr
| lookupIdSubst doc (Subst in_scope ids _ _) v
| | not (isLocalId v) = Var v
| | Just e <- lookupVarEnv ids v = e
| | Just v' <- lookupInScope in_scope v = Var v'
| -- Vital! See Note [Extending the Subst]
| | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc
| <+> ppr v
| $$ ppr in_scope)
| Var v
|
| Note the warning!
|
| It seems that one of these three are true:
|
| A The invariant should be the first sentence; in particular; the
| in_scope_set contains all the free variables that are not
| substituted.
| The rest of that comment needs to be updated to reflect that.
|
| B The invariant should be the second sentence, and the WARN
| is bogus, i.e. WARNs about situations that are actually ok.
| The rest of that comment needs to be updated, and the WARN removed.
|
| C The invariant should be the second sentence, and the WARN
| is still ok there because, well, it is only a warning and only
| appears in DEBUG builds.
| The rest of that comment needs to be updated, the WARN remains.
|
| Which one is it?
|
| Cheers,
| Joachim
|
|
| --
| Joachim Breitner
| mail@joachim-breitner.de
|
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.jo
| achim-
| breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C95b44beead5a4c
| 16387908d5c170ed6c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627
| 613128370750&sdata=9%2Fz2NH8ZXH50NujT4CMx5piisF2hDRjQqJYavC%2FgLDs%3D&
| reserved=0
