Inconsistency in CoreSubst invariant

[Simon Peyton Jones]

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 <ghc-devs-bounces at haskell.org> On Behalf Of Joachim
|  Breitner
|  Sent: 24 May 2018 13:22
|  To: ghc-devs at 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 at 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