Implement two phases of loops join + collapse

4 files changed, 552 insertions, 383 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 94f32b73..e9be07aa 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1993,7 +1993,9 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
   (* Return *)
   List.rev !absl
 
-type borrow_or_loan_id = BorrowId of borrow_id | LoanId of loan_id
+type marker_borrow_or_loan_id =
+  | BorrowId of proj_marker * borrow_id
+  | LoanId of proj_marker * loan_id
 
 type g_loan_content_with_ty =
   (ety * loan_content, rty * aloan_content) concrete_or_abs
@@ -2002,12 +2004,12 @@ type g_borrow_content_with_ty =
   (ety * borrow_content, rty * aborrow_content) concrete_or_abs
 
 type merge_abstraction_info = {
-  loans : loan_id_set;
-  borrows : borrow_id_set;
-  borrows_loans : borrow_or_loan_id list;
+  loans : MarkerBorrowId.Set.t;
+  borrows : MarkerBorrowId.Set.t;
+  borrows_loans : marker_borrow_or_loan_id list;
       (** We use a list to preserve the order in which the borrows were found *)
-  loan_to_content : g_loan_content_with_ty BorrowId.Map.t;
-  borrow_to_content : g_borrow_content_with_ty BorrowId.Map.t;
+  loan_to_content : g_loan_content_with_ty MarkerBorrowId.Map.t;
+  borrow_to_content : g_borrow_content_with_ty MarkerBorrowId.Map.t;
 }
 
 (** Small utility to help merging abstractions.
@@ -2023,46 +2025,57 @@ type merge_abstraction_info = {
       contain shared loans).
  *)
 let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
-    (abs : abs) : merge_abstraction_info =
-  let loans : loan_id_set ref = ref BorrowId.Set.empty in
-  let borrows : borrow_id_set ref = ref BorrowId.Set.empty in
-  let borrows_loans : borrow_or_loan_id list ref = ref [] in
-  let loan_to_content : g_loan_content_with_ty BorrowId.Map.t ref =
-    ref BorrowId.Map.empty
+    (avalues : typed_avalue list) : merge_abstraction_info =
+  let loans : MarkerBorrowId.Set.t ref = ref MarkerBorrowId.Set.empty in
+  let borrows : MarkerBorrowId.Set.t ref = ref MarkerBorrowId.Set.empty in
+  let borrows_loans : marker_borrow_or_loan_id list ref = ref [] in
+  let loan_to_content : g_loan_content_with_ty MarkerBorrowId.Map.t ref =
+    ref MarkerBorrowId.Map.empty
   in
-  let borrow_to_content : g_borrow_content_with_ty BorrowId.Map.t ref =
-    ref BorrowId.Map.empty
+  let borrow_to_content : g_borrow_content_with_ty MarkerBorrowId.Map.t ref =
+    ref MarkerBorrowId.Map.empty
   in
 
-  let push_loans ids (lc : g_loan_content_with_ty) : unit =
-    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) span;
-    loans := BorrowId.Set.union !loans ids;
-    BorrowId.Set.iter
-      (fun id ->
+  let push_loans pm ids (lc : g_loan_content_with_ty) : unit =
+    let pm_ids =
+      BorrowId.Set.to_seq ids
+      |> Seq.map (fun x -> (pm, x))
+      |> MarkerBorrowId.Set.of_seq
+    in
+    sanity_check __FILE__ __LINE__
+      (MarkerBorrowId.Set.disjoint !loans pm_ids)
+      span;
+    loans := MarkerBorrowId.Set.union !loans pm_ids;
+    MarkerBorrowId.Set.iter
+      (fun (pm, id) ->
         sanity_check __FILE__ __LINE__
-          (not (BorrowId.Map.mem id !loan_to_content))
+          (not (MarkerBorrowId.Map.mem (pm, id) !loan_to_content))
           span;
-        loan_to_content := BorrowId.Map.add id lc !loan_to_content;
-        borrows_loans := LoanId id :: !borrows_loans)
-      ids
+        loan_to_content := MarkerBorrowId.Map.add (pm, id) lc !loan_to_content;
+        borrows_loans := LoanId (pm, id) :: !borrows_loans)
+      pm_ids
   in
-  let push_loan id (lc : g_loan_content_with_ty) : unit =
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) span;
-    loans := BorrowId.Set.add id !loans;
+  let push_loan pm id (lc : g_loan_content_with_ty) : unit =
+    sanity_check __FILE__ __LINE__
+      (not (MarkerBorrowId.Set.mem (pm, id) !loans))
+      span;
+    loans := MarkerBorrowId.Set.add (pm, id) !loans;
     sanity_check __FILE__ __LINE__
-      (not (BorrowId.Map.mem id !loan_to_content))
+      (not (MarkerBorrowId.Map.mem (pm, id) !loan_to_content))
       span;
-    loan_to_content := BorrowId.Map.add id lc !loan_to_content;
-    borrows_loans := LoanId id :: !borrows_loans
+    loan_to_content := MarkerBorrowId.Map.add (pm, id) lc !loan_to_content;
+    borrows_loans := LoanId (pm, id) :: !borrows_loans
   in
-  let push_borrow id (bc : g_borrow_content_with_ty) : unit =
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) span;
-    borrows := BorrowId.Set.add id !borrows;
+  let push_borrow pm id (bc : g_borrow_content_with_ty) : unit =
+    sanity_check __FILE__ __LINE__
+      (not (MarkerBorrowId.Set.mem (pm, id) !borrows))
+      span;
+    borrows := MarkerBorrowId.Set.add (pm, id) !borrows;
     sanity_check __FILE__ __LINE__
-      (not (BorrowId.Map.mem id !borrow_to_content))
+      (not (MarkerBorrowId.Map.mem (pm, id) !borrow_to_content))
       span;
-    borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
-    borrows_loans := BorrowId id :: !borrows_loans
+    borrow_to_content := MarkerBorrowId.Map.add (pm, id) bc !borrow_to_content;
+    borrows_loans := BorrowId (pm, id) :: !borrows_loans
   in
 
   let iter_avalues =
