Better modularity in subenv stuff

1 files changed, 99 insertions, 266 deletions

diff --git a/src/CHAD.hs b/src/CHAD.hs
index 9e1f038..b1251aa 100644
--- a/src/CHAD.hs
+++ b/src/CHAD.hs
@@ -16,7 +16,6 @@ module CHAD where
 
 import Data.Bifunctor (first, second)
 import Data.Kind (Type)
-import Data.Proxy
 import Data.Some
 import GHC.TypeLits (Symbol)
 
@@ -274,16 +273,43 @@ subenvOnehot (SCons _ env) IZ = SEYes (subenvNone env)
 subenvOnehot (SCons _ env) (IS i) = SENo (subenvOnehot env i)
 subenvOnehot SNil i = case i of {}
 
-subenvUnion :: Subenv env env1 -> Subenv env env2 -> (forall env3. Subenv env env3 -> Subenv env3 env1 -> Subenv env3 env2 -> r) -> r
-subenvUnion SETop SETop k = k SETop SETop SETop
-subenvUnion (SENo  sub1) (SENo  sub2) k =
-  subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SENo sub3) s31 s32
-subenvUnion (SEYes sub1) (SENo  sub2) k =
-  subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SEYes sub3) (SEYes s31) (SENo s32)
-subenvUnion (SENo  sub1) (SEYes sub2) k =
-  subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SEYes sub3) (SENo s31) (SEYes s32)
-subenvUnion (SEYes sub1) (SEYes sub2) k =
-  subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SEYes sub3) (SEYes s31) (SEYes s32)
+subenvPlus :: SList STy env
+           -> Subenv env env1 -> Subenv env env2
+           -> (forall env3. Subenv env env3
+                         -> Subenv env3 env1
+                         -> Subenv env3 env2
+                         -> (Ex exenv (Tup (D2E env1))
+                             -> Ex exenv (Tup (D2E env2))
+                             -> Ex exenv (Tup (D2E env3)))
+                         -> r)
+           -> r
+subenvPlus SNil SETop SETop k = k SETop SETop SETop (\_ _ -> ENil ext)
+subenvPlus (SCons _ env) (SENo sub1) (SENo sub2) k =
+  subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl -> k (SENo sub3) s31 s32 pl
+subenvPlus (SCons _ env) (SEYes sub1) (SENo sub2) k =
+  subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl ->
+    k (SEYes sub3) (SEYes s31) (SENo s32) $ \e1 e2 ->
+      ELet ext e1 $
+        EPair ext (pl (EFst ext (EVar ext (typeOf e1) IZ))
+                      (weakenExpr WSink e2))
+                  (ESnd ext (EVar ext (typeOf e1) IZ))
+subenvPlus (SCons _ env) (SENo sub1) (SEYes sub2) k =
+  subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl ->
+    k (SEYes sub3) (SENo s31) (SEYes s32) $ \e1 e2 ->
+      ELet ext e2 $
+        EPair ext (pl (weakenExpr WSink e1)
+                      (EFst ext (EVar ext (typeOf e2) IZ)))
+                  (ESnd ext (EVar ext (typeOf e2) IZ))
+subenvPlus (SCons t env) (SEYes sub1) (SEYes sub2) k =
+  subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl ->
+    k (SEYes sub3) (SEYes s31) (SEYes s32) $ \e1 e2 ->
+      ELet ext e1 $
+      ELet ext (weakenExpr WSink e2) $
+        EPair ext (pl (EFst ext (EVar ext (typeOf e1) (IS IZ)))
+                      (EFst ext (EVar ext (typeOf e2) IZ)))
+                  (plus t
+                    (ESnd ext (EVar ext (typeOf e1) (IS IZ)))
+                    (ESnd ext (EVar ext (typeOf e2) IZ)))
 
 expandSubenvZeros :: SList STy env0 -> Subenv env0 env0F -> Ex env (Tup (D2E env0F)) -> Ex env (Tup (D2E env0))
 expandSubenvZeros _ SETop _ = ENil ext
