+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 RuleSubst
+
+We can only do this if 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. Hence the
+use of okToFloat.
+
+There are a couple of tricky points.
+ (a) What if floating the binding captures a variable?
+ 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?
+ 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 "RuleFloatLet".
+
+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.
+
+ * The RnEnv2 in the MatchEnv binds only the local binders
+ in the term (lambdas, case)
+
+ * When we encounter a let in the term to be matched, we
+ check that does not mention any locally bound (lambda, case)
+ variables. If so we fail
+
+ * We use CoreSubst.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.
+
+
+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.