@@ -2086,7 +2099,7 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
           | Abstract _ -> craise __FILE__ __LINE__ span "Unreachable"
         in
         (match lc with
-        | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
+        | VSharedLoan (bids, _) -> push_loans PNone bids (Concrete (ty, lc))
         | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable");
         (* Continue *)
         super#visit_loan_content env lc
@@ -2104,14 +2117,8 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
         in
         (* Register the loans *)
         (match lc with
-        | ASharedLoan (pm, bids, _, _) ->
-            (* TODO: We should keep track of the marker here *)
-            sanity_check __FILE__ __LINE__ (pm = PNone) span;
-            push_loans bids (Abstract (ty, lc))
-        | AMutLoan (pm, bid, _) ->
-            (* TODO: We should keep track of the marker here *)
-            sanity_check __FILE__ __LINE__ (pm = PNone) span;
-            push_loan bid (Abstract (ty, lc))
+        | ASharedLoan (pm, bids, _, _) -> push_loans pm bids (Abstract (ty, lc))
+        | AMutLoan (pm, bid, _) -> push_loan pm bid (Abstract (ty, lc))
         | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ ->
             (* The abstraction has been destructured, so those shouldn't appear *)
@@ -2127,18 +2134,12 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
         in
         (* Explore the borrow content *)
         (match bc with
-        | AMutBorrow (pm, bid, _) ->
-            (* TODO: We should keep track of the marker here *)
-            sanity_check __FILE__ __LINE__ (pm = PNone) span;
-            push_borrow bid (Abstract (ty, bc))
-        | ASharedBorrow (pm, bid) ->
-            (* TODO: We should keep track of the marker here *)
-            sanity_check __FILE__ __LINE__ (pm = PNone) span;
-            push_borrow bid (Abstract (ty, bc))
+        | AMutBorrow (pm, bid, _) | ASharedBorrow (pm, bid) ->
+            push_borrow pm bid (Abstract (ty, bc))
         | AProjSharedBorrow asb ->
             let register asb =
               match asb with
-              | AsbBorrow bid -> push_borrow bid (Abstract (ty, bc))
+              | AsbBorrow bid -> push_borrow PNone bid (Abstract (ty, bc))
               | AsbProjReborrows _ ->
                   (* Can only happen if the symbolic value (potentially) contains
                      borrows - i.e., we have nested borrows *)
@@ -2159,7 +2160,7 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
     end
   in
 
-  List.iter (iter_avalues#visit_typed_avalue None) abs.avalues;
+  List.iter (iter_avalues#visit_typed_avalue None) avalues;
 
   {
     loans = !loans;
@@ -2275,7 +2276,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
     loan_to_content = loan_to_content0;
     borrow_to_content = borrow_to_content0;
   } =
-    compute_merge_abstraction_info span ctx abs0
+    compute_merge_abstraction_info span ctx abs0.avalues
   in
 
   let {
@@ -2285,17 +2286,28 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
     loan_to_content = loan_to_content1;
     borrow_to_content = borrow_to_content1;
   } =
-    compute_merge_abstraction_info span ctx abs1
+    compute_merge_abstraction_info span ctx abs1.avalues
   in
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
   if merge_funs = None then (
-    (* TODO: In this case, there should be no proj markers *)
     sanity_check __FILE__ __LINE__
-      (BorrowId.Set.disjoint borrows0 borrows1)
+      (List.for_all
+         (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone)
+         borrows_loans0)
+      span;
+    sanity_check __FILE__ __LINE__
+      (List.for_all
+         (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone)
+         borrows_loans1)
       span;
-    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) span);
+    sanity_check __FILE__ __LINE__
+      (MarkerBorrowId.Set.disjoint borrows0 borrows1)
+      span;
+    sanity_check __FILE__ __LINE__
+      (MarkerBorrowId.Set.disjoint loans0 loans1)
+      span);
 
   (* Merge.
      There are several cases:
@@ -2315,8 +2327,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
      We ignore this case for now: we check that whenever we merge two shared loans,
      then their sets of ids are equal.
   *)
-  let merged_borrows = ref BorrowId.Set.empty in
-  let merged_loans = ref BorrowId.Set.empty in
+  let merged_borrows = ref MarkerBorrowId.Set.empty in
+  let merged_loans = ref MarkerBorrowId.Set.empty in
   let avalues = ref [] in
   let push_avalue av =
     log#ldebug
@@ -2329,142 +2341,43 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
     match av with None -> () | Some av -> push_avalue av
   in
 
-  let intersect =
-    BorrowId.Set.union
-      (BorrowId.Set.inter loans0 borrows1)
-      (BorrowId.Set.inter loans1 borrows0)
-  in
-  let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t =
-    let bids = BorrowId.Set.diff bids intersect in
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span;
-    bids
+  (* Phase 1 of the merge: We want to simplify all loan/borrow pairs. *)
+
+  (* There is an asymetry in the merge: We only simplify a loan/borrow pair if the loan is in
+     the abstraction on the left *)
+  let intersect = MarkerBorrowId.Set.inter loans0 borrows1 in
+
+  (* This function is called when handling shared loans, where the projection marker is global to a set of borrow ids.
+     Tracking this requires some set transformations *)
+  let filter_bids (pm : proj_marker) (bids : BorrowId.Set.t) : BorrowId.Set.t =
+    let bids =
+      BorrowId.Set.to_seq bids
+      |> Seq.map (fun x -> (pm, x))
+      |> MarkerBorrowId.Set.of_seq
+    in
+    let bids = MarkerBorrowId.Set.diff bids intersect in
+    sanity_check __FILE__ __LINE__ (not (MarkerBorrowId.Set.is_empty bids)) span;
+    MarkerBorrowId.Set.to_seq bids |> Seq.map snd |> BorrowId.Set.of_seq
   in
-  let filter_bid (bid : BorrowId.id) : BorrowId.id option =
-    if BorrowId.Set.mem bid intersect then None else Some bid
+  let filter_bid (bid : marker_borrow_id) : marker_borrow_id option =
+    if MarkerBorrowId.Set.mem bid intersect then None else Some bid
   in
 
-  let borrow_is_merged id = BorrowId.Set.mem id !merged_borrows in
+  let borrow_is_merged id = MarkerBorrowId.Set.mem id !merged_borrows in
   let set_borrow_as_merged id =
-    merged_borrows := BorrowId.Set.add id !merged_borrows
+    merged_borrows := MarkerBorrowId.Set.add id !merged_borrows
   in
-  let loan_is_merged id = BorrowId.Set.mem id !merged_loans in
+  let loan_is_merged id = MarkerBorrowId.Set.mem id !merged_loans in
   let set_loan_as_merged id =
-    merged_loans := BorrowId.Set.add id !merged_loans
+    merged_loans := MarkerBorrowId.Set.add id !merged_loans
   in
-  let set_loans_as_merged ids = BorrowId.Set.iter set_loan_as_merged ids in
-
-  (* Some utility functions *)
-  (* Merge two aborrow contents - note that those contents must have the same id *)
-  let merge_aborrow_contents (ty0 : rty) (bc0 : aborrow_content) (ty1 : rty)
-      (bc1 : aborrow_content) : typed_avalue =
-    match (bc0, bc1) with
-    | AMutBorrow (pm0, id0, child0), AMutBorrow (pm1, id1, child1) ->
-        (* Sanity-check of the precondition *)
-        sanity_check __FILE__ __LINE__ (id0 = id1) span;
-        (* TODO: We should handle the markers here *)
-        sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-        (Option.get merge_funs).merge_amut_borrows id0 ty0 pm0 child0 ty1 pm1
-          child1
-    | ASharedBorrow (pm0, id0), ASharedBorrow (pm1, id1) ->
-        (* Sanity-check of the precondition *)
-        sanity_check __FILE__ __LINE__ (id0 = id1) span;
-        (* TODO: We should handle the markers here *)
-        sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-        (Option.get merge_funs).merge_ashared_borrows id0 ty0 pm0 ty1 pm1
-    | AProjSharedBorrow _, AProjSharedBorrow _ ->
-        (* Unreachable because requires nested borrows *)
-        craise __FILE__ __LINE__ span "Unreachable"
-    | _ ->
-        (* Unreachable because those cases are ignored (ended/ignored borrows)
-           or inconsistent *)
-        craise __FILE__ __LINE__ span "Unreachable"
-  in
-
-  let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
-      (bc1 : g_borrow_content_with_ty) : typed_avalue =
-    match (bc0, bc1) with
-    | Concrete _, Concrete _ ->
-        (* This can happen only in case of nested borrows *)
-        craise __FILE__ __LINE__ span "Unreachable"
-    | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
-        merge_aborrow_contents ty0 bc0 ty1 bc1
-    | Concrete _, Abstract _ | Abstract _, Concrete _ ->
-        (* TODO: is it really unreachable? *)
-        craise __FILE__ __LINE__ span "Unreachable"
-  in
-
-  let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty)
-      (lc1 : aloan_content) : typed_avalue option =
-    match (lc0, lc1) with
-    | AMutLoan (pm0, id0, child0), AMutLoan (pm1, id1, child1) ->
-        (* Sanity-check of the precondition *)
-        sanity_check __FILE__ __LINE__ (id0 = id1) span;
-        (* TODO: We should handle the markers here *)
-        sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-        (* Register the loan id *)
-        set_loan_as_merged id0;
-        (* Merge *)
-        Some
-          ((Option.get merge_funs).merge_amut_loans id0 ty0 pm0 child0 ty1 pm1
-             child1)
-    | ASharedLoan (pm0, ids0, sv0, child0), ASharedLoan (pm1, ids1, sv1, child1)
-      ->
-        (* TODO: We should handle the markers here *)
-        sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-        (* Filter the ids *)
-        let ids0 = filter_bids ids0 in
-        let ids1 = filter_bids ids1 in
-        (* Check that the sets of ids are the same - if it is not the case, it
-           means we actually need to merge more than 2 avalues: we ignore this
-           case for now *)
-        sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span;
-        let ids = ids0 in
-        if BorrowId.Set.is_empty ids then (
-          (* If the set of ids is empty, we can eliminate this shared loan.
-             For now, we check that we can eliminate the whole shared value
-             altogether.
-             A more complete approach would be to explore the value and introduce
-             as many shared loans/borrows/etc. as necessary for the sub-values.
-             For now, we check that there are no such values that we would need
-             to preserve (in practice it works because we destructure the
-             shared values in the abstractions, and forbid nested borrows).
-          *)
-          sanity_check __FILE__ __LINE__
-            (not (value_has_loans_or_borrows ctx sv0.value))
-            span;
-          sanity_check __FILE__ __LINE__
-            (not (value_has_loans_or_borrows ctx sv0.value))
-            span;
-          sanity_check __FILE__ __LINE__ (is_aignored child0.value) span;
-          sanity_check __FILE__ __LINE__ (is_aignored child1.value) span;
-          None)
-        else (
-          (* Register the loan ids *)
-          set_loans_as_merged ids;
-          (* Merge *)
-          Some
-            ((Option.get merge_funs).merge_ashared_loans ids ty0 pm0 sv0 child0
-               ty1 pm1 sv1 child1))
-    | _ ->
-        (* Unreachable because those cases are ignored (ended/ignored borrows)
-           or inconsistent *)
-        craise __FILE__ __LINE__ span "Unreachable"
-  in
-
-  (* Note that because we may filter ids from a set of id, this function has
-     to register the merged loan ids: the caller doesn't do it (contrary to
-     the borrow case) *)
-  let merge_g_loan_contents (lc0 : g_loan_content_with_ty)
-      (lc1 : g_loan_content_with_ty) : typed_avalue option =
-    match (lc0, lc1) with
-    | Concrete _, Concrete _ ->
-        (* This can not happen: the values should have been destructured *)
-        craise __FILE__ __LINE__ span "Unreachable"
-    | Abstract (ty0, lc0), Abstract (ty1, lc1) ->
-        merge_aloan_contents ty0 lc0 ty1 lc1
-    | Concrete _, Abstract _ | Abstract _, Concrete _ ->
-        (* TODO: is it really unreachable? *)
-        craise __FILE__ __LINE__ span "Unreachable"
+  let set_loans_as_merged pm ids =
+    let ids =
+      BorrowId.Set.to_seq ids
+      |> Seq.map (fun x -> (pm, x))
+      |> MarkerBorrowId.Set.of_seq
+    in
+    MarkerBorrowId.Set.iter set_loan_as_merged ids
   in
 
   (* Note that we first explore the borrows/loans of [abs1], because we
@@ -2475,11 +2388,12 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
   List.iter
     (fun bl ->
       match bl with
-      | BorrowId bid ->
+      | BorrowId (pm, bid) ->
+          let bid = (pm, bid) in
           log#ldebug
             (lazy
               ("merge_into_abstraction_aux: merging borrow "
-             ^ BorrowId.to_string bid));
+              ^ MarkerBorrowId.to_string bid));
 
           (* Check if the borrow has already been merged - this can happen
              because we go through all the borrows/loans in [abs0] *then*
@@ -2493,8 +2407,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
             | None -> ()
             | Some bid ->
                 (* Lookup the contents *)
-                let bc0 = BorrowId.Map.find_opt bid borrow_to_content0 in
-                let bc1 = BorrowId.Map.find_opt bid borrow_to_content1 in
+                let bc0 = MarkerBorrowId.Map.find_opt bid borrow_to_content0 in
+                let bc1 = MarkerBorrowId.Map.find_opt bid borrow_to_content1 in
                 (* Merge *)
                 let av : typed_avalue =
                   match (bc0, bc1) with
@@ -2508,12 +2422,15 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
                           craise __FILE__ __LINE__ span "Unreachable"
                       | Abstract (ty, bc) -> { value = ABorrow bc; ty })
                   | Some bc0, Some bc1 ->
-                      sanity_check __FILE__ __LINE__ (merge_funs <> None) span;
-                      merge_g_borrow_contents bc0 bc1
+                      (* With markers, the case where the same borrow is duplicated should now be unreachable.
+                         Note, this is due to all shared borrows currently taking different ids, this will
+                         not be the case anymore when shared loans will take a unique id instead of a set *)
+                      craise __FILE__ __LINE__ span "Unreachable"
                   | None, None -> craise __FILE__ __LINE__ span "Unreachable"
                 in
                 push_avalue av)
-      | LoanId bid ->
+      | LoanId (pm, bid) ->
+          let bid = (pm, bid) in
           if
             (* Check if the loan has already been treated - it can happen
                for the same reason as for borrows, and also because shared
@@ -2526,15 +2443,15 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
             log#ldebug
               (lazy
                 ("merge_into_abstraction_aux: merging loan "
-               ^ BorrowId.to_string bid));
+                ^ MarkerBorrowId.to_string bid));
 
             (* Check if we need to filter it *)
             match filter_bid bid with
             | None -> ()
             | Some bid ->
                 (* Lookup the contents *)
