Inconsistency in CoreSubst invariant

Joachim Breitner mail at joachim-breitner.de
Thu May 24 12:21:33 UTC 2018


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
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180524/5590e764/attachment.sig>


More information about the ghc-devs mailing list