Repository: cryspen/hax (language: rust)

Issue:
Deep question mark not reconstructed
```rust
pub struct S {
    pub g: Foo,
}

pub struct OtherS {
    pub g: Option<Foo>,
}

pub struct Foo {
    y: u8,
}

impl Foo {
    pub fn from(i: &Foo) -> Self {
    Self {
        y: i.y.clone(),
    }
}
}
struct Error();
impl S {
    pub fn from(i: &OtherS) -> Result<Self, Error> {
        Ok(Self {
            g: Foo::from(i.g.as_ref().ok_or(Error())?),
        })
    }
}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/321a6137ee/gist=4d50913c5233dd3ff8902bad383a17b1)

The F* extraction from the example above contains:
```
let impl_S__from (i: t_OtherS)
    : Core.Result.t_Result t_S t_Error =
  match
    Core.Ops.Try_trait.f_branch #(Core.Result.t_Result
          t_Foo t_Error)
      #FStar.Tactics.Typeclasses.solve
      (Core.Option.impl__ok_or #t_Foo
          #t_Error
          (Core.Option.impl__as_ref #t_Foo
              i.f_g
            <:
            Core.Option.t_Option t_Foo)
          (Error <: t_Error)
        <:
        Core.Result.t_Result t_Foo t_Error
      )
    <:
    Core.Ops.Control_flow.t_ControlFlow
      (Core.Result.t_Result
          Core.Convert.t_Infallible
          t_Error) t_Foo
  with
  | Core.Ops.Control_flow.ControlFlow_Break
    residual ->
    Core.Ops.Try_trait.f_from_residual #(Core.Result.t_Result
          t_S t_Error)
      #(Core.Result.t_Result
          Core.Convert.t_Infallible
          t_Error)
      #FStar.Tactics.Typeclasses.solve
      residual
  | Core.Ops.Control_flow.ControlFlow_Continue
    v_val ->
    Core.Result.Result_Ok
    ({ f_g = impl_Foo__from v_val } <: t_S
    )
    <:
    Core.Result.t_Result t_S t_Error
```
This contains the raw encoding used by Rust for question marks, this should be reconstructed by the engine but it is not.



Discussion / hints:
A workaround is to write:

```rust
pub fn from(i: &OtherS) -> Result<Self, Error> {
        let g = i.g.as_ref().ok_or(Error())?;
        Ok(Self {
            g: Foo::from(g),
        })
    }