-                let lc0 = BorrowId.Map.find_opt bid loan_to_content0 in
-                let lc1 = BorrowId.Map.find_opt bid loan_to_content1 in
+                let lc0 = MarkerBorrowId.Map.find_opt bid loan_to_content0 in
+                let lc1 = MarkerBorrowId.Map.find_opt bid loan_to_content1 in
                 (* Merge *)
                 let av : typed_avalue option =
                   match (lc0, lc1) with
@@ -2547,9 +2464,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
                       | Abstract (ty, lc) -> (
                           match lc with
                           | ASharedLoan (pm, bids, sv, child) ->
-                              (* TODO: We should handle the markers here *)
-                              sanity_check __FILE__ __LINE__ (pm = PNone) span;
-                              let bids = filter_bids bids in
+                              let bids = filter_bids pm bids in
                               sanity_check __FILE__ __LINE__
                                 (not (BorrowId.Set.is_empty bids))
                                 span;
@@ -2559,7 +2474,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
                                 (not (value_has_loans_or_borrows ctx sv.value))
                                 span;
                               let lc = ASharedLoan (pm, bids, sv, child) in
-                              set_loans_as_merged bids;
+                              set_loans_as_merged pm bids;
                               Some { value = ALoan lc; ty }
                           | AMutLoan _ ->
                               set_loan_as_merged bid;
@@ -2570,8 +2485,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
                               (* The abstraction has been destructured, so those shouldn't appear *)
                               craise __FILE__ __LINE__ span "Unreachable"))
                   | Some lc0, Some lc1 ->
