Add markers when creating new abstractions because of a join with bottom

1 files changed, 15 insertions, 1 deletions

diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 9b1d3dd0..713f462b 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -516,7 +516,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
-      let mk_aborrow (pm: proj_marker) (bid : borrow_id) : typed_avalue =
+      let mk_aborrow (pm : proj_marker) (bid : borrow_id) : typed_avalue =
         let value = ABorrow (ASharedBorrow (pm, bid)) in
         { value; ty = borrow_ty }
       in
@@ -832,6 +832,20 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
           convert_value_to_abstractions span abs_kind can_end
             destructure_shared_values ctx v
         in
+        (* Add a marker to the abstraction indicating the provenance of the value *)
+        let absl =
+          List.map
+            (fun abs ->
+              {
+                abs with
+                avalues =
+                  List.map
+                    (add_marker_avalue span ctx0
+                       (if value_is_left then PLeft else PRight))
+                    abs.avalues;
+              })
+            absl
+        in
         push_absl absl;
         (* Return [Bottom] *)
         mk_bottom span v.ty