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