Inconsistency in CoreSubst invariant

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Inconsistency in CoreSubst invariant

Joachim Breitner-2
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
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Inconsistency in CoreSubst invariant

Richard Eisenberg-4


> On May 24, 2018, at 8:21 AM, Joachim Breitner <[hidden email]> wrote:
>
> Which one is it?

See Note [The substitution invariant] in TyCoRep. That applies to types, not terms, but I'd be shocked if terms had a different situation. That would suggest that the answer is (A) (and that the WARNing is correct).

Richard

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Inconsistency in CoreSubst invariant

GHC - devs mailing list
In reply to this post by Joachim Breitner-2
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 <[hidden email]> On Behalf Of Joachim
|  Breitner
|  Sent: 24 May 2018 13:22
|  To: [hidden email]
|  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
|    [hidden email]
|  
|  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
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Inconsistency in CoreSubst invariant

Joachim Breitner-2
Hi,

Am Freitag, den 25.05.2018, 11:33 +0000 schrieb 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?

indeed it does!

Thanks,
Joachim
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (849 bytes) Download Attachment