-                      sanity_check __FILE__ __LINE__ (merge_funs <> None) span;
-                      merge_g_loan_contents lc0 lc1
+                      (* With projection markers, shared loans should not be duplicated *)
+                      craise __FILE__ __LINE__ span "Unreachable"
                   | None, None -> craise __FILE__ __LINE__ span "Unreachable"
                 in
                 push_opt_avalue av))
@@ -2579,7 +2494,209 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
 
   (* Reverse the avalues (we visited the loans/borrows in order, but pushed
      new values at the beggining of the stack of avalues) *)
-  let avalues = List.rev !avalues in
+  let abs_values = List.rev !avalues in
+
+  (* Phase 2: We now remove markers, by replacing pairs of the same element with left/right markers into one element
+     with only one marker. To do so, we linearly traverse the abstraction created through the first phase *)
+
+  (* We first reset the list of avalues, and will construct avalues similarly to the previous phase *)
+  avalues := [];
+
+  (* We recompute the relevant information on the abstraction after phase 1 *)
+  let { loans; borrows; borrows_loans; loan_to_content; borrow_to_content } =
+    compute_merge_abstraction_info span ctx abs_values
+  in
+
+  (* We will merge elements with the same borrow/loan id, but with different markers.
+     Hence, we only keep track of the id here: if Borrow PLeft bid has been merged
+     and we see Borrow PRight bid, we should ignore Borrow PRight bid *)
+  let merged_borrows = ref BorrowId.Set.empty in
+  let merged_loans = ref BorrowId.Set.empty in
+
+  let borrow_is_merged id = BorrowId.Set.mem id !merged_borrows in
+  let set_borrow_as_merged id =
+    merged_borrows := BorrowId.Set.add id !merged_borrows
+  in
+
+  let loan_is_merged id = BorrowId.Set.mem id !merged_loans in
+  let set_loan_as_merged id =
+    merged_loans := BorrowId.Set.add id !merged_loans
+  in
+  let set_loans_as_merged ids = BorrowId.Set.iter set_loan_as_merged ids in
+
+  (* Recreates an avalue from a borrow_content. *)
+  let avalue_from_bc = function
+    | Concrete (_, _) ->
+        (* This can happen only in case of nested borrows, and should have been filtered during phase 1 *)
+        craise __FILE__ __LINE__ span "Unreachable"
+    | Abstract (ty, bc) -> { value = ABorrow bc; ty }
+  in
+
+  (* Recreates an avalue from a loan_content *)
+  let avalue_from_lc = function
+    | Concrete (_, _) ->
+        (* This can happen only in case of nested borrows, and should have been filtered during phase 1 *)
+        craise __FILE__ __LINE__ span "Unreachable"
+    | Abstract (ty, bc) -> { value = ALoan bc; ty }
+  in
+
+  (* Some utility functions *)
+  (* Merge two aborrow contents - note that those contents must have the same id *)
+  let merge_aborrow_contents (ty0 : rty) (bc0 : aborrow_content) (ty1 : rty)
+      (bc1 : aborrow_content) : typed_avalue =
+    match (bc0, bc1) with
+    | AMutBorrow (pm0, id0, child0), AMutBorrow (pm1, id1, child1) ->
+        (* Sanity-check of the precondition *)
+        sanity_check __FILE__ __LINE__ (id0 = id1) span;
+        sanity_check __FILE__ __LINE__
+          ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft))
+          span;
+        (Option.get merge_funs).merge_amut_borrows id0 ty0 pm0 child0 ty1 pm1
+          child1
+    | ASharedBorrow (pm0, id0), ASharedBorrow (pm1, id1) ->
+        (* Sanity-check of the precondition *)
+        sanity_check __FILE__ __LINE__ (id0 = id1) span;
+        sanity_check __FILE__ __LINE__
+          ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft))
+          span;
+        (Option.get merge_funs).merge_ashared_borrows id0 ty0 pm0 ty1 pm1
+    | AProjSharedBorrow _, AProjSharedBorrow _ ->
+        (* Unreachable because requires nested borrows *)
+        craise __FILE__ __LINE__ span "Unreachable"
+    | _ ->
+        (* Unreachable because those cases are ignored (ended/ignored borrows)
+           or inconsistent *)
+        craise __FILE__ __LINE__ span "Unreachable"
+  in
+
+  let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
+      (bc1 : g_borrow_content_with_ty) : typed_avalue =
+    match (bc0, bc1) with
+    | Concrete _, Concrete _ ->
+        (* This can happen only in case of nested borrows *)
+        craise __FILE__ __LINE__ span "Unreachable"
+    | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
+        merge_aborrow_contents ty0 bc0 ty1 bc1
+    | Concrete _, Abstract _ | Abstract _, Concrete _ ->
+        (* TODO: is it really unreachable? *)
+        craise __FILE__ __LINE__ span "Unreachable"
+  in
+
+  let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty)
+      (lc1 : aloan_content) : typed_avalue =
+    match (lc0, lc1) with
+    | AMutLoan (pm0, id0, child0), AMutLoan (pm1, id1, child1) ->
+        (* Sanity-check of the precondition *)
+        sanity_check __FILE__ __LINE__ (id0 = id1) span;
+        sanity_check __FILE__ __LINE__
+          ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft))
+          span;
+        (* Register the loan id *)
+        set_loan_as_merged id0;
+        (* Merge *)
+        (Option.get merge_funs).merge_amut_loans id0 ty0 pm0 child0 ty1 pm1
+          child1
+    | ASharedLoan (pm0, ids0, sv0, child0), ASharedLoan (pm1, ids1, sv1, child1)
+      ->
+        sanity_check __FILE__ __LINE__
+          ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft))
+          span;
+        (* Check that the sets of ids are the same - if it is not the case, it
+           means we actually need to merge more than 2 avalues: we ignore this
+           case for now *)
+        sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span;
+        let ids = ids0 in
+        (* Register the loan ids *)
+        set_loans_as_merged ids;
+        (* Merge *)
+        (Option.get merge_funs).merge_ashared_loans ids ty0 pm0 sv0 child0 ty1
+          pm1 sv1 child1
+    | _ ->
+        (* Unreachable because those cases are ignored (ended/ignored borrows)
+           or inconsistent *)
+        craise __FILE__ __LINE__ span "Unreachable"
+  in
+
+  (* Note that because we may filter ids from a set of id, this function has
+     to register the merged loan ids: the caller doesn't do it (contrary to
+     the borrow case) *)
+  let merge_g_loan_contents (lc0 : g_loan_content_with_ty)
+      (lc1 : g_loan_content_with_ty) : typed_avalue =
+    match (lc0, lc1) with
+    | Concrete _, Concrete _ ->
+        (* This can not happen: the values should have been destructured *)
+        craise __FILE__ __LINE__ span "Unreachable"
+    | Abstract (ty0, lc0), Abstract (ty1, lc1) ->
+        merge_aloan_contents ty0 lc0 ty1 lc1
+    | Concrete _, Abstract _ | Abstract _, Concrete _ ->
+        (* TODO: is it really unreachable? *)
+        craise __FILE__ __LINE__ span "Unreachable"
+  in
+
+  let invert_proj_marker = function
+    | PNone -> craise __FILE__ __LINE__ span "Unreachable"
+    | PLeft -> PRight
+    | PRight -> PLeft
+  in
+
+  (* We now iter over all elements in the current abstraction. For each element with a marker
+     (i.e., not PNone), we attempt to find the dual element in the rest of the list. If so,
+     we remove both elements, and insert the same element but with no marker.
+
+     Importantly, attempting the merge when first seeing a marked element allows us to preserve
+     the structure of the abstraction we are merging into (abs1). During phase1, we traversed
+     the borrow_loans of the abs1 first, and hence these elements are at the top of the list *)
+  List.iter
+    (function
+      | BorrowId (PNone, bid) ->
+          (* This element has no marker. We do not filter it, hence we retrieve the contents and inject it into
+             the avalues list *)
+          let bc = MarkerBorrowId.Map.find (PNone, bid) borrow_to_content in
+          push_avalue (avalue_from_bc bc)
+      | BorrowId (pm, bid) ->
+          (* Check if the borrow has already been merged. If so, it was already added to the avalues list, we skip it *)
+          if borrow_is_merged bid then ()
+          else (
+            set_borrow_as_merged bid;
+            let bc0 = MarkerBorrowId.Map.find (pm, bid) borrow_to_content in
+            let obc1 =
+              MarkerBorrowId.Map.find_opt
+                (invert_proj_marker pm, bid)
+                borrow_to_content
+            in
+            match obc1 with
+            | None ->
+                (* No dual element found, we keep the current one in the list of avalues, with the same marker *)
+                push_avalue (avalue_from_bc bc0)
+            | Some bc1 ->
+                (* We have borrows with left and right markers in the environment.
+                   We merge their values, and push the result to the list of avalues. The merge will also remove the projection marker *)
+                push_avalue (merge_g_borrow_contents bc0 bc1))
+      | LoanId (PNone, bid) ->
+          (* Same as BorrowId PNone above. We do not filter this element *)
+          let lc = MarkerBorrowId.Map.find (PNone, bid) loan_to_content in
+          push_avalue (avalue_from_lc lc)
+      | LoanId (pm, bid) -> (
+          if
+            (* Check if the loan has already been merged. If so, we skip it *)
+            loan_is_merged bid
+          then ()
+          else
+            let lc0 = MarkerBorrowId.Map.find (pm, bid) loan_to_content in
+            let olc1 =
+              MarkerBorrowId.Map.find_opt
+                (invert_proj_marker pm, bid)
+                loan_to_content
+            in
+            match olc1 with
+            | None ->
+                (* No dual element found, we keep the current one with the same marker *)
+                push_avalue (avalue_from_lc lc0)
+            | Some lc1 -> push_avalue (merge_g_loan_contents lc0 lc1)))
+    borrows_loans;
+
+  (* We traversed and pushed elements in the same order as the traversal, so we do not need to reverse the list *)
+  let avalues = !avalues in
 
   (* Reorder the avalues. We want the avalues to have the borrows first, then
      the loans (this structure is more stable when we merge abstractions together,
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 23e05e06..cd609ab0 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -26,33 +26,6 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result
 (** Union Find *)
 module UF = UnionFind.Make (UnionFind.StoreMap)
 
-type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord]
-
-module MarkerBorrowIdOrd = struct
-  type t = marker_borrow_id
-
-  let compare = compare_marker_borrow_id
-  let to_string = show_marker_borrow_id
-  let pp_t = pp_marker_borrow_id
-  let show_t = show_marker_borrow_id
-end
-
-module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd)
-module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd)
-
-module MarkerBorrowId : sig
-  type t
-
-  module Set : Collections.Set with type elt = t
-  module Map : Collections.Map with type key = t
-end
-with type t = marker_borrow_id = struct
-  type t = marker_borrow_id
-
-  module Set = MarkerBorrowIdSet
-  module Map = MarkerBorrowIdMap
-end
-
 (** A small utility -
 
     Rem.: some environments may be ill-formed (they may contain several times
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 7f80e496..1e099d96 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -122,8 +122,13 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span)
       i -> s@7 : u32
       abs@4 { MB l0, ML l4 }
     ]}
