summaryrefslogtreecommitdiff
path: root/src/CHAD.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/CHAD.hs')
-rw-r--r--src/CHAD.hs3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs
index 3399de2..9a08457 100644
--- a/src/CHAD.hs
+++ b/src/CHAD.hs
@@ -404,7 +404,8 @@ subenvPlus :: SBool req1 -> SBool req2
-> (forall e. Ex e (Tup env1) -> Ex e (Tup env2) -> Ex e (Tup env3))
-> r)
-> r
-subenvPlus _ _ SNil SETop SETop k = k SETop (Inj id) (Inj id) (\_ _ -> ENil ext)
+-- don't destroy effects!
+subenvPlus _ _ SNil SETop SETop k = k SETop (Inj id) (Inj id) (\a b -> use a $ use b $ ENil ext)
subenvPlus req1 req2 (SCons _ env) (SENo sub1) (SENo sub2) k =
subenvPlus req1 req2 env sub1 sub2 $ \sub3 s31 s32 pl ->