From 5be9a0cb92fa806a5987c9548861ea73c9feab42 Mon Sep 17 00:00:00 2001 From: Ben Gamari Date: Tue, 22 Feb 2022 21:29:18 -0500 Subject: simplCore: Correctly extend in-scope set in rule matching Note [Matching lets] in GHC.Core.Rules claims the following: > We use GHC.Core.Subst.substBind to freshen the binding, using an > in-scope set that is the original in-scope variables plus the > rs_bndrs (currently floated let-bindings). However, previously the implementation didn't actually do extend the in-scope set with rs_bndrs. This appears to be a regression which was introduced by 4ff4d434e9a90623afce00b43e2a5a1ccbdb4c05. Moreover, the originally reasoning was subtly wrong: we must rather use the in-scope set from rv_lcl, extended with rs_bndrs, not that of `rv_fltR` Fixes #21122. --- compiler/GHC/Core/Rules.hs | 72 ++++++++++++++++++++++++++++++---------------- 1 file changed, 47 insertions(+), 25 deletions(-) diff --git a/compiler/GHC/Core/Rules.hs b/compiler/GHC/Core/Rules.hs index 9a1db01c2a..a365b838c4 100644 --- a/compiler/GHC/Core/Rules.hs +++ b/compiler/GHC/Core/Rules.hs @@ -703,6 +703,8 @@ data RuleMatchEnv , rv_fltR :: Subst -- Renamings for floated let-bindings -- (domain disjoint from envR of rv_lcl) -- See Note [Matching lets] + -- N.B. The InScopeSet of rv_fltR is always ignored; + -- see (4) in Note [Matching lets]. , rv_unf :: IdUnfoldingFun } @@ -959,7 +961,10 @@ match renv subst e1 (Let bind e2) mco | otherwise = Nothing where - (flt_subst', bind') = substBind (rv_fltR renv) bind + in_scope = rnInScopeSet (rv_lcl renv) `extendInScopeSetList` rs_bndrs subst + -- in_scope: see (4) in Note [Matching lets] + flt_subst = rv_fltR renv `setInScope` in_scope + (flt_subst', bind') = substBind flt_subst bind new_bndrs = bindersOf bind' ------------------------ Lambdas --------------------- @@ -1319,7 +1324,6 @@ Hence, (a) the guard (not (isLocallyBoundR v2)) Note [Tick annotations in RULE matching] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - We used to unconditionally look through ticks in both template and expression being matched. This is actually illegal for counting or cost-centre-scoped ticks, because we have no place to put them without @@ -1336,6 +1340,7 @@ GHC.Core.Opt.Simplify.Utils for details. cf Note [Tick annotations in call patterns] in GHC.Core.Opt.SpecConstr + Note [Matching lets] ~~~~~~~~~~~~~~~~~~~~ Matching a let-expression. Consider @@ -1354,38 +1359,55 @@ part of the target expression outside the let binding; e.g. Here we obviously cannot float the let-binding for w. Hence the use of okToFloat. -There are a couple of tricky points. - (a) What if floating the binding captures a variable? +There are a couple of tricky points: + (a) What if floating the binding captures a variable that is + free in the entire expression? f (let v = x+1 in v) v --> NOT! let v = x+1 in f (x+1) v - (b) What if two non-nested let bindings bind the same variable? + (b) What if the let shadows a local binding? + f (\v -> (v, let v = x+1 in (v,v)) + --> NOT! + let v = x+1 in f (\v -> (v, (v,v))) + + (c) What if two non-nested let bindings bind the same variable? f (let v = e1 in b1) (let v = e2 in b2) --> NOT! let v = e1 in let v = e2 in (f b2 b2) - See testsuite test "T4814". + See testsuite test `T4814`. Our cunning plan is this: - * Along with the growing substitution for template variables - we maintain a growing set of floated let-bindings (rs_binds) - plus the set of variables thus bound (rs_bndrs). - - * The RnEnv2 in the MatchEnv binds only the local binders - in the term (lambdas, case), not the floated let-bndrs. - - * When we encounter a let in the term to be matched, we use - okToFloat check that does not mention any locally bound (lambda, - case) variables. If so we fail. - - * We use GHC.Core.Subst.substBind to freshen the binding, using an - in-scope set that is the original in-scope variables plus the - rs_bndrs (currently floated let-bindings). So in (a) above - we'll freshen the 'v' binding; in (b) above we'll freshen - the *second* 'v' binding. - - * We apply that freshening substitution, in a lexically-scoped - way to the term, although lazily; this is the rv_fltR field. + (1) Along with the growing substitution for template variables + we maintain a growing set of floated let-bindings (rs_binds) + plus the set of variables thus bound (rs_bndrs). + + (2) The RnEnv2 in the MatchEnv binds only the local binders + in the term (lambdas, case), not the floated let-bndrs. + + (3) When we encounter a `let` in the term to be matched, in the Let + case of `match`, we use `okToFloat` to check that it does not mention any + locally bound (lambda, case) variables. If so we fail. + + (4) In the Let case of `match`, we use GHC.Core.Subst.substBind to + freshen the binding (which, remember (3), mentions no locally + bound variables), in a lexically-scoped way (via rv_fltR in + MatchEnv). + + The subtle point is that we want an in-scope set for this + substitution that includes /two/ sets: + * The in-scope variables at this point, so that we avoid using + those local names for the floated binding; points (a) and (b) above. + * All "earlier" floated bindings, so that we avoid using the + same name for two different floated bindings; point (c) above. + + Because we have to compute the in-scope set here, the in-scope set + stored in `rv_fltR` is always ignored; we leave it only because it's + convenient to have `rv_fltR :: Subst` (with an always-ignored `InScopeSet`) + rather than storing three separate substitutions. + + (5) We apply that freshening substitution, in a lexically-scoped + way to the term, although lazily; this is the rv_fltR field. See #4814, which is an issue resulting from getting this wrong. -- cgit v1.2.1