+
+    If [merge_funs] is None, we ensure that there are no markers in the environments.
+    If [merge_funs] is Some _, we merge environments that contain borrow/loan pairs with the same markers, omitting
+    pairs with the PNone marker (i.e., no marker)
  *)
-let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets)
+let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
+    (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets)
     (ctx0 : eval_ctx) : eval_ctx =
   (* Debug *)
   log#ldebug
@@ -132,6 +137,8 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets)
       ^ eval_ctx_to_string ~span:(Some span) ctx0
       ^ "\n\n"));
 
+  let allow_markers = merge_funs <> None in
+
   let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in
   let can_end = true in
   let destructure_shared_values = true in
@@ -212,49 +219,53 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets)
       let bids = MarkerBorrowId.Set.elements bids in
       List.iter
         (fun bid ->
+          if not allow_markers then
+            sanity_check __FILE__ __LINE__ (fst bid = PNone) span;
           match MarkerBorrowId.Map.find_opt bid loan_to_abs with
           | None -> (* Nothing to do *) ()
           | Some abs_ids1 ->
-              AbstractionId.Set.iter
-                (fun abs_id1 ->
-                  (* We need to merge - unless we have already merged *)
-                  (* First, find the representatives for the two abstractions (the
-                     representative is the abstraction into which we merged) *)
-                  let abs_ref0 =
-                    UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs)
-                  in
-                  let abs_id0 = UnionFind.get abs_ref0 in
-                  let abs_ref1 =
-                    UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs)
-                  in
-                  let abs_id1 = UnionFind.get abs_ref1 in
-                  (* If the two ids are the same, it means the abstractions were already merged *)
-                  if abs_id0 = abs_id1 then ()
-                  else (
-                    (* We actually need to merge the abstractions *)
-
-                    (* Debug *)
-                    log#ldebug
-                      (lazy
-                        ("reduce_ctx: merging abstraction "
-                        ^ AbstractionId.to_string abs_id1
-                        ^ " into "
-                        ^ AbstractionId.to_string abs_id0
-                        ^ ":\n\n"
-                        ^ eval_ctx_to_string ~span:(Some span) !ctx));
-
-                    (* Update the environment - pay attention to the order: we
-                       we merge [abs_id1] *into* [abs_id0] *)
-                    let nctx, abs_id =
-                      merge_into_abstraction span abs_kind can_end None !ctx
-                        abs_id1 abs_id0
+              if allow_markers && fst bid = PNone then ()
+              else
+                AbstractionId.Set.iter
+                  (fun abs_id1 ->
+                    (* We need to merge - unless we have already merged *)
+                    (* First, find the representatives for the two abstractions (the
+                       representative is the abstraction into which we merged) *)
+                    let abs_ref0 =
+                      UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs)
                     in
-                    ctx := nctx;
-
-                    (* Update the union find *)
-                    let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in
-                    UnionFind.set abs_ref_merged abs_id))
-                abs_ids1)
+                    let abs_id0 = UnionFind.get abs_ref0 in
+                    let abs_ref1 =
+                      UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs)
+                    in
+                    let abs_id1 = UnionFind.get abs_ref1 in
+                    (* If the two ids are the same, it means the abstractions were already merged *)
+                    if abs_id0 = abs_id1 then ()
+                    else (
+                      (* We actually need to merge the abstractions *)
+
+                      (* Debug *)
+                      log#ldebug
+                        (lazy
+                          ("reduce_ctx: merging abstraction "
+                          ^ AbstractionId.to_string abs_id1
+                          ^ " into "
+                          ^ AbstractionId.to_string abs_id0
+                          ^ ":\n\n"
+                          ^ eval_ctx_to_string ~span:(Some span) !ctx));
+
+                      (* Update the environment - pay attention to the order: we
+                         we merge [abs_id1] *into* [abs_id0] *)
+                      let nctx, abs_id =
+                        merge_into_abstraction span abs_kind can_end merge_funs
+                          !ctx abs_id1 abs_id0
+                      in
+                      ctx := nctx;
+
+                      (* Update the union find *)
+                      let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in
+                      UnionFind.set abs_ref_merged abs_id))
+                  abs_ids1)
         bids)
     abs_ids;
 
