+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 [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.
+
+\begin{code}
+eqExpr :: RnEnv2 -> CoreExpr -> CoreExpr -> Bool
+-- ^ A kind of shallow equality used in rule matching, so does
+-- /not/ look through newtypes or predicate types
+
+eqExpr env (Var v1) (Var v2)
+ | rnOccL env v1 == rnOccR env v2
+ = True
+
+-- The next two rules expand non-local variables
+-- C.f. Note [Expanding variables]
+-- and Note [Do not expand locally-bound variables]
+eqExpr env (Var v1) e2
+ | not (locallyBoundL env v1)
+ , Just e1' <- expandId (lookupRnInScope env v1)
+ = eqExpr (nukeRnEnvL env) e1' e2
+
+eqExpr env e1 (Var v2)
+ | not (locallyBoundR env v2)
+ , Just e2' <- expandId (lookupRnInScope env v2)
+ = eqExpr (nukeRnEnvR env) e1 e2'
+
+eqExpr _ (Lit lit1) (Lit lit2) = lit1 == lit2
+eqExpr env (App f1 a1) (App f2 a2) = eqExpr env f1 f2 && eqExpr env a1 a2
+eqExpr env (Lam v1 e1) (Lam v2 e2) = eqExpr (rnBndr2 env v1 v2) e1 e2
+eqExpr env (Note n1 e1) (Note n2 e2) = eq_note env n1 n2 && eqExpr env e1 e2
+eqExpr env (Cast e1 co1) (Cast e2 co2) = tcEqTypeX env co1 co2 && eqExpr env e1 e2
+eqExpr env (Type t1) (Type t2) = tcEqTypeX env t1 t2
+
+eqExpr env (Let (NonRec v1 r1) e1)
+ (Let (NonRec v2 r2) e2) = eqExpr env r1 r2
+ && eqExpr (rnBndr2 env v1 v2) e1 e2
+eqExpr env (Let (Rec ps1) e1)
+ (Let (Rec ps2) e2) = equalLength ps1 ps2
+ && and (zipWith eq_rhs ps1 ps2)
+ && eqExpr env' e1 e2
+ where
+ env' = foldl2 rn_bndr2 env ps2 ps2
+ rn_bndr2 env (b1,_) (b2,_) = rnBndr2 env b1 b2
+ eq_rhs (_,r1) (_,r2) = eqExpr env' r1 r2
+eqExpr env (Case e1 v1 t1 a1)
+ (Case e2 v2 t2 a2) = eqExpr env e1 e2
+ && tcEqTypeX env t1 t2
+ && equalLength a1 a2
+ && and (zipWith (eq_alt env') a1 a2)
+ where
+ env' = rnBndr2 env v1 v2
+
+eqExpr _ _ _ = False
+
+eq_alt :: RnEnv2 -> CoreAlt -> CoreAlt -> Bool
+eq_alt env (c1,vs1,r1) (c2,vs2,r2) = c1==c2 && eqExpr (rnBndrs2 env vs1 vs2) r1 r2
+
+eq_note :: RnEnv2 -> Note -> Note -> Bool
+eq_note _ (SCC cc1) (SCC cc2) = cc1 == cc2
+eq_note _ (CoreNote s1) (CoreNote s2) = s1 == s2
+eq_note _ (InlineMe) (InlineMe) = True
+eq_note _ _ _ = False
+\end{code}
+
+Auxiliary functions
+
+\begin{code}
+locallyBoundL, locallyBoundR :: RnEnv2 -> Var -> Bool
+locallyBoundL rn_env v = inRnEnvL rn_env v
+locallyBoundR rn_env v = inRnEnvR rn_env v
+
+
+expandId :: Id -> Maybe CoreExpr
+expandId id
+ | isExpandableUnfolding unfolding = Just (unfoldingTemplate unfolding)
+ | otherwise = Nothing
+ where
+ unfolding = idUnfolding id
+\end{code}