+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# } } )
+