Repository: cryspen/hax (language: rust)

Issue:
Fatal error in `side_effect_utils.ml`
```
error: [HAX0002] (Other (side_effect_utils.ml)) Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub!
Details: Expected two exact same types, got x=core::result::t_Result<tuple0, int> and y=core::result::t_Result<tuple2<int, [int; 32]>, int>
```

```rust
fn fun() -> Result<(), u8> {
    let val = [0u8; 5]
        .iter()
        // Removing the inner Result/? below makes this pass
        .map(|&prev| Ok::<(u8, [u8; 32]), u8>((prev, Ok::<[u8; 32], u8>([0u8; 32])?)))
        // Removing the ? below makes this pass
        .collect::<Result<Vec<_>, _>>()?;
    Ok(())
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/321a6137ee/gist=ff874b38c8ca2b558057f1c1e7c8359e)



Discussion / hints:
We should try to give a better error here, but I am pretty sure we do not have general support for `map` and `zip` yet because of potential mutability. We should, of course. Let's investigate if early returns within closures are correctly supported yet.

Fix patch:
diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml
index 8d3a6b2a6..4f76505d8 100644
--- a/engine/lib/side_effect_utils.ml
+++ b/engine/lib/side_effect_utils.ml
@@ -481,7 +481,12 @@ struct
                   @@ List.map ~f:U.Reducers.variables_of_pat params
                 in
                 let body = lets_of_bindings lbs body in
-                let effects = SideEffects.without_rw_vars vars effects in
+                let effects =
+                  {
+                    (SideEffects.without_rw_vars vars effects) with
+                    return = None;
+                  }
+                in
                 (body, { lbs = []; effects })
               in
               ({ e with e = Closure { params; body; captures } }, body_effects)


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index b56fb65f0..bcd7f6e77 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
@@ -81,6 +81,52 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
   | Core.Option.Option_Some some -> some
   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
 '''
+"Side_effects.Issue_1300_.fst" = '''
+module Side_effects.Issue_1300_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let v_fun (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 =
+  match
+    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map (Core.Slice.Iter.t_Iter u8)
+          (u8 -> Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8))
+      #FStar.Tactics.Typeclasses.solve
+      #(Core.Result.t_Result (Alloc.Vec.t_Vec (u8 & t_Array u8 (mk_usize 32)) Alloc.Alloc.t_Global)
+          u8)
+      (Core.Iter.Traits.Iterator.f_map #(Core.Slice.Iter.t_Iter u8)
+          #FStar.Tactics.Typeclasses.solve
+          #(Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8)
+          (Core.Slice.impl__iter #u8
+              (Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 5) <: t_Slice u8)
+            <:
+            Core.Slice.Iter.t_Iter u8)
+          (fun prev ->
+              let prev:u8 = prev in
+              match
+                Core.Result.Result_Ok
+                (Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 32) <: t_Array u8 (mk_usize 32))
+                <:
+                Core.Result.t_Result (t_Array u8 (mk_usize 32)) u8
+              with
+              | Core.Result.Result_Ok hoist45 ->
+                Core.Result.Result_Ok (prev, hoist45 <: (u8 & t_Array u8 (mk_usize 32)))
+                <:
+                Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8
+              | Core.Result.Result_Err err ->
+                Core.Result.Result_Err err
+                <:
+                Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8)
+        <:
+        Core.Iter.Adapters.Map.t_Map (Core.Slice.Iter.t_Iter u8)
+          (u8 -> Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8))
+    <:
+    Core.Result.t_Result (Alloc.Vec.t_Vec (u8 & t_Array u8 (mk_usize 32)) Alloc.Alloc.t_Global) u8
+  with
+  | Core.Result.Result_Ok v_val ->
+    Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit u8
+  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Prims.unit u8
+'''
 "Side_effects.Nested_return.fst" = '''
 module Side_effects.Nested_return
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -97,8 +143,8 @@ let v_fun (rng: i8) : (i8 & Core.Result.t_Result Prims.unit Prims.unit) =
   let tmp0, out:(i8 & Core.Result.t_Result Prims.unit Prims.unit) = other_fun rng in
   let rng:i8 = tmp0 in
   match out <: Core.Result.t_Result Prims.unit Prims.unit with
-  | Core.Result.Result_Ok hoist43 ->
-    rng, (Core.Result.Result_Ok hoist43 <: Core.Result.t_Result Prims.unit Prims.unit)
+  | Core.Result.Result_Ok hoist41 ->
+    rng, (Core.Result.Result_Ok hoist41 <: Core.Result.t_Result Prims.unit Prims.unit)
     <:
     (i8 & Core.Result.t_Result Prims.unit Prims.unit)
   | Core.Result.Result_Err err ->
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
index 4148c9cf8..5776afa9b 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
@@ -66,21 +66,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) :
   fun rng  :=
     solve_lift (run (letb '(tmp0,out) := other_fun rng in
     letb _ := assign todo(term) in
-    letb hoist43 := out in
-    letb hoist44 := f_branch hoist43 in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with
+    letb hoist41 := out in
+    letb hoist42 := f_branch hoist41 in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with
     | ControlFlow_Break_case residual =>
       letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in
-      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist42))
+      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist40))
     | ControlFlow_Continue_case val =>
       letb val := ret_both ((val) : ('unit)) in
       ControlFlow_Continue (solve_lift val)
     end in
-    letb hoist46 := Result_Ok hoist45 in
-    letb hoist47 := prod_b (rng,hoist46) in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in
-    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in
+    letb hoist44 := Result_Ok hoist43 in
+    letb hoist45 := prod_b (rng,hoist44) in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in
+    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in
     prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit).
 Fail Next Obligation.
 
@@ -346,14 +346,23 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) :=
+  fun _  :=
+    letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev =>
+      letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in
+      letb hoist48 := prod_b (prev,hoist47) in
+      Result_Ok hoist48)) in
+    Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8).
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
 Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
   test x y  :=
-    solve_lift (run (letb hoist40 := fun i =>
+    solve_lift (run (impl__map x (fun i =>
       letm[choice_typeMonad.option_bind_code] hoist38 := y in
       Option_Some (letb hoist39 := i .+ hoist38 in
-      Option_Some hoist39) in
-    letb hoist41 := impl__map x hoist40 in
-    hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+      Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
 Fail Next Obligation.
 '''
 "Side_effects_Issue_1083_.v" = '''
@@ -395,21 +404,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) :
   fun rng  :=
     solve_lift (run (letb '(tmp0,out) := other_fun rng in
     letb _ := assign todo(term) in
-    letb hoist43 := out in
-    letb hoist44 := f_branch hoist43 in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with
+    letb hoist41 := out in
+    letb hoist42 := f_branch hoist41 in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with
     | ControlFlow_Break_case residual =>
       letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in
-      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist42))
+      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist40))
     | ControlFlow_Continue_case val =>
       letb val := ret_both ((val) : ('unit)) in
       ControlFlow_Continue (solve_lift val)
     end in
-    letb hoist46 := Result_Ok hoist45 in
-    letb hoist47 := prod_b (rng,hoist46) in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in
-    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in
+    letb hoist44 := Result_Ok hoist43 in
+    letb hoist45 := prod_b (rng,hoist44) in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in
+    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in
     prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit).
 Fail Next Obligation.
 
@@ -675,14 +684,23 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) :=
+  fun _  :=
+    letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev =>
+      letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in
+      letb hoist48 := prod_b (prev,hoist47) in
+      Result_Ok hoist48)) in
+    Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8).
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
 Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
   test x y  :=
-    solve_lift (run (letb hoist40 := fun i =>
+    solve_lift (run (impl__map x (fun i =>
       letm[choice_typeMonad.option_bind_code] hoist38 := y in
       Option_Some (letb hoist39 := i .+ hoist38 in
-      Option_Some hoist39) in
-    letb hoist41 := impl__map x hoist40 in
-    hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+      Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
 Fail Next Obligation.
 '''
 "Side_effects_Issue_1089_.v" = '''
@@ -724,21 +742,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) :
   fun rng  :=
     solve_lift (run (letb '(tmp0,out) := other_fun rng in
     letb _ := assign todo(term) in
-    letb hoist43 := out in
-    letb hoist44 := f_branch hoist43 in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with
+    letb hoist41 := out in
+    letb hoist42 := f_branch hoist41 in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with
     | ControlFlow_Break_case residual =>
       letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in
-      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist42))
+      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist40))
     | ControlFlow_Continue_case val =>
       letb val := ret_both ((val) : ('unit)) in
       ControlFlow_Continue (solve_lift val)
     end in
-    letb hoist46 := Result_Ok hoist45 in
-    letb hoist47 := prod_b (rng,hoist46) in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in
-    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in
+    letb hoist44 := Result_Ok hoist43 in
+    letb hoist45 := prod_b (rng,hoist44) in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in
+    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in
     prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit).
 Fail Next Obligation.
 
@@ -1004,14 +1022,361 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) :=
+  fun _  :=
+    letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev =>
+      letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in
+      letb hoist48 := prod_b (prev,hoist47) in
+      Result_Ok hoist48)) in
+    Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8).
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
 Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
   test x y  :=
-    solve_lift (run (letb hoist40 := fun i =>
+    solve_lift (run (impl__map x (fun i =>
       letm[choice_typeMonad.option_bind_code] hoist38 := y in
       Option_Some (letb hoist39 := i .+ hoist38 in
-      Option_Some hoist39) in
-    letb hoist41 := impl__map x hoist40 in
-    hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+      Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+Fail Next Obligation.
+'''
+"Side_effects_Issue_1300_.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+(*Not implemented yet? todo(item)*)
+
+Equations other_fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : both L1 I1 (int8 × t_Result 'unit 'unit) :=
+  other_fun rng  :=
+    letb hax_temp_output := Result_Ok (ret_both (tt : 'unit)) in
+    solve_lift (prod_b (rng,hax_temp_output)) : both L1 I1 (int8 × t_Result 'unit 'unit).
+Fail Next Obligation.
+
+Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : both L1 I1 (int8 × t_Result 'unit 'unit) :=
+  fun rng  :=
+    solve_lift (run (letb '(tmp0,out) := other_fun rng in
+    letb _ := assign todo(term) in
+    letb hoist41 := out in
+    letb hoist42 := f_branch hoist41 in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with
+    | ControlFlow_Break_case residual =>
+      letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in
+      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist40))
+    | ControlFlow_Continue_case val =>
+      letb val := ret_both ((val) : ('unit)) in
+      ControlFlow_Continue (solve_lift val)
+    end in
+    letb hoist44 := Result_Ok hoist43 in
+    letb hoist45 := prod_b (rng,hoist44) in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in
+    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in
+    prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit).
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
+Class t_MyFrom (Self : choice_type) := {
+  f_my_from_loc : {fset Location} ;
+  f_my_from : (forall {L1 I1}, both L1 I1 v_T -> both (L1 :|: f_my_from_loc) I1 v_Self) ;
+}.
+Hint Unfold f_my_from_loc.
+
+#[global] Program Instance int16_t_MyFrom : t_MyFrom int16 int8 :=
+  let f_my_from := fun  {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) => solve_lift (cast_int (WS2 := _) x) : both (L1 :|: fset []) I1 int16 in
+  {| f_my_from_loc := (fset [] : {fset Location});
+  f_my_from := (@f_my_from)|}.
+Fail Next Obligation.
+Hint Unfold int16_t_MyFrom.
+
+Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
+  f x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
+Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
+  add3 x y z  :=
+    solve_lift (impl_u32__wrapping_add (impl_u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
+Fail Next Obligation.
+
+Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
+  local_mutation x  :=
+    letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb hoist1 := x >.? (ret_both (3 : int32)) in
+    solve_lift (ifb hoist1
+    then letb _ := assign todo(term) in
+    letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
+    letb _ := assign todo(term) in
+    letb hoist2 := ret_both (0 : int32) in
+    letb hoist3 := Build_t_Range (f_start := hoist2) (f_end := ret_both (10 : int32)) in
+    letb hoist4 := f_into_iter hoist3 in
+    letb _ := foldi_both_list hoist4 (fun i =>
+      ssp (fun _ =>
+        assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in
+    impl_u32__wrapping_add x y
+    else letb hoist7 := matchb x with
+    | 12 =>
+      letb _ := assign todo(term) in
+      solve_lift (ret_both (3 : int32))
+    | 13 =>
+      letb hoist6 := x in
+      letb _ := assign todo(term) in
+      letb hoist5 := impl_u32__wrapping_add (ret_both (123 : int32)) x in
+      solve_lift (add3 hoist6 hoist5 x)
+    | _ =>
+      solve_lift (ret_both (0 : int32))
+    end in
+    letb _ := assign todo(term) in
+    impl_u32__wrapping_add x y) : both L1 I1 int32.
+Fail Next Obligation.
+
+Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
+  early_returns x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32))
+    then letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (0 : int32)) in
+    ControlFlow_Continue (never_to_any hoist8)
+    else () in
+    letb hoist9 := x >.? (ret_both (30 : int32)) in
+    letm[choice_typeMonad.result_bind_code int32] hoist11 := ifb hoist9
+    then matchb ret_both (true : 'bool) with
+    | true =>
+      letm[choice_typeMonad.result_bind_code int32] hoist10 := ControlFlow_Break (ret_both (34 : int32)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist10))
+    | _ =>
+      ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
+    end
+    else ControlFlow_Continue (letb _ := assign todo(term) in
+    x .+ (ret_both (1 : int32))) in
+    letb hoist12 := impl_u32__wrapping_add (ret_both (123 : int32)) hoist11 in
+    letb hoist13 := impl_u32__wrapping_add hoist12 x in
+    letm[choice_typeMonad.result_bind_code int32] hoist14 := ControlFlow_Break hoist13 in
+    ControlFlow_Continue (never_to_any hoist14))) : both L1 I1 int32.
+Fail Next Obligation.
+
+Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
+  simplifiable_return c1 c2 c3  :=
+    solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in
+    letm[choice_typeMonad.result_bind_code int32] _ := ifb c1
+    then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2
+    then letb _ := assign todo(term) in
+    ifb c3
+    then letm[choice_typeMonad.result_bind_code int32] hoist15 := ControlFlow_Break (ret_both (1 : int32)) in
+    ControlFlow_Continue (never_to_any hoist15)
+    else ()
+    else () in
+    ControlFlow_Continue (letb _ := assign todo(term) in
+    ret_both (tt : 'unit))
+    else () in
+    ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
+Fail Next Obligation.
+
+Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
+  simplifiable_question_mark c x  :=
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c
+    then letm[choice_typeMonad.option_bind_code] hoist16 := x in
+    Option_Some (hoist16 .+ (ret_both (10 : int32)))
+    else Option_Some (ret_both (0 : int32)) in
+    Option_Some (letb b := ret_both (20 : int32) in
+    Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+Fail Next Obligation.
+
+Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in
+    Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark_coercion y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) :=
+  options x y z  :=
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist21 := x in
+    letb hoist22 := hoist21 >.? (ret_both (10 : int8)) in
+    letm[choice_typeMonad.option_bind_code] hoist28 := ifb hoist22
+    then letm[choice_typeMonad.option_bind_code] hoist23 := x in
+    Option_Some (letb hoist24 := impl_u8__wrapping_add hoist23 (ret_both (3 : int8)) in
+    Option_Some hoist24)
+    else letm[choice_typeMonad.option_bind_code] hoist26 := x in
+    letm[choice_typeMonad.option_bind_code] hoist25 := y in
+    Option_Some (letb hoist27 := impl_u8__wrapping_add hoist26 hoist25 in
+    Option_Some hoist27) in
+    letm[choice_typeMonad.option_bind_code] hoist29 := hoist28 in
+    letm[choice_typeMonad.option_bind_code] v := matchb hoist29 with
+    | 3 =>
+      Option_None
+    | 4 =>
+      letm[choice_typeMonad.option_bind_code] hoist18 := z in
+      Option_Some (letb hoist19 := hoist18 >.? (ret_both (4 : int64)) in
+      letb hoist20 := ifb hoist19
+      then ret_both (0 : int8)
+      else ret_both (3 : int8) in
+      solve_lift ((ret_both (4 : int8)) .+ hoist20))
+    | _ =>
+      Option_Some (solve_lift (ret_both (12 : int8)))
+    end in
+    letm[choice_typeMonad.option_bind_code] hoist30 := x in
+    letb hoist32 := impl_u8__wrapping_add v hoist30 in
+    letm[choice_typeMonad.option_bind_code] hoist31 := y in
+    Option_Some (letb hoist33 := impl_u8__wrapping_add hoist32 hoist31 in
+    Option_Some hoist33))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
+Fail Next Obligation.
+
+Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
+  question_mark x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    then letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb hoist34 := x >.? (ret_both (90 : int32)) in
+    ifb hoist34
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    else ()
+    else () in
+    Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
+Fail Next Obligation.
+
+Definition t_A : choice_type :=
+  'unit.
+Equations Build_t_A : both (fset []) (fset []) (t_A) :=
+  Build_t_A  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_A))) : both (fset []) (fset []) (t_A).
+Fail Next Obligation.
+
+Definition t_B : choice_type :=
+  'unit.
+Equations Build_t_B : both (fset []) (fset []) (t_B) :=
+  Build_t_B  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B).
+Fail Next Obligation.
+
+Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) :=
+  monad_lifting x  :=
+    solve_lift (run (ifb x >.? (ret_both (123 : int8))
+    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := ControlFlow_Continue (Result_Err B) in
+    letb hoist36 := Result_Ok hoist35 in
+    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist37 := ControlFlow_Break hoist36 in
+    ControlFlow_Continue (never_to_any hoist37)
+    else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B).
+Fail Next Obligation.
+
+Definition t_Bar : choice_type :=
+  ('bool × nseq ('bool × 'bool) 6 × 'bool).
+Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool :=
+  f_a s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (fst x : 'bool))) : both L I 'bool.
+Fail Next Obligation.
+Equations f_b {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I (nseq ('bool × 'bool) 6 × 'bool) :=
+  f_b s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd x : (nseq ('bool × 'bool) 6 × 'bool)))) : both L I (nseq ('bool × 'bool) 6 × 'bool).
+Fail Next Obligation.
+Equations Build_t_Bar {L0 : {fset Location}} {L1 : {fset Location}} {I0 : Interface} {I1 : Interface} {f_a : both L0 I0 'bool} {f_b : both L1 I1 (nseq ('bool × 'bool) 6 × 'bool)} : both (L0:|:L1) (I0:|:I1) (t_Bar) :=
+  Build_t_Bar  :=
+    bind_both f_b (fun f_b =>
+      bind_both f_a (fun f_a =>
+        solve_lift (ret_both ((f_a,f_b) : (t_Bar))))) : both (L0:|:L1) (I0:|:I1) (t_Bar).
+Fail Next Obligation.
+Notation "'Build_t_Bar' '[' x ']' '(' 'f_a' ':=' y ')'" := (Build_t_Bar (f_a := y) (f_b := f_b x)).
+Notation "'Build_t_Bar' '[' x ']' '(' 'f_b' ':=' y ')'" := (Build_t_Bar (f_a := f_a x) (f_b := y)).
+
+Definition t_Foo : choice_type :=
+  ('bool × 'bool × t_Vec t_Bar t_Global × nseq t_Bar 6 × t_Bar).
+Equations f_x {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I 'bool :=
+  f_x s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (fst (fst (fst x)) : 'bool))) : both L I 'bool.
+Fail Next Obligation.
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I ('bool × t_Vec t_Bar t_Global) :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd (fst (fst x)) : ('bool × t_Vec t_Bar t_Global)))) : both L I ('bool × t_Vec t_Bar t_Global).
+Fail Next Obligation.
+Equations f_z {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I (nseq t_Bar 6) :=
+  f_z s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd (fst x) : (nseq t_Bar 6)))) : both L I (nseq t_Bar 6).
+Fail Next Obligation.
+Equations f_bar {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I t_Bar :=
+  f_bar s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd x : t_Bar))) : both L I t_Bar.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I0 : Interface} {I1 : Interface} {I2 : Interface} {I3 : Interface} {f_x : both L0 I0 'bool} {f_y : both L1 I1 ('bool × t_Vec t_Bar t_Global)} {f_z : both L2 I2 (nseq t_Bar 6)} {f_bar : both L3 I3 t_Bar} : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_bar (fun f_bar =>
+      bind_both f_z (fun f_z =>
+        bind_both f_y (fun f_y =>
+          bind_both f_x (fun f_x =>
+            solve_lift (ret_both ((f_x,f_y,f_z,f_bar) : (t_Foo))))))) : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_x' ':=' y ')'" := (Build_t_Foo (f_x := y) (f_y := f_y x) (f_z := f_z x) (f_bar := f_bar x)).
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := y) (f_z := f_z x) (f_bar := f_bar x)).
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)).
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)).
+
+Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  assign_non_trivial_lhs foo  :=
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    solve_lift foo : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
+Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) :=
+  fun _  :=
+    letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev =>
+      letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in
+      letb hoist48 := prod_b (prev,hoist47) in
+      Result_Ok hoist48)) in
+    Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8).
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
+Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
+  test x y  :=
+    solve_lift (run (impl__map x (fun i =>
+      letm[choice_typeMonad.option_bind_code] hoist38 := y in
+      Option_Some (letb hoist39 := i .+ hoist38 in
+      Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
 Fail Next Obligation.
 '''
 "Side_effects_Nested_return.v" = '''
@@ -1053,21 +1418,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) :
   fun rng  :=
     solve_lift (run (letb '(tmp0,out) := other_fun rng in
     letb _ := assign todo(term) in
-    letb hoist43 := out in
-    letb hoist44 := f_branch hoist43 in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with
+    letb hoist41 := out in
+    letb hoist42 := f_branch hoist41 in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with
     | ControlFlow_Break_case residual =>
       letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in
-      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist42))
+      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist40))
     | ControlFlow_Continue_case val =>
       letb val := ret_both ((val) : ('unit)) in
       ControlFlow_Continue (solve_lift val)
     end in
-    letb hoist46 := Result_Ok hoist45 in
-    letb hoist47 := prod_b (rng,hoist46) in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in
-    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in
+    letb hoist44 := Result_Ok hoist43 in
+    letb hoist45 := prod_b (rng,hoist44) in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in
+    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in
     prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit).
 Fail Next Obligation.
 
@@ -1333,13 +1698,22 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) :=
+  fun _  :=
+    letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev =>
+      letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in
+      letb hoist48 := prod_b (prev,hoist47) in
+      Result_Ok hoist48)) in
+    Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8).
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
 Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
   test x y  :=
-    solve_lift (run (letb hoist40 := fun i =>
+    solve_lift (run (impl__map x (fun i =>
       letm[choice_typeMonad.option_bind_code] hoist38 := y in
       Option_Some (letb hoist39 := i .+ hoist38 in
-      Option_Some hoist39) in
-    letb hoist41 := impl__map x hoist40 in
-    hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+      Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
 Fail Next Obligation.
 '''
diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs
index feb2eba44..a08b80e58 100644
--- a/tests/side-effects/src/lib.rs
+++ b/tests/side-effects/src/lib.rs
@@ -190,3 +190,15 @@ mod nested_return {
         return Ok(other_fun(rng)?);
     }
 }
+
+mod issue_1300 {
+    fn fun() -> Result<(), u8> {
+        let val = [0u8; 5]
+            .iter()
+            // Removing the inner Result/? below makes this pass
+            .map(|&prev| Ok::<(u8, [u8; 32]), u8>((prev, Ok::<[u8; 32], u8>([0u8; 32])?)))
+            // Removing the ? below makes this pass
+            .collect::<Result<Vec<_>, _>>()?;
+        Ok(())
+    }
+}