+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.
+
+Other cases to think about
+ (let x=y+1 in \x. (x,x))
+ --> let x=y+1 in (\x1. (x1,x1))
+ (\x. let x = y+1 in (x,x))
+ --> let x1 = y+1 in (\x. (x1,x1)
+ (let x=y+1 in (x,x), let x=y-1 in (x,x))
+ --> let x=y+1 in let x1=y-1 in ((x,x),(x1,x1))
+
+Note [Matching cases]
+~~~~~~~~~~~~~~~~~~~~~
+{- NOTE: This idea is currently disabled. It really only works if
+ the primops involved are OkForSpeculation, and, since
+ they have side effects readIntOfAddr and touch are not.
+ Maybe we'll get back to this later . -}
+
+Consider
+ f (case readIntOffAddr# p# i# realWorld# of { (# s#, n# #) ->
+ case touch# fp s# of { _ ->
+ I# n# } } )
+This happened in a tight loop generated by stream fusion that
+Roman encountered. We'd like to treat this just like the let
+case, because the primops concerned are ok-for-speculation.
+That is, we'd like to behave as if it had been
+ case readIntOffAddr# p# i# realWorld# of { (# s#, n# #) ->
+ case touch# fp s# of { _ ->
+ f (I# n# } } )
+
+Note [Lookup in-scope]
+~~~~~~~~~~~~~~~~~~~~~~
+Consider this example
+ foo :: Int -> Maybe Int -> Int
+ foo 0 (Just n) = n
+ foo m (Just n) = foo (m-n) (Just n)
+
+SpecConstr sees this fragment:
+
+ case w_smT of wild_Xf [Just A] {
+ Data.Maybe.Nothing -> lvl_smf;
+ Data.Maybe.Just n_acT [Just S(L)] ->
+ case n_acT of wild1_ams [Just A] { GHC.Base.I# y_amr [Just L] ->
+ \$wfoo_smW (GHC.Prim.-# ds_Xmb y_amr) wild_Xf
+ }};
+
+and correctly generates the rule
+
+ RULES: "SC:$wfoo1" [0] __forall {y_amr [Just L] :: GHC.Prim.Int#
+ sc_snn :: GHC.Prim.Int#}
+ \$wfoo_smW sc_snn (Data.Maybe.Just @ GHC.Base.Int (GHC.Base.I# y_amr))
+ = \$s\$wfoo_sno y_amr sc_snn ;]
+
+BUT we must ensure that this rule matches in the original function!
+Note that the call to \$wfoo is
+ \$wfoo_smW (GHC.Prim.-# ds_Xmb y_amr) wild_Xf
+
+During matching we expand wild_Xf to (Just n_acT). But then we must also
+expand n_acT to (I# y_amr). And we can only do that if we look up n_acT
+in the in-scope set, because in wild_Xf's unfolding it won't have an unfolding
+at all.
+
+That is why the 'lookupRnInScope' call in the (Var v2) case of 'match'
+is so important.