@@ -278,8 +289,11 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets)
   (* Return the new context *)
   ctx
 
+(* Reduce_ctx can only be called in a context with no markers *)
+let reduce_ctx = reduce_ctx_with_markers None
+
 (* TODO Adapt and comment *)
-let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
+let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id)
     (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx)
     : eval_ctx =
   (* Debug *)
@@ -296,128 +310,153 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
   let is_fresh_abs_id (id : AbstractionId.id) : bool =
     not (AbstractionId.Set.mem id old_ids.aids)
   in
-  let is_fresh_did (id : DummyVarId.id) : bool =
-    not (DummyVarId.Set.mem id old_ids.dids)
-  in
-  (* Convert the dummy values to abstractions (note that when we convert
-     values to abstractions, the resulting abstraction should be destructured) *)
-  (* Note that we preserve the order of the dummy values: we replace them with
-     abstractions in place - this makes matching easier *)
-  let env =
-    List.concat
-      (List.map
-         (fun ee ->
-           match ee with
-           | EAbs _ | EFrame | EBinding (BVar _, _) -> [ ee ]
-           | EBinding (BDummy id, v) ->
-               if is_fresh_did id then
-                 let absl =
-                   convert_value_to_abstractions span abs_kind can_end
-                     destructure_shared_values ctx0 v
-                 in
-                 List.map (fun abs -> EAbs abs) absl
-               else [ ee ])
-         ctx0.env)
-  in
-  let ctx = { ctx0 with env } in
-  log#ldebug
-    (lazy
-      ("collapse_ctx: after converting values to abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n"
-      ^ eval_ctx_to_string ~span:(Some span) ctx
-      ^ "\n\n"));
-
-  log#ldebug
-    (lazy
-      ("collapse_ctx: after decomposing the shared values in the abstractions:\n"
-     ^ show_ids_sets old_ids ^ "\n\n- ctx:\n"
-      ^ eval_ctx_to_string ~span:(Some span) ctx
-      ^ "\n\n"));
 
   (* Explore all the *new* abstractions, and compute various maps *)
   let explore (abs : abs) = is_fresh_abs_id abs.abs_id in
