+Note [Expanding variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is another Very Important rule: if the term being matched is a
+variable, we expand it so long as its unfolding is "expandable". (Its
+occurrence information is not necessarily up to date, so we don't use
+it.) By "expandable" we mean a WHNF or a "constructor-like" application.
+This is the key reason for "constructor-like" Ids. If we have
+ {-# NOINLINE [1] CONLIKE g #-}
+ {-# RULE f (g x) = h x #-}
+then in the term
+ let v = g 3 in ....(f v)....
+we want to make the rule fire, to replace (f v) with (h 3).
+
+Note [Do not expand locally-bound variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Do *not* expand locally-bound variables, else there's a worry that the
+unfolding might mention variables that are themselves renamed.
+Example
+ case x of y { (p,q) -> ...y... }
+Don't expand 'y' to (p,q) because p,q might themselves have been
+renamed. Essentially we only expand unfoldings that are "outside"
+the entire match.
+
+Hence, (a) the guard (not (isLocallyBoundR v2))
+ (b) when we expand we nuke the renaming envt (nukeRnEnvR).
+
+Note [Notes in RULE matching]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Look through Notes in both template and expression being matched. In
+particular, we don't want to be confused by InlineMe notes. Maybe we
+should be more careful about profiling notes, but for now I'm just
+riding roughshod over them. cf Note [Notes in call patterns] in
+SpecConstr
+
+Note [Matching lets]
+~~~~~~~~~~~~~~~~~~~~
+Matching a let-expression. Consider
+ RULE forall x. f (g x) = <rhs>
+and target expression
+ f (let { w=R } in g E))
+Then we'd like the rule to match, to generate
+ let { w=R } in (\x. <rhs>) E
+In effect, we want to float the let-binding outward, to enable
+the match to happen. This is the WHOLE REASON for accumulating
+bindings in the SubstEnv
+
+We can only do this if
+ (a) Widening the scope of w does not capture any variables
+ We use a conservative test: w is not already in scope
+ If not, we clone the binders, and substitute
+ (b) The free variables of R are not bound by the part of the
+ target expression outside the let binding; e.g.
+ f (\v. let w = v+1 in g E)
+ Here we obviously cannot float the let-binding for w.
+
+You may think rule (a) would never apply, because rule matching is
+mostly invoked from the simplifier, when we have just run substExpr
+over the argument, so there will be no shadowing anyway.
+The fly in the ointment is that the forall'd variables of the
+RULE itself are considered in scope.
+
+I though of various ways to solve (a). One plan was to
+clone the binders if they are in scope. But watch out!
+ (let x=y+1 in let z=x+1 in (z,z)
+ --> should match (p,p) but watch out that
+ the use of x on z's rhs is OK!
+If we clone x, then the let-binding for 'z' is then caught by (b),
+at least unless we elaborate the RnEnv stuff a bit.
+
+So for we simply fail to match unless both (a) and (b) hold.
projects / ghc-hetmet.git / blobdiff