@@ -293,6 +319,25 @@ expandSubenvZeros (SCons t ts) (SEYes sub) e =
     in EPair ext (expandSubenvZeros ts sub (EFst ext var)) (ESnd ext var)
 expandSubenvZeros (SCons t ts) (SENo sub) e = EPair ext (expandSubenvZeros ts sub e) (zero t)
 
+unscope :: Descr env0 sto
+        -> STy a -> Storage s
+        -> Subenv (Select (a : env0) (s : sto) "merge") envSub
+        -> Ex env (TEVM (D2E (Select (a : env0) (s : sto) "accum")) (Tup (D2E envSub)))
+        -> (forall envSub'.
+               Subenv (Select env0 sto "merge") envSub'
+            -> Ex env (TEVM (D2E (Select env0 sto "accum")) (TPair (Tup (D2E envSub')) (D2 a)))
+            -> r)
+        -> r
+unscope des ty s sub e k = case s of
+  SAccum -> k sub (EMScope e)
+  SMerge -> case sub of
+    SEYes sub' -> k sub' e
+    SENo sub' -> k sub' $
+                   EMBind e $
+                     EMReturn (d2e (select SAccum des)) $
+                       EPair ext (EVar ext (tTup (d2e (subList (select SMerge des) sub'))) IZ)
+                                 (zero ty)
+
 -- d1W :: env :> env' -> D1E env :> D1E env'
 -- d1W WId = WId
 -- d1W WSink = WSink
@@ -425,60 +470,26 @@ drev des policy = \case
     , Some storage <- policy des (typeOf rhs)
     , Ret body0 body1 subBody body2 <- drev (des `DPush` (typeOf rhs, storage)) policy body ->
     weakenBindings weakenExpr (WCopy (sinkWithBindings rhs0)) body0 $ \body0' wbody0' ->
-    case storage of
-      SAccum ->
-        subenvUnion subRHS subBody $ \subBoth subRHS2Both subBody2Both ->
-        let bodyResType = STPair (tTup (d2e (subList (select SMerge des) subBody))) (d2 (typeOf rhs)) in
-        Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0')
-            (weakenExpr wbody0' body1)
-            subBoth
-            (EMBind
-               (weakenExpr (WCopy wbody0') (EMScope body2))
-               (ELet ext (ESnd ext (EVar ext bodyResType IZ)) $
-                 EMBind
-                   (weakenExpr (WCopy (wSinks @[_,_] .> WPop (sinkWithBindings body0'))) rhs2)
-                   (EMReturn d2acc (plusTup (subList (select SMerge des) subBoth)
-                                      (expandSubenvZeros
-                                        (subList (select SMerge des) subBoth)
-                                        subBody2Both
-                                        (EFst ext (EVar ext bodyResType (IS (IS IZ)))))
-                                      (expandSubenvZeros
-                                        (subList (select SMerge des) subBoth)
-                                        subRHS2Both
-                                        (EVar ext (tTup (d2e (subList (select SMerge des) subRHS))) IZ))))))
-
-      SMerge -> case subBody of  -- is the let-bound variable used in the body?
-        SENo subBody' ->  -- it isn't, so the RHS was dead code? Let's not differentiate through the RHS then, in any case
-          Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0')
-              (weakenExpr wbody0' body1)
-              subBody'
-              (weakenExpr (WCopy wbody0') body2)  -- we have no cotangent for the RHS, nothing to pass on, so it's just this
-        SEYes subBody' ->
-          subenvUnion subRHS subBody' $ \subBoth subRHS2Both subBody2Both ->
-          let bodyResType = STPair (tTup (d2e (subList (select SMerge des) subBody'))) (d2 (typeOf rhs)) in
-          Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0')
-              (weakenExpr wbody0' body1)
-              subBoth
-              (EMBind
-                 (weakenExpr (WCopy wbody0') body2)
-                 (ELet ext (ESnd ext (EVar ext bodyResType IZ)) $
-                   EMBind
-                     (weakenExpr (WCopy (wSinks @[_,_] .> WPop (sinkWithBindings body0'))) rhs2)
-                     (EMReturn d2acc (plusTup (subList (select SMerge des) subBoth)
-                                        (expandSubenvZeros
-                                          (subList (select SMerge des) subBoth)
-                                          subBody2Both
-                                          (EFst ext (EVar ext bodyResType (IS (IS IZ)))))
-                                        (expandSubenvZeros
-                                          (subList (select SMerge des) subBoth)
-                                          subRHS2Both
-                                          (EVar ext (tTup (d2e (subList (select SMerge des) subRHS))) IZ))))))
+    unscope des (typeOf rhs) storage subBody body2 $ \subBody' body2' ->
+    subenvPlus (select SMerge des) subRHS subBody' $ \subBoth _ _ plus_RHS_Body ->
+    let bodyResType = STPair (tTup (d2e (subList (select SMerge des) subBody'))) (d2 (typeOf rhs)) in
+    Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0')
+        (weakenExpr wbody0' body1)
+        subBoth
+        (EMBind
+           (weakenExpr (WCopy wbody0') body2')
+           (EMBind
+             (ELet ext (ESnd ext (EVar ext bodyResType IZ)) $
+               weakenExpr (WCopy (wSinks @[_,_] .> WPop (sinkWithBindings body0'))) rhs2)
+             (EMReturn d2acc (plus_RHS_Body
+                                (EVar ext (tTup (d2e (subList (select SMerge des) subRHS))) IZ)
+                                (EFst ext (EVar ext bodyResType (IS IZ)))))))
 
   EPair _ a b
     | Rets binds (RetPair a1 subA a2 `SCons` RetPair b1 subB b2 `SCons` SNil)
         <- retConcat $ drev des policy a `SCons` drev des policy b `SCons` SNil
     , let dt = STPair (d2 (typeOf a)) (d2 (typeOf b)) ->
-    subenvUnion subA subB $ \subBoth subA2Both subB2Both ->
+    subenvPlus (select SMerge des) subA subB $ \subBoth _ _ plus_A_B ->
     Ret binds
         (EPair ext a1 b1)
         subBoth
@@ -489,15 +500,9 @@ drev des policy = \case
             EMBind (ELet ext (ESnd ext (EVar ext dt (IS IZ)))
                       (weakenExpr (WCopy (wSinks @[_,_,_])) b2)) $
             EMReturn d2acc
-              (plusTup (subList (select SMerge des) subBoth)
-                (expandSubenvZeros
-                  (subList (select SMerge des) subBoth)
-                  subA2Both
-                  (EVar ext (tTup (d2e (subList (select SMerge des) subA))) (IS IZ)))
-                (expandSubenvZeros
-                  (subList (select SMerge des) subBoth)
-                  subB2Both
-                  (EVar ext (tTup (d2e (subList (select SMerge des) subB))) IZ)))))
+              (plus_A_B
+                (EVar ext (tTup (d2e (subList (select SMerge des) subA))) (IS IZ))
+                (EVar ext (tTup (d2e (subList (select SMerge des) subB))) IZ))))
 
   EFst _ e
     | Ret e0 e1 sub e2 <- drev des policy e
@@ -553,7 +558,11 @@ drev des policy = \case
     , let tPrimal = STPair (d1 (typeOf a)) (STEither tapeA tapeB) ->
     weakenBindings weakenExpr (WCopy (WSink .> sinkWithBindings e0)) a0 $ \a0' wa0' ->
     weakenBindings weakenExpr (WCopy (WSink .> sinkWithBindings e0)) b0 $ \b0' wb0' ->
-    caseOutSubenv des t1 storageA t2 storageB Proxy Proxy subE subA subB $ \subOut subOutE expandA2 expandB2 ->
+    unscope des t1 storageA subA a2 $ \subA' a2' ->
+    unscope des t2 storageB subB b2 $ \subB' b2' ->
+    subenvPlus (select SMerge des) subA' subB' $ \subAB sAB_A sAB_B _ ->
+    subenvPlus (select SMerge des) subAB subE $ \subOut _ _ plus_AB_E ->
+    let tCaseRet = STPair (tTup (d2e (subList (select SMerge des) subAB))) (STEither (d2 t1) (d2 t2)) in
     Ret (e0 `BPush`
          (d1 (typeOf e), e1) `BPush`
          (tPrimal,
@@ -569,27 +578,33 @@ drev des policy = \case
                     TupBindsReconstruct rebinds wrebinds ->
                       letBinds rebinds $
                         ELet ext (EVar ext (d2 (typeOf a)) (sinkWithBindings rebinds @> IS (IS IZ))) $
-                          EMBind (weakenExpr (WCopy wrebinds) $ expandA2 a2)
+                          EMBind (weakenExpr (WCopy wrebinds) a2')
                                  (EMReturn d2acc
-                                    (EInr ext STNil (EInl ext (d2 t2)
-                                       (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subOut))) (d2 t1)) IZ))))))
-                 (EError (STEVM d2acc (STEither STNil (STEither (d2 t1) (d2 t2)))) "dcase l/rtape"))
+                                    (EPair ext
+                                      (expandSubenvZeros (subList (select SMerge des) subAB) sAB_A $
+                                         EFst ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subA'))) (d2 t1)) IZ))
+                                      (EInl ext (d2 t2)
+                                        (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subA'))) (d2 t1)) IZ))))))
+                 (EError (STEVM d2acc tCaseRet) "dcase l/rtape"))
               (ECase ext (ESnd ext (EVar ext tPrimal (IS (IS IZ))))
-                 (EError (STEVM d2acc (STEither STNil (STEither (d2 t1) (d2 t2)))) "dcase r/ltape")
+                 (EError (STEVM d2acc tCaseRet) "dcase r/ltape")
                  (case reconB (WSink .> WCopy (wSinks @[_,_,_] .> sinkWithBindings e0)) IZ of
                     TupBindsReconstruct rebinds wrebinds ->
                       letBinds rebinds $
                         ELet ext (EVar ext (d2 (typeOf a)) (sinkWithBindings rebinds @> IS (IS IZ))) $
-                          EMBind (weakenExpr (WCopy wrebinds) $ expandB2 b2)
+                          EMBind (weakenExpr (WCopy wrebinds) b2')
                                  (EMReturn d2acc
-                                    (EInr ext STNil (EInr ext (d2 t1)
-                                       (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subOut))) (d2 t2)) IZ))))))))
-           (weakenExpr (WCopy (wSinks @[_,_,_])) $
-             EMBind e2 $
-               EMReturn d2acc (expandSubenvZeros
-                                 (subList (select SMerge des) subOut)
-                                 subOutE
-                                 (EVar ext (tTup (d2e (subList (select SMerge des) subE))) IZ))))
+                                    (EPair ext
+                                       (expandSubenvZeros (subList (select SMerge des) subAB) sAB_B $
+                                          EFst ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subB'))) (d2 t2)) IZ))
+                                       (EInr ext (d2 t1)
+                                         (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subB'))) (d2 t2)) IZ))))))))
+           (EMBind (ELet ext (EInr ext STNil (ESnd ext (EVar ext tCaseRet IZ))) $
+                      weakenExpr (WCopy (wSinks @[_,_,_,_])) e2) $
+              EMReturn d2acc $
+                plus_AB_E
+                  (EFst ext (EVar ext tCaseRet (IS IZ)))
+                  (EVar ext (tTup (d2e (subList (select SMerge des) subE))) IZ)))
 
   EConst _ t val ->
     Ret BTop
@@ -618,185 +633,3 @@ drev des policy = \case
 
   where
     d2acc = d2e (select SAccum des)
-
-caseOutSubenv
-  :: Descr env sto
-  -> STy a1 -> Storage s1
-  -> STy a2 -> Storage s2
-  -> Proxy exenv2 -> Proxy exenv3
-  -> Subenv (Select env sto "merge") envE
-  -> Subenv (Select (a1 : env) (s1 : sto) "merge") env1
-  -> Subenv (Select (a2 : env) (s2 : sto) "merge") env2
-  -> (forall envOut.
-         Subenv (Select env sto "merge") envOut
-      -> Subenv envOut envE
-      -> (Ex exenv2 (TEVM (D2E (Select (a1 : env) (s1 : sto) "accum")) (Tup (D2E env1)))
-          -> Ex exenv2 (TEVM (D2E (Select env sto "accum")) (TPair (Tup (D2E envOut)) (D2 a1))))
-      -> (Ex exenv3 (TEVM (D2E (Select (a2 : env) (s2 : sto) "accum")) (Tup (D2E env2)))
-          -> Ex exenv3 (TEVM (D2E (Select env sto "accum")) (TPair (Tup (D2E envOut)) (D2 a2))))
-      -> r)
-  -> r
-caseOutSubenv des t1 s1 t2 s2 _ _ subE sub1 sub2 k =
-  case (s1, sub1, s2, sub2) of
-    (SAccum, _, SAccum, _) ->
-      subenvUnion sub1 sub2 $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind (EMScope e1) $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub1))) (d2 t1) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-          (\e2 -> EMBind (EMScope e2) $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub2))) (d2 t2) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-    (SAccum, _, SMerge, SEYes sub2') ->
-      subenvUnion sub1 sub2' $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind (EMScope e1) $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub1))) (d2 t1) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-          (\e2 -> EMBind e2 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub2'))) (d2 t2) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-    (SAccum, _, SMerge, SENo sub2') ->
-      subenvUnion sub1 sub2' $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind (EMScope e1) $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub1))) (d2 t1) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-          (\e2 -> EMBind e2 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = tTup (d2e (subList (select SMerge des) sub2')) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EVar ext t IZ)
-                                (zero t2))
-    (SMerge, SEYes sub1', SAccum, _) ->
-      subenvUnion sub1' sub2 $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind e1 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub1'))) (d2 t1) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-          (\e2 -> EMBind (EMScope e2) $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub2))) (d2 t2) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-    (SMerge, SENo sub1', SAccum, _) ->
-      subenvUnion sub1' sub2 $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind e1 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = tTup (d2e (subList (select SMerge des) sub1')) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EVar ext t IZ)
-                                (zero t1))
-          (\e2 -> EMBind (EMScope e2) $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub2))) (d2 t2) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-    (SMerge, SEYes sub1', SMerge, SEYes sub2') ->
-      subenvUnion sub1' sub2' $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind e1 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub1'))) (d2 t1) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-          (\e2 -> EMBind e2 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub2'))) (d2 t2) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-    (SMerge, SEYes sub1', SMerge, SENo sub2') ->
-      subenvUnion sub1' sub2' $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind e1 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub1'))) (d2 t1) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-          (\e2 -> EMBind e2 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = tTup (d2e (subList (select SMerge des) sub2')) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EVar ext t IZ)
-                                (zero t2))
-    (SMerge, SENo sub1', SMerge, SEYes sub2') ->
-      subenvUnion sub1' sub2' $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind e1 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = tTup (d2e (subList (select SMerge des) sub1')) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EVar ext t IZ)
-                                (zero t1))
-          (\e2 -> EMBind e2 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = STPair (tTup (d2e (subList (select SMerge des) sub2'))) (d2 t2) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EFst ext (EVar ext t IZ))
-                                (ESnd ext (EVar ext t IZ)))
-    (SMerge, SENo sub1', SMerge, SENo sub2') ->
-      subenvUnion sub1' sub2' $ \sub3 s31 s32 ->
-      subenvUnion subE sub3 $ \sub4 s4E s43 ->
-        k sub4 s4E
-          (\e1 -> EMBind e1 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = tTup (d2e (subList (select SMerge des) sub1')) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s31 $
-                                   EVar ext t IZ)
-                                (zero t1))
-          (\e2 -> EMBind e2 $
-                    EMReturn (d2e (select SAccum des)) $
-                      let t = tTup (d2e (subList (select SMerge des) sub2')) in
-                      EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $
-                                 expandSubenvZeros (subList (select SMerge des) sub3) s32 $
-                                   EVar ext t IZ)
-                                (zero t2))