-  let ids_maps = compute_abs_borrows_loans_maps span false explore env in
+  let ids_maps = compute_abs_borrows_loans_maps span false explore ctx0.env in
   let {
     abs_ids;
     abs_to_borrows;
-    abs_to_loans = _;
+    abs_to_loans;
     abs_to_borrows_loans;
-    borrow_to_abs = _;
+    borrow_to_abs;
     loan_to_abs;
     borrow_loan_to_abs;
   } =
     ids_maps
   in
 
-  (* Change the merging behaviour depending on the input parameters *)
-  let abs_to_borrows, loan_to_abs =
-    (abs_to_borrows_loans, borrow_loan_to_abs)
-  in
-
   (* Merge the abstractions together *)
   let merged_abs : AbstractionId.id UnionFind.elem AbstractionId.Map.t =
     AbstractionId.Map.of_list
       (List.map (fun id -> (id, UnionFind.make id)) abs_ids)
   in
 
-  let ctx = ref ctx in
+  let ctx = ref ctx0 in
 
-  (* Merge all the mergeable abs.
+  let invert_proj_marker = function
+    | PNone -> craise __FILE__ __LINE__ span "Unreachable"
+    | PLeft -> PRight
+    | PRight -> PLeft
+  in
 
-     We iterate over the abstractions, then over the borrows in the abstractions.
-     We do this because we want to control the order in which abstractions
-     are merged (the ids are iterated in increasing order). Otherwise, we
-     could simply iterate over all the borrows in [borrow_to_abs]...
+  (* Merge all the mergeable abs where the same element in present in both abs,
+     but with left and right markers respectively.
+
+     We first check all borrows, then all loans
   *)
   List.iter
     (fun abs_id0 ->
       let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in
       let bids = MarkerBorrowId.Set.elements bids in
       List.iter
-        (fun bid ->
-          match MarkerBorrowId.Map.find_opt bid loan_to_abs with
-          | None -> (* Nothing to do *) ()
-          | Some abs_ids1 ->
-              AbstractionId.Set.iter
-                (fun abs_id1 ->
-                  (* We need to merge - unless we have already merged *)
-                  (* First, find the representatives for the two abstractions (the
-                     representative is the abstraction into which we merged) *)
-                  let abs_ref0 =
-                    UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs)
-                  in
-                  let abs_id0 = UnionFind.get abs_ref0 in
-                  let abs_ref1 =
-                    UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs)
-                  in
-                  let abs_id1 = UnionFind.get abs_ref1 in
-                  (* If the two ids are the same, it means the abstractions were already merged *)
-                  if abs_id0 = abs_id1 then ()
-                  else (
-                    (* We actually need to merge the abstractions *)
-
-                    (* Debug *)
-                    log#ldebug
-                      (lazy
-                        ("collapse_ctx: merging abstraction "
-                        ^ AbstractionId.to_string abs_id1
-                        ^ " into "
-                        ^ AbstractionId.to_string abs_id0
-                        ^ ":\n\n"
-                        ^ eval_ctx_to_string ~span:(Some span) !ctx));
-
-                    (* Update the environment - pay attention to the order: we
-                       we merge [abs_id1] *into* [abs_id0] *)
-                    let nctx, abs_id =
-                      merge_into_abstraction span abs_kind can_end
-                        (Some merge_funs) !ctx abs_id1 abs_id0
+        (fun (pm, bid) ->
+          if pm = PNone then ()
+          else
+            (* We are looking for an element with the same borrow_id, but with the dual marker *)
+            match
+              MarkerBorrowId.Map.find_opt
+                (invert_proj_marker pm, bid)
+                borrow_to_abs
+            with
+            | None -> (* Nothing to do *) ()
+            | Some abs_ids1 ->
+                AbstractionId.Set.iter
+                  (fun abs_id1 ->
+                    (* We need to merge - unless we have already merged *)
+                    (* First, find the representatives for the two abstractions (the
+                       representative is the abstraction into which we merged) *)
+                    let abs_ref0 =
+                      UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs)
                     in
-                    ctx := nctx;
-
-                    (* Update the union find *)
-                    let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in
-                    UnionFind.set abs_ref_merged abs_id))
-                abs_ids1)
+                    let abs_id0 = UnionFind.get abs_ref0 in
+                    let abs_ref1 =
+                      UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs)
+                    in
+                    let abs_id1 = UnionFind.get abs_ref1 in
+                    (* If the two ids are the same, it means the abstractions were already merged *)
+                    if abs_id0 = abs_id1 then ()
+                    else (
+                      (* We actually need to merge the abstractions *)
+
+                      (* Debug *)
+                      log#ldebug
+                        (lazy
+                          ("collapse_ctx: merging abstraction "
+                          ^ AbstractionId.to_string abs_id1
+                          ^ " into "
+                          ^ AbstractionId.to_string abs_id0
+                          ^ ":\n\n"
+                          ^ eval_ctx_to_string ~span:(Some span) !ctx));
+
+                      (* Update the environment - pay attention to the order: we
+                         we merge [abs_id1] *into* [abs_id0] *)
+                      let nctx, abs_id =
+                        merge_into_abstraction span abs_kind can_end
+                          (Some merge_funs) !ctx abs_id1 abs_id0
+                      in
+                      ctx := nctx;
+
+                      (* Update the union find *)
+                      let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in
+                      UnionFind.set abs_ref_merged abs_id))
+                  abs_ids1)
+        bids;
+      (* We now traverse the loans *)
+      let bids = AbstractionId.Map.find abs_id0 abs_to_loans in
+      let bids = MarkerBorrowId.Set.elements bids in
+      List.iter
+        (fun (pm, bid) ->
+          if pm = PNone then ()
+          else
+            (* We are looking for an element with the same borrow_id, but with the dual marker *)
+            match
+              MarkerBorrowId.Map.find_opt
+                (invert_proj_marker pm, bid)
+                loan_to_abs
+            with
+            | None -> (* Nothing to do *) ()
+            | Some abs_ids1 ->
+                AbstractionId.Set.iter
+                  (fun abs_id1 ->
+                    (* We need to merge - unless we have already merged *)
+                    (* First, find the representatives for the two abstractions (the
+                       representative is the abstraction into which we merged) *)
+                    let abs_ref0 =
+                      UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs)
+                    in
+                    let abs_id0 = UnionFind.get abs_ref0 in
+                    let abs_ref1 =
+                      UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs)
+                    in
+                    let abs_id1 = UnionFind.get abs_ref1 in
+                    (* If the two ids are the same, it means the abstractions were already merged *)
+                    if abs_id0 = abs_id1 then ()
+                    else (
+                      (* We actually need to merge the abstractions *)
+
+                      (* Debug *)
+                      log#ldebug
+                        (lazy
+                          ("collapse_ctx: merging abstraction "
+                          ^ AbstractionId.to_string abs_id1
+                          ^ " into "
+                          ^ AbstractionId.to_string abs_id0
+                          ^ ":\n\n"
+                          ^ eval_ctx_to_string ~span:(Some span) !ctx));
+
+                      (* Update the environment - pay attention to the order: we
+                         we merge [abs_id1] *into* [abs_id0] *)
+                      let nctx, abs_id =
+                        merge_into_abstraction span abs_kind can_end
+                          (Some merge_funs) !ctx abs_id1 abs_id0
+                      in
+                      ctx := nctx;
+
+                      (* Update the union find *)
+                      let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in
+                      UnionFind.set abs_ref_merged abs_id))
+                  abs_ids1)
         bids)
     abs_ids;
 