```

Fix patch:
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index ef55bf45c..46655a69a 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -109,8 +109,8 @@ module Make (F : Features.T) = struct
 
     let deref_mut_app = concrete_app1 Core__ops__deref__DerefMut__deref_mut
 
-    let local_var (e : expr) : expr option =
-      match e.e with LocalVar _ -> Some e | _ -> None
+    let local_var (e : expr) : local_ident option =
+      match e.e with LocalVar v -> Some v | _ -> None
 
     let arrow (typ : ty) : (ty list * ty) option =
       match typ with
diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml
index b77977519..bd6a62875 100644
--- a/engine/lib/phases/phase_simplify_question_marks.ml
+++ b/engine/lib/phases/phase_simplify_question_marks.ml
@@ -175,14 +175,7 @@ module%inlined_contents Make (FA : Features.T) = struct
               arms =
                 [
                   { arm = { arm_pat = pat_break; body }; _ };
-                  {
-                    arm =
-                      {
-                        arm_pat = pat_continue;
-                        body = { e = LocalVar continue_var; _ };
-                      };
-                    _;
-                  };
+                  { arm = { arm_pat = pat_continue; body = continue_expr }; _ };
                 ];
             }
           when Global_ident.eq_name Core__ops__try_trait__Try__branch n ->
@@ -195,6 +188,13 @@ module%inlined_contents Make (FA : Features.T) = struct
             in
             let* f_break, residual_var' = extract_pat_app_bd pat_break in
             let* f_continue, continue_var' = extract_pat_app_bd pat_continue in
+            let continue_expr =
+              Option.value
+                (UA.Expect.borrow continue_expr)
+                ~default:continue_expr
+            in
+            let continue_expr = UA.unbox_underef_expr continue_expr in
+            let* continue_var = UA.Expect.local_var continue_expr in
             let*? _ = [%equal: local_ident] residual_var residual_var' in
             let*? _ = [%equal: local_ident] continue_var continue_var' in
             let*? _ =


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 bcd7f6e77..a92a71909 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,38 @@ 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_1299_.fst" = '''
+module Side_effects.Issue_1299_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Foo = { f_y:u8 }
+
+type t_S = { f_g:t_Foo }
+
+type t_OtherS = { f_g:Core.Option.t_Option t_Foo }
+
+let impl_Foo__from (i: t_Foo) : t_Foo =
+  { f_y = Core.Clone.f_clone #u8 #FStar.Tactics.Typeclasses.solve i.f_y } <: t_Foo
+
+type t_Error = | Error : t_Error
+
+let impl_S__from (i: t_OtherS) : Core.Result.t_Result t_S t_Error =
+  match
+    Core.Option.impl__ok_or #t_Foo
+      #t_Error
+      (Core.Option.impl__as_ref #t_Foo i.f_g <: Core.Option.t_Option t_Foo)
+      (Error <: t_Error)
+    <:
+    Core.Result.t_Result t_Foo t_Error
+  with
+  | Core.Result.Result_Ok hoist47 ->
+    Core.Result.Result_Ok ({ f_g = impl_Foo__from hoist47 } <: t_S)
+    <:
+    Core.Result.t_Result t_S t_Error
+  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_S t_Error
+'''
 "Side_effects.Issue_1300_.fst" = '''
 module Side_effects.Issue_1300_
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
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 5776afa9b..ec29f9d97 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
@@ -86,6 +86,70 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Definition t_Foo : choice_type :=
+  (int8).
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I int8 :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : int8))) : both L I int8.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {I0 : Interface} {f_y : both L0 I0 int8} : both L0 I0 (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_y (fun f_y =>
+      solve_lift (ret_both ((f_y) : (t_Foo)))) : both L0 I0 (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_y := y)).
+
+Definition t_S : choice_type :=
+  (t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_S) : both L I t_Foo :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : t_Foo))) : both L I t_Foo.
+Fail Next Obligation.
+Equations Build_t_S {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 t_Foo} : both L0 I0 (t_S) :=
+  Build_t_S  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_S)))) : both L0 I0 (t_S).
+Fail Next Obligation.
+Notation "'Build_t_S' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_S (f_g := y)).
+
+Definition t_OtherS : choice_type :=
+  (t_Option t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_OtherS) : both L I (t_Option t_Foo) :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : (t_Option t_Foo)))) : both L I (t_Option t_Foo).
+Fail Next Obligation.
+Equations Build_t_OtherS {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 (t_Option t_Foo)} : both L0 I0 (t_OtherS) :=
+  Build_t_OtherS  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_OtherS)))) : both L0 I0 (t_OtherS).
+Fail Next Obligation.
+Notation "'Build_t_OtherS' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_OtherS (f_g := y)).
+
+Equations impl_Foo__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  impl_Foo__from i  :=
+    solve_lift (Build_t_Foo (f_y := f_clone (f_y i))) : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+Definition t_Error : choice_type :=
+  'unit.
+Equations Build_t_Error : both (fset []) (fset []) (t_Error) :=
+  Build_t_Error  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_Error))) : both (fset []) (fset []) (t_Error).
+Fail Next Obligation.
+
+Equations impl_S__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_OtherS) : both L1 I1 (t_Result t_S t_Error) :=
+  impl_S__from i  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code t_Error] hoist49 := impl__ok_or (impl__as_ref (f_g i)) Error in
+    Result_Ok (letb hoist50 := impl_Foo__from hoist49 in
+    letb hoist51 := Build_t_S (f_g := hoist50) in
+    Result_Ok hoist51))) : both L1 I1 (t_Result t_S t_Error).
+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) ;
@@ -424,6 +488,70 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Definition t_Foo : choice_type :=
+  (int8).
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I int8 :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : int8))) : both L I int8.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {I0 : Interface} {f_y : both L0 I0 int8} : both L0 I0 (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_y (fun f_y =>
+      solve_lift (ret_both ((f_y) : (t_Foo)))) : both L0 I0 (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_y := y)).
+
+Definition t_S : choice_type :=
+  (t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_S) : both L I t_Foo :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : t_Foo))) : both L I t_Foo.
+Fail Next Obligation.
+Equations Build_t_S {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 t_Foo} : both L0 I0 (t_S) :=
+  Build_t_S  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_S)))) : both L0 I0 (t_S).
+Fail Next Obligation.
+Notation "'Build_t_S' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_S (f_g := y)).
+
+Definition t_OtherS : choice_type :=
+  (t_Option t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_OtherS) : both L I (t_Option t_Foo) :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : (t_Option t_Foo)))) : both L I (t_Option t_Foo).
+Fail Next Obligation.
+Equations Build_t_OtherS {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 (t_Option t_Foo)} : both L0 I0 (t_OtherS) :=
+  Build_t_OtherS  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_OtherS)))) : both L0 I0 (t_OtherS).
+Fail Next Obligation.
+Notation "'Build_t_OtherS' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_OtherS (f_g := y)).
+
+Equations impl_Foo__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  impl_Foo__from i  :=
+    solve_lift (Build_t_Foo (f_y := f_clone (f_y i))) : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+Definition t_Error : choice_type :=
+  'unit.
+Equations Build_t_Error : both (fset []) (fset []) (t_Error) :=
+  Build_t_Error  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_Error))) : both (fset []) (fset []) (t_Error).
+Fail Next Obligation.
+
+Equations impl_S__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_OtherS) : both L1 I1 (t_Result t_S t_Error) :=
+  impl_S__from i  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code t_Error] hoist49 := impl__ok_or (impl__as_ref (f_g i)) Error in
+    Result_Ok (letb hoist50 := impl_Foo__from hoist49 in
+    letb hoist51 := Build_t_S (f_g := hoist50) in
+    Result_Ok hoist51))) : both L1 I1 (t_Result t_S t_Error).
+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) ;
@@ -762,6 +890,472 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Definition t_Foo : choice_type :=
+  (int8).
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I int8 :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : int8))) : both L I int8.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {I0 : Interface} {f_y : both L0 I0 int8} : both L0 I0 (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_y (fun f_y =>
+      solve_lift (ret_both ((f_y) : (t_Foo)))) : both L0 I0 (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_y := y)).
+
+Definition t_S : choice_type :=
+  (t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_S) : both L I t_Foo :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : t_Foo))) : both L I t_Foo.
+Fail Next Obligation.
+Equations Build_t_S {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 t_Foo} : both L0 I0 (t_S) :=
+  Build_t_S  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_S)))) : both L0 I0 (t_S).
+Fail Next Obligation.
+Notation "'Build_t_S' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_S (f_g := y)).
+
+Definition t_OtherS : choice_type :=
+  (t_Option t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_OtherS) : both L I (t_Option t_Foo) :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : (t_Option t_Foo)))) : both L I (t_Option t_Foo).
+Fail Next Obligation.
+Equations Build_t_OtherS {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 (t_Option t_Foo)} : both L0 I0 (t_OtherS) :=
+  Build_t_OtherS  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_OtherS)))) : both L0 I0 (t_OtherS).
+Fail Next Obligation.
+Notation "'Build_t_OtherS' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_OtherS (f_g := y)).
+
+Equations impl_Foo__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  impl_Foo__from i  :=
+    solve_lift (Build_t_Foo (f_y := f_clone (f_y i))) : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+Definition t_Error : choice_type :=
+  'unit.
+Equations Build_t_Error : both (fset []) (fset []) (t_Error) :=
+  Build_t_Error  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_Error))) : both (fset []) (fset []) (t_Error).
+Fail Next Obligation.
+
+Equations impl_S__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_OtherS) : both L1 I1 (t_Result t_S t_Error) :=
+  impl_S__from i  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code t_Error] hoist49 := impl__ok_or (impl__as_ref (f_g i)) Error in
+    Result_Ok (letb hoist50 := impl_Foo__from hoist49 in
+    letb hoist51 := Build_t_S (f_g := hoist50) in
+    Result_Ok hoist51))) : both L1 I1 (t_Result t_S t_Error).
+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_Issue_1299_.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)*)
+
+Definition t_Foo : choice_type :=
+  (int8).
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I int8 :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : int8))) : both L I int8.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {I0 : Interface} {f_y : both L0 I0 int8} : both L0 I0 (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_y (fun f_y =>
+      solve_lift (ret_both ((f_y) : (t_Foo)))) : both L0 I0 (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_y := y)).
+
+Definition t_S : choice_type :=
+  (t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_S) : both L I t_Foo :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : t_Foo))) : both L I t_Foo.
+Fail Next Obligation.
+Equations Build_t_S {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 t_Foo} : both L0 I0 (t_S) :=
+  Build_t_S  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_S)))) : both L0 I0 (t_S).
+Fail Next Obligation.
+Notation "'Build_t_S' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_S (f_g := y)).
+
+Definition t_OtherS : choice_type :=
+  (t_Option t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_OtherS) : both L I (t_Option t_Foo) :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : (t_Option t_Foo)))) : both L I (t_Option t_Foo).
+Fail Next Obligation.
+Equations Build_t_OtherS {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 (t_Option t_Foo)} : both L0 I0 (t_OtherS) :=
+  Build_t_OtherS  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_OtherS)))) : both L0 I0 (t_OtherS).
+Fail Next Obligation.
+Notation "'Build_t_OtherS' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_OtherS (f_g := y)).
+
+Equations impl_Foo__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  impl_Foo__from i  :=
+    solve_lift (Build_t_Foo (f_y := f_clone (f_y i))) : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+Definition t_Error : choice_type :=
+  'unit.
+Equations Build_t_Error : both (fset []) (fset []) (t_Error) :=
+  Build_t_Error  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_Error))) : both (fset []) (fset []) (t_Error).
+Fail Next Obligation.
+
+Equations impl_S__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_OtherS) : both L1 I1 (t_Result t_S t_Error) :=
+  impl_S__from i  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code t_Error] hoist49 := impl__ok_or (impl__as_ref (f_g i)) Error in
+    Result_Ok (letb hoist50 := impl_Foo__from hoist49 in
+    letb hoist51 := Build_t_S (f_g := hoist50) in
+    Result_Ok hoist51))) : both L1 I1 (t_Result t_S t_Error).
+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) ;
@@ -1100,6 +1694,70 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Definition t_Foo : choice_type :=
+  (int8).
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I int8 :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : int8))) : both L I int8.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {I0 : Interface} {f_y : both L0 I0 int8} : both L0 I0 (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_y (fun f_y =>
+      solve_lift (ret_both ((f_y) : (t_Foo)))) : both L0 I0 (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_y := y)).
+
+Definition t_S : choice_type :=
+  (t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_S) : both L I t_Foo :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : t_Foo))) : both L I t_Foo.
+Fail Next Obligation.
+Equations Build_t_S {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 t_Foo} : both L0 I0 (t_S) :=
+  Build_t_S  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_S)))) : both L0 I0 (t_S).
+Fail Next Obligation.
+Notation "'Build_t_S' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_S (f_g := y)).
+
+Definition t_OtherS : choice_type :=
+  (t_Option t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_OtherS) : both L I (t_Option t_Foo) :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : (t_Option t_Foo)))) : both L I (t_Option t_Foo).
+Fail Next Obligation.
+Equations Build_t_OtherS {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 (t_Option t_Foo)} : both L0 I0 (t_OtherS) :=
+  Build_t_OtherS  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_OtherS)))) : both L0 I0 (t_OtherS).
+Fail Next Obligation.
+Notation "'Build_t_OtherS' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_OtherS (f_g := y)).
+
+Equations impl_Foo__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  impl_Foo__from i  :=
+    solve_lift (Build_t_Foo (f_y := f_clone (f_y i))) : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+Definition t_Error : choice_type :=
+  'unit.
+Equations Build_t_Error : both (fset []) (fset []) (t_Error) :=
+  Build_t_Error  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_Error))) : both (fset []) (fset []) (t_Error).
+Fail Next Obligation.
+
+Equations impl_S__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_OtherS) : both L1 I1 (t_Result t_S t_Error) :=
+  impl_S__from i  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code t_Error] hoist49 := impl__ok_or (impl__as_ref (f_g i)) Error in
+    Result_Ok (letb hoist50 := impl_Foo__from hoist49 in
+    letb hoist51 := Build_t_S (f_g := hoist50) in
+    Result_Ok hoist51))) : both L1 I1 (t_Result t_S t_Error).
+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) ;
@@ -1438,6 +2096,70 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+Definition t_Foo : choice_type :=
+  (int8).
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I int8 :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : int8))) : both L I int8.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {I0 : Interface} {f_y : both L0 I0 int8} : both L0 I0 (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_y (fun f_y =>
+      solve_lift (ret_both ((f_y) : (t_Foo)))) : both L0 I0 (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_y := y)).
+
+Definition t_S : choice_type :=
+  (t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_S) : both L I t_Foo :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : t_Foo))) : both L I t_Foo.
+Fail Next Obligation.
+Equations Build_t_S {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 t_Foo} : both L0 I0 (t_S) :=
+  Build_t_S  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_S)))) : both L0 I0 (t_S).
+Fail Next Obligation.
+Notation "'Build_t_S' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_S (f_g := y)).
+
+Definition t_OtherS : choice_type :=
+  (t_Option t_Foo).
+Equations f_g {L : {fset Location}} {I : Interface} (s : both L I t_OtherS) : both L I (t_Option t_Foo) :=
+  f_g s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : (t_Option t_Foo)))) : both L I (t_Option t_Foo).
+Fail Next Obligation.
+Equations Build_t_OtherS {L0 : {fset Location}} {I0 : Interface} {f_g : both L0 I0 (t_Option t_Foo)} : both L0 I0 (t_OtherS) :=
+  Build_t_OtherS  :=
+    bind_both f_g (fun f_g =>
+      solve_lift (ret_both ((f_g) : (t_OtherS)))) : both L0 I0 (t_OtherS).
+Fail Next Obligation.
+Notation "'Build_t_OtherS' '[' x ']' '(' 'f_g' ':=' y ')'" := (Build_t_OtherS (f_g := y)).
+
+Equations impl_Foo__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  impl_Foo__from i  :=
+    solve_lift (Build_t_Foo (f_y := f_clone (f_y i))) : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+Definition t_Error : choice_type :=
+  'unit.
+Equations Build_t_Error : both (fset []) (fset []) (t_Error) :=
+  Build_t_Error  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_Error))) : both (fset []) (fset []) (t_Error).
+Fail Next Obligation.
+
+Equations impl_S__from {L1 : {fset Location}} {I1 : Interface} (i : both L1 I1 t_OtherS) : both L1 I1 (t_Result t_S t_Error) :=
+  impl_S__from i  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code t_Error] hoist49 := impl__ok_or (impl__as_ref (f_g i)) Error in
+    Result_Ok (letb hoist50 := impl_Foo__from hoist49 in
+    letb hoist51 := Build_t_S (f_g := hoist50) in
+    Result_Ok hoist51))) : both L1 I1 (t_Result t_S t_Error).
+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) ;
diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs
index a08b80e58..89b9633c7 100644
--- a/tests/side-effects/src/lib.rs
+++ b/tests/side-effects/src/lib.rs
@@ -202,3 +202,31 @@ mod issue_1300 {
         Ok(())
     }
 }
+
+mod issue_1299 {
+    pub struct S {
+        pub g: Foo,
+    }
+
+    pub struct OtherS {
+        pub g: Option<Foo>,
+    }
+
+    pub struct Foo {
+        y: u8,
+    }
+
+    impl Foo {
+        pub fn from(i: &Foo) -> Self {
+            Self { y: i.y.clone() }
+        }
+    }
+    struct Error();
+    impl S {
+        pub fn from(i: &OtherS) -> Result<Self, Error> {
+            Ok(Self {
+                g: Foo::from(i.g.as_ref().ok_or(Error())?),
+            })
+        }
+    }
+}