+\begin{code}
+data RnEnv2
+ = RV2 { envL :: VarEnv Var -- Renaming for Left term
+ , envR :: VarEnv Var -- Renaming for Right term
+ , in_scope :: InScopeSet } -- In scope in left or right terms
+
+-- The renamings envL and envR are *guaranteed* to contain a binding
+-- for every variable bound as we go into the term, even if it is not
+-- renamed. That way we can ask what variables are locally bound
+-- (inRnEnvL, inRnEnvR)
+
+mkRnEnv2 :: InScopeSet -> RnEnv2
+mkRnEnv2 vars = RV2 { envL = emptyVarEnv
+ , envR = emptyVarEnv
+ , in_scope = vars }
+
+rnBndrs2 :: RnEnv2 -> [Var] -> [Var] -> RnEnv2
+-- Arg lists must be of equal length
+rnBndrs2 env bsL bsR = foldl2 rnBndr2 env bsL bsR
+
+rnBndr2 :: RnEnv2 -> Var -> Var -> RnEnv2
+-- (rnBndr2 env bL bR) go under a binder bL in the Left term 1,
+-- and binder bR in the Right term
+-- It finds a new binder, new_b,
+-- and returns an environment mapping bL->new_b and bR->new_b resp.
+rnBndr2 (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bL bR
+ = RV2 { envL = extendVarEnv envL bL new_b -- See Note
+ , envR = extendVarEnv envR bR new_b -- [Rebinding]
+ , in_scope = extendInScopeSet in_scope new_b }
+ where
+ -- Find a new binder not in scope in either term
+ new_b | not (bL `elemInScopeSet` in_scope) = bL
+ | not (bR `elemInScopeSet` in_scope) = bR
+ | otherwise = uniqAway' in_scope bL
+
+ -- Note [Rebinding]
+ -- If the new var is the same as the old one, note that
+ -- the extendVarEnv *deletes* any current renaming
+ -- E.g. (\x. \x. ...) ~ (\y. \z. ...)
+ --
+ -- Inside \x \y { [x->y], [y->y], {y} }
+ -- \x \z { [x->x], [y->y, z->x], {y,x} }
+
+rnBndrL, rnBndrR :: RnEnv2 -> Var -> (RnEnv2, Var)
+-- Used when there's a binder on one side or the other only
+-- Useful when eta-expanding
+rnBndrL (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bL
+ = (RV2 { envL = extendVarEnv envL bL new_b
+ , envR = envR
+ , in_scope = extendInScopeSet in_scope new_b }, new_b)
+ where
+ new_b | not (bL `elemInScopeSet` in_scope) = bL
+ | otherwise = uniqAway' in_scope bL
+
+rnBndrR (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bR
+ = (RV2 { envL = envL
+ , envR = extendVarEnv envR bR new_b
+ , in_scope = extendInScopeSet in_scope new_b }, new_b)
+ where
+ new_b | not (bR `elemInScopeSet` in_scope) = bR
+ | otherwise = uniqAway' in_scope bR
+
+rnOccL, rnOccR :: RnEnv2 -> Var -> Var
+-- Look up the renaming of an occurrence in the left or right term
+rnOccL (RV2 { envL = env }) v = lookupVarEnv env v `orElse` v
+rnOccR (RV2 { envR = env }) v = lookupVarEnv env v `orElse` v
+
+inRnEnvL, inRnEnvR :: RnEnv2 -> Var -> Bool
+-- Tells whether a variable is locally bound
+inRnEnvL (RV2 { envL = env }) v = isJust (lookupVarEnv env v)
+inRnEnvR (RV2 { envR = env }) v = isJust (lookupVarEnv env v)
+
+nukeRnEnvL, nukeRnEnvR :: RnEnv2 -> RnEnv2
+nukeRnEnvL env = env { envL = emptyVarEnv }
+nukeRnEnvR env = env { envR = emptyVarEnv }
+\end{code}