@@ -441,6 +480,25 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
   (* Return the new context *)
   ctx
 
+(* Collapse two environments containing projection markers; this function is called after
+   joining environments.
+
+   The collapse is done in two steps.
+   First, we reduce the environment, merging for instance abstractions containing MB l0 _ and ML l0,
+   when both elements have the same marker, e.g., PNone, PLeft, or PRight.
+
+   Second, we merge abstractions containing the same element with left and right markers respectively.
+
+   At the end of the second step, all markers should have been removed from the resulting environment.
+*)
+let collapse_ctx (span : Meta.span) (loop_id : LoopId.id)
+    (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx)
+    : eval_ctx =
+  let ctx =
+    reduce_ctx_with_markers (Some merge_funs) span loop_id old_ids ctx0
+  in
+  collapse_ctx_markers span loop_id merge_funs old_ids ctx
+
 let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
     (loop_id : LoopId.id) (ctx : eval_ctx) : merge_duplicates_funcs =
   (* Rem.: the merge functions raise exceptions (that we catch). *)
@@ -466,9 +524,6 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
     sanity_check __FILE__ __LINE__ (is_aignored child0.value) span;
     sanity_check __FILE__ __LINE__ (is_aignored child1.value) span;
 
-    (* TODO: Handle markers *)
-    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-
     (* We need to pick a type for the avalue. The types on the left and on the
        right may use different regions: it doesn't really matter (here, we pick
        the one from the left), because we will merge those regions together
@@ -493,9 +548,6 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
         span
     in
 
-    (* TODO: Handle markers *)
-    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-
     (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let value = ABorrow (ASharedBorrow (PNone, id)) in
@@ -506,8 +558,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
     (* Sanity checks *)
     sanity_check __FILE__ __LINE__ (is_aignored child0.value) span;
     sanity_check __FILE__ __LINE__ (is_aignored child1.value) span;
-    (* TODO: Handle markers *)
-    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
+
     (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let child = child0 in
@@ -530,8 +581,6 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
     sanity_check __FILE__ __LINE__
       (not (value_has_loans_or_borrows ctx sv1.value))
       span;
-    (* TODO: Handle markers *)
-    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
 
     let ty = ty0 in
     let child = child0 in
@@ -670,10 +719,9 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
       | x -> x
     in
 
-    (* TODO: Readd this
-       let env0 = List.map (add_marker PLeft) env0 in
-       let env1 = List.map (add_marker PRight) env1 in
-    *)
+    let env0 = List.map (add_marker PLeft) env0 in
+    let env1 = List.map (add_marker PRight) env1 in
+
     List.iter check_valid env0;
     List.iter check_valid env1;
     (* Concatenate the suffixes and append the abstractions introduced while
diff --git a/compiler/Values.ml b/compiler/Values.ml
index ca33604d..c32cbc6e 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -180,6 +180,37 @@ type abstraction_id_set = AbstractionId.Set.t [@@deriving show, ord]
     For additional explanations see: https://arxiv.org/pdf/2404.02680#section.5 *)
 type proj_marker = PNone | PLeft | PRight [@@deriving show, ord]
 
+type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord]
+
+module MarkerBorrowIdOrd = struct
+  type t = marker_borrow_id
+
+  let compare = compare_marker_borrow_id
+  let to_string = show_marker_borrow_id
+  let pp_t = pp_marker_borrow_id
+  let show_t = show_marker_borrow_id
+end
+
+module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd)
+module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd)
+
+module MarkerBorrowId : sig
+  type t
+
+  val to_string : t -> string
+
+  module Set : Collections.Set with type elt = t
+  module Map : Collections.Map with type key = t
+end
+with type t = marker_borrow_id = struct
+  type t = marker_borrow_id
+
+  let to_string = show_marker_borrow_id
+
+  module Set = MarkerBorrowIdSet
+  module Map = MarkerBorrowIdMap
+end
+
 (** Ancestor for {!typed_avalue} iter visitor *)
 class ['self] iter_typed_avalue_base =
   object (self : 'self)