Make progress on environment matches and joins

7 files changed, 1104 insertions, 240 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 28caf6e6..d20a02a2 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -444,7 +444,7 @@ let give_back_symbolic_value (_config : C.config)
   | V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
     ->
       ()
-  | FunCallRet | SynthInput | Global | LoopOutput ->
+  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin ->
       raise (Failure "Unrechable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
@@ -1573,8 +1573,9 @@ let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) :
            "Can't activate a reserved mutable borrow referencing a loan inside\n\
            \         an abstraction")
 
-let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (ctx : C.eval_ctx)
-    (abs0 : V.abs) : V.abs =
+let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
+    (destructure_shared_values : bool) (ctx : C.eval_ctx) (abs0 : V.abs) : V.abs
+    =
   (* Accumulator to store the destructured values *)
   let avalues = ref [] in
   (* Utility function to store a value in the accumulator *)
@@ -1602,10 +1603,21 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (ctx : C.eval_ctx)
         | V.ASharedLoan (bids, sv, child_av) ->
             (* We don't support nested borrows for now *)
             assert (not (value_has_borrows ctx sv.V.value));
+            (* Destructure the shared value *)
+            let avl, sv =
+              if destructure_shared_values then list_values sv else ([], sv)
+            in
             (* Push a value *)
             let ignored = mk_aignored child_av.V.ty in
             let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
             push { V.value; ty };
+            (* Push the avalues introduced because we decomposed the inner loans -
+               note that we pay attention to the order in which we introduce
+               the avalues: we want to push them *after* the outer loan. If we
+               didn't want that, we would have implemented [list_values] in
+               exactly the same way as [list_avalues] (i.e., with a similar
+               signature) *)
+            List.iter push avl;
             (* Explore the child *)
             list_avalues false push_fail child_av
         | V.AMutLoan (bid, child_av) ->
@@ -1660,19 +1672,62 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (ctx : C.eval_ctx)
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
         assert (not (ty_has_borrows ctx.type_context.type_infos ty))
+  and list_values (v : V.typed_value) : V.typed_avalue list * V.typed_value =
+    let ty = v.V.ty in
+    match v.V.value with
+    | Primitive _ -> ([], v)
+    | Adt adt ->
+        let avll, field_values =
+          List.split (List.map list_values adt.field_values)
+        in
+        let avl = List.concat avll in
+        let adt = { adt with V.field_values } in
+        (avl, { v with V.value = Adt adt })
+    | Bottom -> raise (Failure "Unreachable")
+    | Borrow _ ->
+        (* We don't support nested borrows for now *)
+        raise (Failure "Unreachable")
+    | Loan lc -> (
+        match lc with
+        | SharedLoan (bids, sv) ->
+            let avl, sv = list_values sv in
+            if destructure_shared_values then
+              (* Rem.: the shared value can't contain loans nor borrows *)
+              let rty = ety_no_regions_to_rty ty in
+              let av : V.typed_avalue =
+                assert (not (value_has_loans_or_borrows ctx sv.V.value));
+                let value =
+                  V.ALoan (V.ASharedLoan (bids, sv, mk_aignored rty))
+                in
+                { V.value; ty = rty }
+              in
+              let avl = List.append avl [ av ] in
+              (avl, sv)
+            else (avl, { v with V.value = V.Loan (V.SharedLoan (bids, sv)) })
+        | MutLoan _ -> raise (Failure "Unreachable"))
+    | Symbolic _ ->
+        (* For now, we fore all symbolic values containing borrows to be eagerly
+           expanded *)
+        assert (not (ty_has_borrows ctx.type_context.type_infos ty));
+        ([], v)
   in
+
   (* Destructure the avalues *)
   List.iter (list_avalues true push_avalue) abs0.V.avalues;
   let avalues = List.rev !avalues in
   (* Update *)
   { abs0 with V.avalues; kind = abs_kind; can_end }
 
-let abs_is_destructured (ctx : C.eval_ctx) (abs : V.abs) : bool =
-  let abs' = destructure_abs abs.kind abs.can_end ctx abs in
+let abs_is_destructured (destructure_shared_values : bool) (ctx : C.eval_ctx)
+    (abs : V.abs) : bool =
+  let abs' =
+    destructure_abs abs.kind abs.can_end destructure_shared_values ctx abs
+  in
   abs = abs'
 
 let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
-    (ctx : C.eval_ctx) (v : V.typed_value) : V.abs list =
+    (destructure_shared_values : bool) (ctx : C.eval_ctx) (v : V.typed_value) :
+    V.abs list =
   (* Convert the value to a list of avalues *)
   let absl = ref [] in
   let push_abs (r_id : T.RegionId.id) (avalues : V.typed_avalue list) : unit =
@@ -1697,32 +1752,52 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
       absl := abs :: !absl
   in
 
-  (* [group]: group in one abstraction (because we dived into a borrow/loan) *)
-  let rec to_avalues (allow_borrows : bool) (group : bool)
-      (r_id : T.RegionId.id) (v : V.typed_value) : V.typed_avalue list =
+  (* [group]: group in one abstraction (because we dived into a borrow/loan)
+
+     We return one typed-value for the shared values: when we encounter a shared
+     loan, we need to compute the value which will be shared. If [destructure_shared_values]
+     is [true], this shared value will be stripped of its shared loans.
+  *)
+  let rec to_avalues (allow_borrows : bool) (inside_borrowed : bool)
+      (group : bool) (r_id : T.RegionId.id) (v : V.typed_value) :
+      V.typed_avalue list * V.typed_value =
     let ty = v.V.ty in
     match v.V.value with
-    | V.Primitive _ -> []
+    | V.Primitive _ -> ([], v)
     | V.Bottom ->
         (* Can happen: we *do* convert dummy values to abstractions, and dummy
            values can contain bottoms *)
-        []
+        ([], v)
     | V.Adt adt ->
         (* Two cases, depending on whether we have to group all the borrows/loans
            inside one abstraction or not *)
-        if group then
-          (* Convert to avalues, and transmit to the parent *)
-          List.concat
-            (List.map (to_avalues allow_borrows group r_id) adt.field_values)
-        else (
-          (* Create one abstraction per field, and transmit nothing to the parent *)
-          List.iter
-            (fun fv ->
-              let r_id = C.fresh_region_id () in
-              let values = to_avalues allow_borrows group r_id fv in
-              push_abs r_id values)
-            adt.field_values;
-          [])
+        let avl, field_values =
+          if group then
+            (* Convert to avalues, and transmit to the parent *)
+            let avl, field_values =
+              List.split
+                (List.map
+                   (to_avalues allow_borrows inside_borrowed group r_id)
+                   adt.field_values)
+            in
+            (List.concat avl, field_values)
+          else
+            (* Create one abstraction per field, and transmit nothing to the parent *)
+            let field_values =
+              List.map
+                (fun fv ->
+                  let r_id = C.fresh_region_id () in
+                  let avl, fv =
+                    to_avalues allow_borrows inside_borrowed group r_id fv
+                  in
+                  push_abs r_id avl;
+                  fv)
+                adt.field_values
+            in
+            ([], field_values)
+        in
+        let adt = { adt with field_values } in
+        (avl, { v with V.value = V.Adt adt })
     | V.Borrow bc -> (
         let _, ref_ty, kind = ty_as_ref ty in
         (* Sanity check *)
@@ -1733,21 +1808,30 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
             let ref_ty = ety_no_regions_to_rty ref_ty in
             let ty = T.Ref (T.Var r_id, ref_ty, kind) in
             let value = V.ABorrow (V.ASharedBorrow bid) in
-            [ { V.value; ty } ]
+            ([ { V.value; ty } ], v)
         | MutBorrow (bid, bv) ->
             let r_id = if group then r_id else C.fresh_region_id () in
             (* We don't support nested borrows for now *)
             assert (not (value_has_borrows ctx bv.V.value));
-            (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+            (* We don't allow shared borrows inside mutably borrowed values -
+               note that destructuring those is unsoud: if we immutably borrow
+               a value inside a mutably borrowed value, we have to make sure
+               the immutably borrowed value isn't modified for as long as the
+               immutable borrow lives. In case of shared values it is not
+               a problem, because this is enforced by the outer shared loan. *)
+            assert (not (value_has_loans bv.V.value));
+            (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
             let mv = bv in
             let ref_ty = ety_no_regions_to_rty ref_ty in
             let ty = T.Ref (T.Var r_id, ref_ty, kind) in
             let ignored = mk_aignored ref_ty in
-            let value = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
-            let value = { V.value; ty } in
+            let av = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
+            let av = { V.value = av; ty } in
             (* Continue exploring, looking for loans (and forbidding borrows,
                because we don't support nested borrows for now) *)
-            value :: to_avalues false true r_id bv
+            let avl, bv = to_avalues false true true r_id bv in
+            let value = { v with V.value = V.Borrow (V.MutBorrow (bid, bv)) } in
+            (av :: avl, value)
         | ReservedMutBorrow _ ->
             (* This borrow should have been activated *)
             raise (Failure "Unexpected"))
@@ -1758,58 +1842,134 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
             (* We don't support nested borrows for now *)
             assert (not (value_has_borrows ctx sv.V.value));
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+            (* For avalues, a loan has the borrow type *)
             let ty = ety_no_regions_to_rty ty in
+            let ty = mk_ref_ty (T.Var r_id) ty T.Shared in
             let ignored = mk_aignored ty in
-            let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
-            let value = { V.value; ty } in
+            (* Rem.: the shared value might contain loans *)
+            let avl, sv = to_avalues false true true r_id sv in
+            let av = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
+            let av = { V.value = av; ty } in
             (* Continue exploring, looking for loans (and forbidding borrows,
                because we don't support nested borrows for now) *)
-            value :: to_avalues false true r_id sv
+            let value : V.value =
+              if destructure_shared_values then sv.V.value
+              else V.Loan (V.SharedLoan (bids, sv))
+            in
+            let value = { v with V.value } in
+            (av :: avl, value)
         | V.MutLoan bid ->
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+            (* For avalues, a loan has the borrow type *)
             let ty = ety_no_regions_to_rty ty in
+            let ty = mk_ref_ty (T.Var r_id) ty T.Mut in
             let ignored = mk_aignored ty in
-            let value = V.ALoan (V.AMutLoan (bid, ignored)) in
-            [ { V.value; ty } ])
+            let av = V.ALoan (V.AMutLoan (bid, ignored)) in
+            let av = { V.value = av; ty } in
+            ([ av ], v))
     | V.Symbolic _ ->
         (* For now, we force all the symbolic values containing borrows to
            be eagerly expanded, and we don't support nested borrows *)
         assert (not (value_has_borrows ctx v.V.value));
         (* Return nothing *)
-        []
+        ([], v)
   in
   (* Generate the avalues *)
   let r_id = C.fresh_region_id () in
-  let values = to_avalues true false r_id v in
+  let values, _ = to_avalues true false false r_id v in
   (* Introduce an abstraction for the returned values *)
   push_abs r_id values;
   (* Return *)
   List.rev !absl
 
-let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
-    (ctx : C.eval_ctx) (abs0 : V.abs) (abs1 : V.abs) : V.abs =
-  (* Check that the abstractions are destructured *)
-  if !Config.check_invariants then (
-    assert (abs_is_destructured ctx abs0);
-    assert (abs_is_destructured ctx abs1));
+type borrow_or_loan_id = BorrowId of V.borrow_id | LoanId of V.loan_id
+
+type g_loan_content_with_ty =
+  (T.ety * V.loan_content, T.rty * V.aloan_content) concrete_or_abs
+
+type g_borrow_content_with_ty =
+  (T.ety * V.borrow_content, T.rty * V.aborrow_content) concrete_or_abs
+
+type merge_abstraction_info = {
+  loans : V.loan_id_set;
+  borrows : V.borrow_id_set;
+  borrows_loans : 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 V.BorrowId.Map.t;
+  borrow_to_content : g_borrow_content_with_ty V.BorrowId.Map.t;
+}
 
-  (* Visit the abstractions, list their borrows and loans *)
-  let borrows = ref V.BorrowId.Set.empty in
-  let loans = ref V.BorrowId.Set.empty in
+(** Small utility to help merging abstractions.
 
-  let push_loans ids = loans := V.BorrowId.Set.union !loans ids in
-  let push_loan id = loans := V.BorrowId.Set.add id !loans in
-  let push_borrow id = borrows := V.BorrowId.Set.add id !borrows in
+    We compute the list of loan/borrow contents, maps from borrow/loan ids
+    to borrow/loan contents, etc.
+
+    Note that this function is very specific to [merge_abstractions]: we
+    have strong assumptions about the shape of the abstraction, and in
+    particular that:
+    - its values don't contain nested borrows
+    - all the borrows are destructured (for instance, shared loans can't
+      contain shared loans).
+ *)
+let compute_merge_abstractions_info (ctx : C.eval_ctx) (abs : V.abs) :
+    merge_abstraction_info =
+  let loans : V.loan_id_set ref = ref V.BorrowId.Set.empty in
+  let borrows : V.borrow_id_set ref = ref V.BorrowId.Set.empty in
+  let borrows_loans : borrow_or_loan_id list ref = ref [] in
+  let loan_to_content : g_loan_content_with_ty V.BorrowId.Map.t ref =
+    ref V.BorrowId.Map.empty
+  in
+  let borrow_to_content : g_borrow_content_with_ty V.BorrowId.Map.t ref =
+    ref V.BorrowId.Map.empty
+  in
+
+  let push_loans ids (lc : g_loan_content_with_ty) : unit =
+    assert (V.BorrowId.Set.disjoint !loans ids);
+    loans := V.BorrowId.Set.union !loans ids;
+    V.BorrowId.Set.iter
+      (fun id ->
+        assert (not (V.BorrowId.Map.mem id !loan_to_content));
+        loan_to_content := V.BorrowId.Map.add id lc !loan_to_content;
+        borrows_loans := LoanId id :: !borrows_loans)
+      ids
+  in
+  let push_loan id (lc : g_loan_content_with_ty) : unit =
+    assert (not (V.BorrowId.Set.mem id !loans));
+    loans := V.BorrowId.Set.add id !loans;
+    assert (not (V.BorrowId.Map.mem id !loan_to_content));
+    loan_to_content := V.BorrowId.Map.add id lc !loan_to_content;
+    borrows_loans := LoanId id :: !borrows_loans
+  in
+  let push_borrow id (bc : g_borrow_content_with_ty) : unit =
+    assert (not (V.BorrowId.Set.mem id !borrows));
+    borrows := V.BorrowId.Set.add id !borrows;
+    assert (not (V.BorrowId.Map.mem id !borrow_to_content));
+    borrow_to_content := V.BorrowId.Map.add id bc !borrow_to_content;
+    borrows_loans := BorrowId id :: !borrows_loans
+  in
 
   let iter_avalues =
     object
       inherit [_] V.iter_typed_avalue as super
 
+      (** We redefine this to track the types *)
+      method! visit_typed_avalue _ v =
+        super#visit_typed_avalue (Some (Abstract v.V.ty)) v
+
+      (** We redefine this to track the types *)
+      method! visit_typed_value _ (v : V.typed_value) =
+        super#visit_typed_value (Some (Concrete v.V.ty)) v
+
       method! visit_loan_content env lc =
         (* Can happen if we explore shared values whose sub-values are
            reborrowed *)
+        let ty =
+          match Option.get env with
+          | Concrete ty -> ty
+          | Abstract _ -> raise (Failure "Unreachable")
+        in
         (match lc with
-        | SharedLoan (bids, _) -> push_loans bids
+        | SharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
         | MutLoan _ -> raise (Failure "Unreachable"));
         (* Continue *)
         super#visit_loan_content env lc
@@ -1820,10 +1980,15 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
         raise (Failure "Unreachable")
 
       method! visit_aloan_content env lc =
+        let ty =
+          match Option.get env with
+          | Concrete _ -> raise (Failure "Unreachable")
+          | Abstract ty -> ty
+        in
         (* Register the loans *)
         (match lc with
-        | V.ASharedLoan (bids, _, _) -> push_loans bids
-        | V.AMutLoan (bid, _) -> push_loan bid
+        | V.ASharedLoan (bids, _, _) -> push_loans bids (Abstract (ty, lc))
+        | V.AMutLoan (bid, _) -> push_loan bid (Abstract (ty, lc))
         | V.AEndedMutLoan _ | V.AEndedSharedLoan _ | V.AIgnoredMutLoan _
         | V.AEndedIgnoredMutLoan _ | V.AIgnoredSharedLoan _ ->
             (* The abstraction has been destructured, so those shouldn't appear *)
@@ -1832,14 +1997,19 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
         super#visit_aloan_content env lc
 
       method! visit_aborrow_content env bc =
+        let ty =
+          match Option.get env with
+          | Concrete _ -> raise (Failure "Unreachable")
+          | Abstract ty -> ty
+        in
         (* Explore the borrow content *)
         (match bc with
-        | V.AMutBorrow (_, bid, _) -> push_borrow bid
-        | V.ASharedBorrow bid -> push_borrow bid
+        | V.AMutBorrow (_, bid, _) -> push_borrow bid (Abstract (ty, bc))
+        | V.ASharedBorrow bid -> push_borrow bid (Abstract (ty, bc))
         | V.AProjSharedBorrow asb ->
             let register asb =
               match asb with
-              | V.AsbBorrow bid -> push_borrow bid
+              | V.AsbBorrow bid -> push_borrow bid (Abstract (ty, bc))
               | V.AsbProjReborrows _ ->
                   (* Can only happen if the symbolic value (potentially) contains
                      borrows - i.e., we have nested borrows *)
@@ -1854,131 +2024,290 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
 
       method! visit_symbolic_value _ _ =
         (* Sanity check *)
-        raise (Failure "Unrechable")
+        raise (Failure "Unreachable")
     end
   in
 
-  List.iter (iter_avalues#visit_typed_avalue ()) abs0.V.avalues;
-  List.iter (iter_avalues#visit_typed_avalue ()) abs1.V.avalues;
+  List.iter (iter_avalues#visit_typed_avalue None) abs.V.avalues;
+
+  {
+    loans = !loans;
+    borrows = !borrows;
+    borrows_loans = List.rev !borrows_loans;
+    loan_to_content = !loan_to_content;
+    borrow_to_content = !borrow_to_content;
+  }
+
+type merge_duplicates_funcs = {
+  merge_amut_borrows :
+    V.borrow_id ->
+    T.rty ->
+    V.mvalue ->
+    V.typed_avalue ->
+    T.rty ->
+    V.mvalue ->
+    V.typed_avalue ->
+    V.typed_avalue;
+  merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+  merge_amut_loans :
+    V.loan_id ->
+    T.rty ->
+    V.typed_avalue ->
+    T.rty ->
+    V.typed_avalue ->
+    V.typed_avalue;
+  merge_ashared_loans :
+    V.loan_id_set ->
+    T.rty ->
+    V.typed_value ->
+    T.rty ->
+    V.typed_value ->
+    V.typed_avalue;
+}
+
+let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
+    (merge_funs : merge_duplicates_funcs option) (ctx : C.eval_ctx)
+    (abs0 : V.abs) (abs1 : V.abs) : V.abs =
+  (* Check that the abstractions are destructured *)
+  if !Config.check_invariants then (
+    let destructure_shared_values = true in
+    assert (abs_is_destructured destructure_shared_values ctx abs0);
+    assert (abs_is_destructured destructure_shared_values ctx abs1));
+
+  (* Compute the relevant information *)
+  let {
+    loans = loans0;
+    borrows = borrows0;
+    borrows_loans = borrows_loans0;
+    loan_to_content = loan_to_content0;
+    borrow_to_content = borrow_to_content0;
+  } =
+    compute_merge_abstractions_info ctx abs0
+  in
 
-  (* List the values, ignoring the loans/borrows which whose associated
-     borrows/loans are in the other abstraction already - note that we
-     take advantage of the fact that the values are destructured.
+  let {
+    loans = loans1;
+    borrows = borrows1;
+    borrows_loans = borrows_loans1;
+    loan_to_content = loan_to_content1;
+    borrow_to_content = borrow_to_content1;
+  } =
+    compute_merge_abstractions_info ctx abs1
+  in
 
-     We convert the loans/borrows we want to ignore to [Ignored] values,
-     then filter them.
+  (* Sanity check: there is no loan/borrows which appears in both abstractions,
+     unless we allow to merge duplicates *)
+  if merge_funs = None then (
+    assert (V.BorrowId.Set.disjoint borrows0 borrows1);
+    assert (V.BorrowId.Set.disjoint loans0 loans1));
+
+  (* Merge.
+     There are several cases:
+     - if a borrow/loan is only in one abstraction, we simply check if we need
+       to filter it (because its associated loan/borrow is in the other
+       abstraction).
+     - if a borrow/loan is present in both abstractions, we need to merge its
+       content.
+
+     Note that it is possible that we may need to merge strictly more than 2 avalues,
+     because of shared loans. For instance, if we have:
+     {[
+       abs'0 { shared_loan { l0, l1 } ... }
+       abs'1 { shared_loan { l0 } ..., shared_loan { l1 } ... }
+     ]}
+
+     We ignore this case for now: we check that whenever we merge two shared loans,
+     then their sets of ids are equal.
   *)
-  let intersect = V.BorrowId.Set.inter !loans !borrows in
-  let filter_bids (bids : V.BorrowId.Set.t) : V.BorrowId.Set.t option =
+  let merged_borrows = ref V.BorrowId.Set.empty in
+  let merged_loans = ref V.BorrowId.Set.empty in
+  let avalues = ref [] in
+  let push_avalue av = avalues := av :: !avalues in
+
+  let intersect =
+    V.BorrowId.Set.union
+      (V.BorrowId.Set.inter loans0 borrows1)
+      (V.BorrowId.Set.inter loans1 borrows0)
+  in
+  let filter_bids (bids : V.BorrowId.Set.t) : V.BorrowId.Set.t =
     let bids = V.BorrowId.Set.diff bids intersect in
-    if V.BorrowId.Set.is_empty bids then None else Some bids
+    assert (not (V.BorrowId.Set.is_empty bids));
+    bids
   in
   let filter_bid (bid : V.BorrowId.id) : V.BorrowId.id option =
     if V.BorrowId.Set.mem bid intersect then None else Some bid
   in
 
-  let map_avalues =
-    object (self : 'self)
-      inherit [_] V.map_typed_avalue as super
-
-      method! visit_Loan env lc =
-        (* Can happen if we explore shared values whose sub-values are
-           reborrowed *)
-        match lc with
-        | SharedLoan (bids, sv) -> (
-            match filter_bids bids with
-            | None -> (self#visit_typed_value env sv).V.value
-            | Some bids -> super#visit_Loan env (SharedLoan (bids, sv)))
-        | MutLoan _ -> raise (Failure "Unreachable")
+  let borrow_is_merged id = V.BorrowId.Set.mem id !merged_borrows in
+  let set_borrow_as_merged id =
+    merged_borrows := V.BorrowId.Set.add id !merged_borrows
+  in
+  let loan_is_merged id = V.BorrowId.Set.mem id !merged_loans in
+  let set_loan_as_merged id =
+    merged_loans := V.BorrowId.Set.add id !merged_loans
+  in
 
-      method! visit_borrow_content _ _ =
-        (* Can happen if we explore shared values which contain borrows -
-           i.e., if we have nested borrows (we forbid this for now) *)
+  (* Some utility functions *)
+  (* Merge two aborrow contents - note that those contents must have the same id *)
+  let merge_aborrow_contents (ty0 : T.rty) (bc0 : V.aborrow_content)
+      (ty1 : T.rty) (bc1 : V.aborrow_content) : V.typed_avalue =
+    match (bc0, bc1) with
+    | V.AMutBorrow (mv0, id, child0), V.AMutBorrow (mv1, _, child1) ->
+        (Option.get merge_funs).merge_amut_borrows id ty0 mv0 child0 ty1 mv1
+          child1
+    | ASharedBorrow id, ASharedBorrow _ ->
+        (Option.get merge_funs).merge_ashared_borrows id ty0 ty1
+    | AProjSharedBorrow _, AProjSharedBorrow _ ->
+        (* Unreachable because requires nested borrows *)
         raise (Failure "Unreachable")
+    | _ ->
+        (* Unreachable because those cases are ignored (ended/ignored borrows)
+           or inconsistent *)
+        raise (Failure "Unreachable")
+  in
 
-      method! visit_ALoan env lc =
-        (* Register the loans *)
-        match lc with
-        | V.ASharedLoan (bids, sv, asv) -> (
-            match filter_bids bids with
-            | None ->
-                let sv = super#visit_typed_value env sv in
-                assert (is_aignored asv.V.value);
-                (* Check if the shared value contains loans or borrows - rem.: there shouldn't
-                   be borrows actually, because for now we forbid nested borrows.
-
-                   If it doesn't, we can ignore the value altogether.
-                *)
-                if
-                  loans_in_value sv
-                  || ty_has_borrows ctx.type_context.type_infos sv.V.ty
-                then
-                  (* The value is not shared anymore, but it contains shared sub-values.
-
-                     It would be good to deconstruct the sub-values. For now, let's fail
-                     (rem.: it would be sound to have a shared aloan with an empty set
-                     of borrow ids).
-                  *)
-                  raise (Failure "Unimplemented")
-                else V.AIgnored
-            | Some bids -> super#visit_ALoan env (ASharedLoan (bids, sv, asv)))
-        | V.AMutLoan (bid, child) -> (
-            assert (is_aignored child.V.value);
-            match filter_bid bid with
-            | None -> V.AIgnored
-            | Some _ -> super#visit_ALoan env lc)
-        | V.AEndedMutLoan _ | V.AEndedSharedLoan _ | V.AIgnoredMutLoan _
-        | V.AEndedIgnoredMutLoan _ | V.AIgnoredSharedLoan _ ->
-            (* The abstraction has been destructured, so those shouldn't appear *)
-            raise (Failure "Unreachable")
-
-      method! visit_ABorrow env bc =
-        (* Explore the borrow content *)
-        match bc with
-        | V.AMutBorrow (_, bid, child) -> (
-            assert (is_aignored child.V.value);
-            match filter_bid bid with
-            | None -> V.AIgnored
-            | Some _ -> super#visit_ABorrow env bc)
-        | V.ASharedBorrow bid -> (
-            match filter_bid bid with
-            | None -> V.AIgnored
-            | Some _ -> super#visit_ABorrow env bc)
-        | V.AProjSharedBorrow asb ->
-            let filter asb =
-              match asb with
-              | V.AsbBorrow bid -> (
-                  match filter_bid bid with None -> None | Some _ -> Some asb)
-              | V.AsbProjReborrows _ ->
-                  (* Can only happen if the symbolic value (potentially) contains
-                     borrows - i.e., we have nested borrows *)
-                  raise (Failure "Unreachable")
-            in
-            let asb = List.filter_map filter asb in
-            V.ABorrow (V.AProjSharedBorrow asb)
-        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
-        | V.AEndedMutBorrow _ | V.AEndedSharedBorrow ->
-            (* The abstraction has been destructured, so those shouldn't appear *)
-            raise (Failure "Unreachable")
-
-      method! visit_symbolic_value _ _ =
-        (* Sanity check *)
-        raise (Failure "Unrechable")
-    end
+  let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
+      (bc1 : g_borrow_content_with_ty) : V.typed_avalue =
+    match (bc0, bc1) with
+    | Concrete (ty0, bc0), Concrete (ty1, bc1) ->
+        (* This can happen only in case of nested borrows *)
+        raise (Failure "Unreachable")
+    | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
+        merge_aborrow_contents ty0 bc0 ty1 bc1
+    | Concrete _, Abstract _ | Abstract _, Concrete _ ->
+        (* TODO: is it really unreachable? *)
+        raise (Failure "Unreachable")
   in
 
-  (* Apply the transformation *)
-  let avalues =
-    List.map
-      (map_avalues#visit_typed_avalue ())
-      (List.append abs0.avalues abs1.avalues)
+  let merge_aloan_contents (ty0 : T.rty) (lc0 : V.aloan_content) (ty1 : T.rty)
+      (lc1 : V.aloan_content) : V.typed_avalue =
+    match (lc0, lc1) with
+    | V.AMutLoan (id, child0), V.AMutLoan (_, child1) ->
+        (* Register the loan id *)
+        set_loan_as_merged id;
+        (* Merge *)
+        (Option.get merge_funs).merge_amut_loans id ty0 child0 ty1 child1
+    | ASharedLoan (ids0, sv0, child0), ASharedLoan (ids1, sv1, child1) ->
+        (* 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 *)
+        assert (ids0 = ids1);
+        let ids = ids0 in
+        assert (not (V.BorrowId.Set.is_empty ids));
+        (* Register the loan ids *)
+        V.BorrowId.Set.iter set_loan_as_merged ids;
+        (* Merge *)
+        (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 ty1 sv1
+    | _ ->
+        (* Unreachable because those cases are ignored (ended/ignored borrows)
+           or inconsistent *)
+        raise (Failure "Unreachable")
   in
 
-  (* Filter the ignored values *)
-  let avalues =
-    List.filter (fun (v : V.typed_avalue) -> not (is_aignored v.value)) avalues
+  (* 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) : V.typed_avalue =
+    match (lc0, lc1) with
+    | Concrete _, Concrete _ ->
+        (* This can not happen: the values should have been destructured *)
+        raise (Failure "Unreachable")
+    | Abstract (ty0, lc0), Abstract (ty1, lc1) ->
+        merge_aloan_contents ty0 lc0 ty1 lc1
+    | Concrete _, Abstract _ | Abstract _, Concrete _ ->
+        (* TODO: is it really unreachable? *)
+        raise (Failure "Unreachable")
   in
 
+  let borrows_loans = List.append borrows_loans0 borrows_loans1 in
+  (* Iterate over all the borrows/loans ids found in teh abstractions *)
+  List.iter
+    (fun bl ->
+      match bl with
+      | BorrowId bid -> (
+          (* Check if the borrow has already been merged *)
+          assert (not (borrow_is_merged bid));
+          set_borrow_as_merged bid;
+          (* Check if we need to filter it *)
+          match filter_bid bid with
+          | None -> ()
+          | Some bid ->
+              (* Lookup the contents *)
+              let bc0 = V.BorrowId.Map.find_opt bid borrow_to_content0 in
+              let bc1 = V.BorrowId.Map.find_opt bid borrow_to_content1 in
+              (* Merge *)
+              let av : V.typed_avalue =
+                match (bc0, bc1) with
+                | None, Some bc | Some bc, None -> (
+                    match bc with
+                    | Concrete (_, _) ->
+                        (* This can happen only in case of nested borrows -
+                           a concrete borrow can only happen inside a shared
+                           loan
+                        *)
+                        raise (Failure "Unreachable")
+                    | Abstract (ty, bc) -> { V.value = V.ABorrow bc; ty })
+                | Some bc0, Some bc1 ->
+                    assert (merge_funs <> None);
+                    merge_g_borrow_contents bc0 bc1
+                | None, None -> raise (Failure "Unreachable")
+              in
+              push_avalue av)
+      | LoanId bid -> (
+          if
+            (* Check if the loan has already been treated - it can happen
+               because shared loans contain sets of borrows.
+            *)
+            loan_is_merged bid
+          then ()
+          else
+            (* Check if we need to filter it *)
+            match filter_bid bid with
+            | None -> ()
+            | Some bid ->
+                (* Lookup the contents *)
+                let lc0 = V.BorrowId.Map.find_opt bid loan_to_content0 in
+                let lc1 = V.BorrowId.Map.find_opt bid loan_to_content1 in
+                (* Merge *)
+                let av : V.typed_avalue =
+                  match (lc0, lc1) with
+                  | None, Some lc | Some lc, None -> (
+                      match lc with
+                      | Concrete _ ->
+                          (* This shouldn't happen because the avalues should
+                             have been destructured. *)
+                          raise (Failure "Unreachable")
+                      | Abstract (ty, lc) -> (
+                          match lc with
+                          | V.ASharedLoan (bids, sv, child) ->
+                              let bids = filter_bids bids in
+                              assert (not (V.BorrowId.Set.is_empty bids));
+                              assert (is_aignored child.V.value);
+                              assert (
+                                not (value_has_loans_or_borrows ctx sv.V.value));
+                              let lc = V.ASharedLoan (bids, sv, child) in
+                              { V.value = V.ALoan lc; ty }
+                          | V.AMutLoan _ -> { V.value = V.ALoan lc; ty }
+                          | V.AEndedMutLoan _ | V.AEndedSharedLoan _
+                          | V.AIgnoredMutLoan _ | V.AEndedIgnoredMutLoan _
+                          | V.AIgnoredSharedLoan _ ->
+                              (* The abstraction has been destructured, so those shouldn't appear *)
+                              raise (Failure "Unreachable")))
+                  | Some lc0, Some lc1 ->
+                      assert (merge_funs <> None);
+                      merge_g_loan_contents lc0 lc1
+                  | None, None -> raise (Failure "Unreachable")
+                in
+                push_avalue av))
+    borrows_loans;
+
+  (* Reverse the values *)
+  let avalues = List.rev !avalues in
+
   (* Create the new abstraction *)
   let abs_id = C.fresh_abstraction_id () in
   (* Note that one of the two abstractions might a parent of the other *)
@@ -2005,6 +2334,6 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
     }
   in
   (* Sanity check *)
-  if !Config.check_invariants then assert (abs_is_destructured ctx abs);
+  if !Config.check_invariants then assert (abs_is_destructured true ctx abs);
   (* Return *)
   abs
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 0d1be9c2..8b8b76d9 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -70,21 +70,37 @@ val promote_reserved_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
     ]}
 
     Rem.: we do this to simplify the merging of abstractions. We can do this
-    because for now, we don't support nested borrows.
+    because for now we don't support nested borrows. In order to implement
+    support for nested borrows, we will probably need to maintain the structure
+    of the avalues.
 
     Paramters:
     - [abs_kind]
     - [can_end]
+    - [destructure_shared_values]: if [true], explore shared values and whenever we find
+      a shared loan, move it elsewhere by replacing it with the same value without
+      the shared loan, and adding another ashared loan in the abstraction.
+      For instance:
+      {[
+         ML {l0} (0, ML {l1} 1)
+
+         ~~>
+
+         ML {l0} (0, 1)
+         ML {l1} 1
+      ]}
     - [ctx]
     - [abs]
  *)
-val destructure_abs : V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs
+val destructure_abs : V.abs_kind -> bool -> bool -> C.eval_ctx -> V.abs -> V.abs
 
 (** Return [true] if the values in an abstraction are destructured.
 
     We simply destructure it and check that it gives the identity.
+
+    The input boolean is [destructure_shared_value]. See {!destructure_abs}.
  *)
-val abs_is_destructured : C.eval_ctx -> V.abs -> bool
+val abs_is_destructured : bool -> C.eval_ctx -> V.abs -> bool
 
 (** Turn a value into a abstractions.
 
@@ -104,20 +120,54 @@ val abs_is_destructured : C.eval_ctx -> V.abs -> bool
     Parameters:
     - [abs_kind]
     - [can_end]
+    - [destructure_shared_values]: this is similar to [destructure_shared_values]
+      for {!destructure_abs}.
     - [ctx]
     - [v]
  *)
 val convert_value_to_abstractions :
-  V.abs_kind -> bool -> C.eval_ctx -> V.typed_value -> V.abs list
+  V.abs_kind -> bool -> bool -> C.eval_ctx -> V.typed_value -> V.abs list
+
+(** See {!merge_abstractions}.
+
+    Rem.: it may be more idiomatic to have a functor, but this seems a bit
+    heavyweight, though.
+  *)
+type merge_duplicates_funcs = {
+  merge_amut_borrows :
+    V.borrow_id ->
+    T.rty ->
+    V.mvalue ->
+    V.typed_avalue ->
+    T.rty ->
+    V.mvalue ->
+    V.typed_avalue ->
+    V.typed_avalue;
+  merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+  merge_amut_loans :
+    V.loan_id ->
+    T.rty ->
+    V.typed_avalue ->
+    T.rty ->
+    V.typed_avalue ->
+    V.typed_avalue;
+  merge_ashared_loans :
+    V.loan_id_set ->
+    T.rty ->
+    V.typed_value ->
+    T.rty ->
+    V.typed_value ->
+    V.typed_avalue;
+}
 
 (** Merge two abstractions together.
 
-    Merging two abstractions together implies removing the loans/borrows
+    When we merge two abstractions together, we remove the loans/borrows
     which appear in one and whose associated loans/borrows appear in the
     other. For instance:
     {[
-      abs'0 { mut_borrow l0, mut_loan l1 }
-      abs'1 { mut_borrow l1, mut_borrow l2 }
+      abs'0 { mut_borrow l0, mut_loan l1 }   // Rem.: mut_loan l1
+      abs'1 { mut_borrow l1, mut_borrow l2 } // Rem.: mut_borrow l1
 
           ~~>
 
@@ -127,9 +177,27 @@ val convert_value_to_abstractions :
     Parameters:
     - [kind]
     - [can_end]
+    - [merge_funs]: in the case it can happen that a loan or a borrow appears in
+      both abstractions, we use those functions to merge the different occurrences
+      (such things can happen when joining environments: we might temporarily
+      duplicate borrows during the join, before merging those borrows together).
+      For instance, this happens for the following abstractions is forbidden:
+      {[
+        abs'0 { mut_borrow l0, mut_loan l1 } // mut_borrow l0 !
+        abs'1 { mut_borrow l0, mut_loan l2 } // mut_borrow l0 !
+      ]}
+      If you want to forbid this, provide [None]. In that case, [merge_abstractions]
+      actually simply performs some sort of a union.
+
     - [ctx]
     - [abs0]
     - [abs1]
  *)
 val merge_abstractions :
-  V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs -> V.abs
+  V.abs_kind ->
+  bool ->
+  merge_duplicates_funcs option ->
+  C.eval_ctx ->
+  V.abs ->
+  V.abs ->
+  V.abs
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 8d23e4da..54949d3f 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -617,6 +617,20 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
     None
   with FoundLoanContent lc -> Some lc
 
+(** Return the first loan we find in a list of values *)
+let get_first_loan_in_values (vs : V.typed_value list) : V.loan_content option =
+  let obj =
+    object
+      inherit [_] V.iter_typed_value
+      method! visit_loan_content _ lc = raise (FoundLoanContent lc)
+    end
+  in
+  (* We use exceptions *)
+  try
+    List.iter (obj#visit_typed_value ()) vs;
+    None
+  with FoundLoanContent lc -> Some lc
+
 (** Return the first borrow we find in a value *)
 let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option =
   let obj =
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 08607deb..002abfb5 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -49,11 +49,11 @@ let mk_match_ctx (ctx : C.eval_ctx) : match_ctx =
   { ctx; aids; sids; bids }
 
 type updt_env_kind =
-  | EndAbsInSrc of V.AbstractionId.id
-  | EndBorrowsInSrc of V.BorrowId.Set.t
-  | EndBorrowInSrc of V.BorrowId.id
-  | EndBorrowInTgt of V.BorrowId.id
-  | EndBorrowsInTgt of V.BorrowId.Set.t
+  | AbsInLeft of V.AbstractionId.id
+  | LoanInLeft of V.BorrowId.id
+  | LoansInLeft of V.BorrowId.Set.t
+  | LoanInRight of V.BorrowId.id
+  | LoansInRight of V.BorrowId.Set.t
 
 (** Utility exception *)
 exception ValueMatchFailure of updt_env_kind
@@ -63,43 +63,87 @@ type joined_ctx_or_update = (match_ctx, updt_env_kind) result
 (** Union Find *)
 module UnionFind = UF.Make (UF.StoreMap)
 
-(** A small utility *)
+(** A small utility -
+
+    Rem.: some environments may be ill-formed (they may contain several times
+    the same loan or borrow - this happens for instance when merging
+    environments). This is the reason why we use sets in some places (for
+    instance, [borrow_to_abs] maps to a *set* of ids).
+*)
 type abs_borrows_loans_maps = {
   abs_ids : V.AbstractionId.id list;
   abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t;
   abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
-  borrow_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
-  loan_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
+  abs_to_borrows_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
+  borrow_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
+  loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
+  borrow_loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
 }
 
 (** Compute various maps linking the abstractions and the borrows/loans they contain.
 
     The [explore] function is used to filter abstractions.
+
+    [no_duplicates] checks that borrows/loans are not referenced more than once
+    (see the documentation for {!abs_borrows_loans_maps}).
  *)
-let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
-    abs_borrows_loans_maps =
+let compute_abs_borrows_loans_maps (no_duplicates : bool)
+    (explore : V.abs -> bool) (env : C.env) : abs_borrows_loans_maps =
   let abs_ids = ref [] in
   let abs_to_borrows = ref V.AbstractionId.Map.empty in
   let abs_to_loans = ref V.AbstractionId.Map.empty in
+  let abs_to_borrows_loans = ref V.AbstractionId.Map.empty in
   let borrow_to_abs = ref V.BorrowId.Map.empty in
   let loan_to_abs = ref V.BorrowId.Map.empty in
+  let borrow_loan_to_abs = ref V.BorrowId.Map.empty in
 
+  let module R (Id0 : Identifiers.Id) (Id1 : Identifiers.Id) = struct
+    (*
+       [check_singleton_sets]: check that the mapping maps to a singletong.
+       [check_not_already_registered]: check if the mapping was not already registered.
+    *)
+    let register_mapping (check_singleton_sets : bool)
+        (check_not_already_registered : bool) (map : Id1.Set.t Id0.Map.t ref)
+        (id0 : Id0.id) (id1 : Id1.id) : unit =
+      (* Sanity check *)
+      (if check_singleton_sets || check_not_already_registered then
+       match Id0.Map.find_opt id0 !map with
+       | None -> ()
+       | Some set ->
+           assert (
+             (not check_not_already_registered) || not (Id1.Set.mem id1 set)));
+      (* Update the mapping *)
+      map :=
+        Id0.Map.update id0
+          (fun ids ->
+            match ids with
+            | None -> Some (Id1.Set.singleton id1)
+            | Some ids ->
+                (* Sanity check *)
+                assert (not check_singleton_sets);
+                assert (
+                  (not check_not_already_registered)
+                  || not (Id1.Set.mem id1 ids));
+                (* Update *)
+                Some (Id1.Set.add id1 ids))
+          !map
+  end in
+  let module RAbsBorrow = R (V.AbstractionId) (V.BorrowId) in
+  let module RBorrowAbs = R (V.BorrowId) (V.AbstractionId) in
   let register_borrow_id abs_id bid =
-    abs_to_borrows :=
-      V.AbstractionId.Map.update abs_id
-        (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
-        !abs_to_borrows;
-    assert (not (V.BorrowId.Map.mem bid !borrow_to_abs));
-    borrow_to_abs := V.BorrowId.Map.add bid abs_id !borrow_to_abs
+    RAbsBorrow.register_mapping false no_duplicates abs_to_borrows abs_id bid;
+    RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid;
+    RBorrowAbs.register_mapping no_duplicates no_duplicates borrow_to_abs bid
+      abs_id;
+    RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id
   in
 
   let register_loan_id abs_id bid =
-    abs_to_loans :=
-      V.AbstractionId.Map.update abs_id
-        (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
-        !abs_to_loans;
-    assert (not (V.BorrowId.Map.mem bid !loan_to_abs));
-    loan_to_abs := V.BorrowId.Map.add bid abs_id !loan_to_abs
+    RAbsBorrow.register_mapping false no_duplicates abs_to_loans abs_id bid;
+    RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid;
+    RBorrowAbs.register_mapping no_duplicates no_duplicates loan_to_abs bid
+      abs_id;
+    RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id
   in
 
   let explore_abs =
@@ -159,8 +203,10 @@ let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
     abs_ids = List.rev !abs_ids;
     abs_to_borrows = !abs_to_borrows;
     abs_to_loans = !abs_to_loans;
+    abs_to_borrows_loans = !abs_to_borrows_loans;
     borrow_to_abs = !borrow_to_abs;
     loan_to_abs = !loan_to_abs;
+    borrow_loan_to_abs = !borrow_loan_to_abs;
   }
 
 (** Collapse an environment.
@@ -178,11 +224,19 @@ let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
       merge them.
     In effect, this allows us to merge newly introduced abstractions/borrows
     with their parent abstractions.
+
+    [merge_funs]: those are used to merge loans or borrows which appear in both
+    abstractions (rem.: here we mean that, for instance, both abstractions
+    contain a shared loan with id l0).
+    This can happen when merging environments (note that such environments are not well-formed -
+    they become well formed again after collapsing).
  *)
-let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
+let collapse_ctx (loop_id : V.LoopId.id)
+    (merge_funs : merge_duplicates_funcs option) (thresh : cnt_thresholds)
     (ctx0 : C.eval_ctx) : C.eval_ctx =
   let abs_kind = V.Loop loop_id in
-  let can_end = true in
+  let can_end = false in
+  let destructure_shared_values = true in
   let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
     V.AbstractionId.Ord.compare thresh.aid id >= 0
   in
@@ -201,7 +255,8 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
            | C.Var (DummyBinder id, v) ->
                if is_fresh_did id then
                  let absl =
-                   convert_value_to_abstractions abs_kind can_end ctx0 v
+                   convert_value_to_abstractions abs_kind can_end
+                     destructure_shared_values ctx0 v
                  in
                  List.map (fun abs -> C.Abs abs) absl
                else [ ee ])
@@ -210,18 +265,28 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
 
   (* Explore all the *new* abstractions, and compute various maps *)
   let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in
-  let ids_maps = compute_abs_borrows_loans_maps explore env in
+  let ids_maps =
+    compute_abs_borrows_loans_maps (merge_funs = None) explore env
+  in
   let {
     abs_ids;
     abs_to_borrows;
     abs_to_loans = _;
+    abs_to_borrows_loans;
     borrow_to_abs = _;
     loan_to_abs;
+    borrow_loan_to_abs;
   } =
     ids_maps
   in
 
-  (* Use the maps to merge the abstractions together *)
+  (* Change the merging behaviour depending on the input parameters *)
+  let abs_to_borrows, loan_to_abs =
+    if merge_funs <> None then (abs_to_borrows_loans, borrow_loan_to_abs)
+    else (abs_to_borrows, loan_to_abs)
+  in
+
+  (* Merge the abstractions together *)
   let merged_abs : V.AbstractionId.id UF.elem V.AbstractionId.Map.t =
     V.AbstractionId.Map.of_list (List.map (fun id -> (id, UF.make id)) abs_ids)
   in
@@ -243,35 +308,41 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
         (fun bid ->
           match V.BorrowId.Map.find_opt bid loan_to_abs with
           | None -> (* Nothing to do *) ()
-          | Some 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 =
-                UF.find (V.AbstractionId.Map.find abs_id0 merged_abs)
-              in
-              let abs_id0 = UF.get abs_ref0 in
-              let abs_ref1 =
-                UF.find (V.AbstractionId.Map.find abs_id1 merged_abs)
-              in
-              let abs_id1 = UF.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 *)
-                (* Lookup the abstractions *)
-                let abs0 = C.ctx_lookup_abs !ctx abs_id0 in
-                let abs1 = C.ctx_lookup_abs !ctx abs_id1 in
-                (* Merge them - note that we take care to merge [abs0] into [abs1]
-                   (the order is important).
-                *)
-                let nabs = merge_abstractions abs_kind can_end !ctx abs1 abs0 in
-                (* Update the environment *)
-                ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs);
-                ctx := fst (C.ctx_remove_abs !ctx abs_id0);
-                (* Update the union find *)
-                let abs_ref_merged = UF.union abs_ref0 abs_ref1 in
-                UF.set abs_ref_merged nabs.abs_id)
+          | Some abs_ids1 ->
+              V.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 =
+                    UF.find (V.AbstractionId.Map.find abs_id0 merged_abs)
+                  in
+                  let abs_id0 = UF.get abs_ref0 in
+                  let abs_ref1 =
+                    UF.find (V.AbstractionId.Map.find abs_id1 merged_abs)
+                  in
+                  let abs_id1 = UF.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 *)
+                    (* Lookup the abstractions *)
+                    let abs0 = C.ctx_lookup_abs !ctx abs_id0 in
+                    let abs1 = C.ctx_lookup_abs !ctx abs_id1 in
+                    (* Merge them - note that we take care to merge [abs0] into [abs1]
+                       (the order is important).
+                    *)
+                    let nabs =
+                      merge_abstractions abs_kind can_end merge_funs !ctx abs1
+                        abs0
+                    in
+                    (* Update the environment *)
+                    ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs);
+                    ctx := fst (C.ctx_remove_abs !ctx abs_id0);
+                    (* Update the union find *)
+                    let abs_ref_merged = UF.union abs_ref0 abs_ref1 in
+                    UF.set abs_ref_merged nabs.abs_id)
+                abs_ids1)
         bids)
     abs_ids;
 
@@ -313,6 +384,355 @@ let match_rtypes (rid_map : T.RegionId.InjSubst.t ref) (ctx : C.eval_ctx)
   in
   match_types check_regions ctx ty0 ty1
 
+(** See {!Match} *)
+module type Matcher = sig
+  (** The input primitive values are not equal *)
+  val match_distinct_primitive_values :
+    T.ety -> V.primitive_value -> V.primitive_value -> V.typed_value
+
+  (** The input ADTs don't have the same variant *)
+  val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value
+
+  (** The meta-value is the result of a match *)
+  val match_shared_borrows :
+    T.ety -> V.mvalue -> V.borrow_id -> V.borrow_id -> V.mvalue * V.borrow_id
+
+  (** The input parameters are:
+      - [ty]
+      - [bid0]: first borrow id
+      - [bv0]: first borrowed value
+      - [bid1]
+      - [bv1]
+      - [bv]: the result of matching [bv0] with [bv1]
+  *)
+  val match_mut_borrows :
+    T.ety ->
+    V.borrow_id ->
+    V.typed_value ->
+    V.borrow_id ->
+    V.typed_value ->
+    V.typed_value ->
+    V.borrow_id * V.typed_value
+
+  (** The shared value is the result of a match *)
+  val match_shared_loans :
+    T.ety ->
+    V.loan_id_set ->
+    V.loan_id_set ->
+    V.typed_value ->
+    V.loan_id_set * V.typed_value
+
+  val match_mut_loans : T.ety -> V.loan_id -> V.loan_id -> V.loan_id
+
+  (** There are no constraints on the input symbolic values *)
+  val match_symbolic_values :
+    V.symbolic_value -> V.symbolic_value -> V.symbolic_value
+end
+
+(** Generic functor to implement matching functions between values, environments,
+    etc.
+
+    We use it for joins, to check if two environments are convertible, etc.
+ *)
+module Match (M : Matcher) = struct
+  (** Match two values *)
+  let rec match_typed_values (ctx : C.eval_ctx) (v0 : V.typed_value)
+      (v1 : V.typed_value) : V.typed_value =
+    let match_rec = match_typed_values ctx in
+    assert (v0.V.ty = v1.V.ty);
+    match (v0.V.value, v1.V.value) with
+    | V.Primitive pv0, V.Primitive pv1 ->
+        if pv0 = pv1 then v1
+        else (
+          assert (v0.V.ty = v1.V.ty);
+          M.match_distinct_primitive_values v0.V.ty pv0 pv1)
+    | V.Adt av0, V.Adt av1 ->
+        if av0.variant_id = av1.variant_id then
+          let fields = List.combine av0.field_values av1.field_values in
+          let field_values =
+            List.map (fun (f0, f1) -> match_rec f0 f1) fields
+          in
+          let value : V.value =
+            V.Adt { variant_id = av0.variant_id; field_values }
+          in
+          { V.value; ty = v1.V.ty }
+        else (
+          (* For now, we don't merge ADTs which contain borrows *)
+          assert (not (value_has_borrows ctx v0.V.value));
+          assert (not (value_has_borrows ctx v1.V.value));
+          (* Merge *)
+          M.match_distinct_adts v0.V.ty av0 av1)
+    | Bottom, Bottom -> v1
+    | Borrow bc0, Borrow bc1 ->
+        let bc =
+          match (bc0, bc1) with
+          | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
+              (* Not completely sure what to do with the meta-value. If a shared
+                 symbolic value gets expanded in a branch, it may be simplified
+                 (by being folded back to a symbolic value) upon doing the join,
+                 which as a result would lead to code where it is considered as
+                 mutable (which is sound). On the other hand, if we access a
+                 symbolic value in a loop, the translated loop should take it as
+                 input anyway, so maybe this actually leads to equivalent
+                 code.
+              *)
+              let mv = match_rec mv0 mv1 in
+              assert (not (value_has_borrows ctx mv.V.value));
+              let mv, bid = M.match_shared_borrows v0.V.ty mv bid0 bid1 in
+              V.SharedBorrow (mv, bid)
+          | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
+              let bv = match_rec bv0 bv1 in
+              assert (not (value_has_borrows ctx bv.V.value));
+              let bid, bv = M.match_mut_borrows v0.V.ty bid0 bv0 bid1 bv1 bv in
+              V.MutBorrow (bid, bv)
+          | ReservedMutBorrow _, _
+          | _, ReservedMutBorrow _
+          | SharedBorrow _, MutBorrow _
+          | MutBorrow _, SharedBorrow _ ->
+              (* If we get here, either there is a typing inconsistency, or we are
+                 trying to match a reserved borrow, which shouldn't happen because
+                 reserved borrow should be eliminated very quickly - they are introduced
+                 just before function calls which activate them *)
+              raise (Failure "Unexpected")
+        in
+        { V.value = V.Borrow bc; V.ty = v1.V.ty }
+    | Loan lc0, Loan lc1 ->
+        (* TODO: maybe we should enforce that the ids are always exactly the same -
+           without matching *)
+        let lc =
+          match (lc0, lc1) with
+          | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) ->
+              let sv = match_rec sv0 sv1 in
+              assert (not (value_has_borrows ctx sv.V.value));
+              let ids, sv = M.match_shared_loans v0.V.ty ids0 ids1 sv in
+              V.SharedLoan (ids, sv)
+          | MutLoan id0, MutLoan id1 ->
+              let id = M.match_mut_loans v0.V.ty id0 id1 in
+              V.MutLoan id
+          | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ ->
+              raise (Failure "Unreachable")
+        in
+        { V.value = Loan lc; ty = v1.V.ty }
+    | Symbolic sv0, Symbolic sv1 ->
+        let sv = M.match_symbolic_values sv0 sv1 in
+        { v1 with V.value = V.Symbolic sv }
+    (* (* TODO: id check mapping *)
+       let id0 = lookup_sid sv0.sv_id in
+       let id1 = sv1.sv_id in
+       if id0 = id1 then (
+         assert (sv0.sv_kind = sv1.sv_kind);
+         (* Sanity check: the types should be the same *)
+         match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty;
+         (* Return *)
+         v1)
+       else (
+         (* For now, we force all the symbolic values containing borrows to
+            be eagerly expanded, and we don't support nested borrows *)
+         assert (not (value_has_borrows ctx v0.V.value));
+         assert (not (value_has_borrows ctx v1.V.value));
+         raise (Failure "Unimplemented")
+    *)
+    | Loan lc, _ -> (
+        match lc with
+        | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
+        | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
+    | _, Loan lc -> (
+        match lc with
+        | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
+        | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
+    | Symbolic _, _ -> raise (Failure "Unimplemented")
+    | _, Symbolic _ -> raise (Failure "Unimplemented")
+    | _ -> raise (Failure "Unreachable")
+end
+
+(* Very annoying: functors only take modules as inputs... *)
+module type MatchJoinState = sig
+  (** The current context *)
+  val ctx : C.eval_ctx
+
+  (** The current loop *)
+  val loop_id : V.LoopId.id
+
+  (** The abstractions introduced when performing the matches *)
+  val nabs : V.abs list ref
+end
+
+module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
+  (** Small utility *)
+  let push_abs (abs : V.abs) : unit = S.nabs := abs :: !S.nabs
+
+  let match_distinct_primitive_values (ty : T.ety) (_ : V.primitive_value)
+      (_ : V.primitive_value) : V.typed_value =
+    mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty
+
+  let match_distinct_adts (ty : T.ety) (adt0 : V.adt_value) (adt1 : V.adt_value)
+      : V.typed_value =
+    (* Check that the ADTs don't contain borrows - this is redundant with checks
+       performed by the caller, but we prefer to be safe with regards to future
+       updates
+    *)
+    let check_no_borrows (v : V.typed_value) =
+      assert (not (value_has_borrows S.ctx v.V.value))
+    in
+    List.iter check_no_borrows adt0.field_values;
+    List.iter check_no_borrows adt1.field_values;
+
+    (* Check if there are loans: we request to end them *)
+    let check_loans (left : bool) (fields : V.typed_value list) : unit =
+      match InterpreterBorrowsCore.get_first_loan_in_values fields with
+      | Some (V.SharedLoan (ids, _)) ->
+          if left then raise (ValueMatchFailure (LoansInLeft ids))
+          else raise (ValueMatchFailure (LoansInRight ids))
+      | Some (V.MutLoan id) ->
+          if left then raise (ValueMatchFailure (LoanInLeft id))
+          else raise (ValueMatchFailure (LoanInRight id))
+      | None -> ()
+    in
+    check_loans true adt0.field_values;
+    check_loans false adt1.field_values;
+
+    (* No borrows, no loans: we can introduce a symbolic value *)
+    mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty
+
+  let match_shared_borrows (ty : T.ety) (mv : V.mvalue) (bid0 : V.borrow_id)
+      (bid1 : V.borrow_id) : V.mvalue * V.borrow_id =
+    if bid0 = bid1 then (mv, bid0)
+    else
+      (* We replace bid0 and bid1 with a fresh borrow id, and introduce
+         an abstraction which links all of them:
+         {[
+           { SB bid0, SB bid1, SL {bid2} }
+         ]}
+      *)
+      let rid = C.fresh_region_id () in
+      let bid2 = C.fresh_borrow_id () in
+
+      (* Generate a fresh symbolic value for the shared value *)
+      let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty in
+
+      let _, bv_ty, kind = ty_as_ref ty in
+      let borrow_ty =
+        mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind
+      in
+
+      (* Generate the avalues for the abstraction *)
+      let mk_aborrow (bid : V.borrow_id) : V.typed_avalue =
+        let value = V.ABorrow (V.ASharedBorrow bid) in
+        { V.value; ty = borrow_ty }
+      in
+      let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in
+
+      let loan =
+        V.ASharedLoan
+          ( V.BorrowId.Set.singleton bid2,
+            sv,
+            mk_aignored (ety_no_regions_to_rty bv_ty) )
+      in
+      (* Note that an aloan has a borrow type *)
+      let loan = { V.value = V.ALoan loan; ty = borrow_ty } in
+
+      let avalues = List.append borrows [ loan ] in
+
+      (* Generate the abstraction *)
+      let abs =
+        {
+          V.abs_id = C.fresh_abstraction_id ();
+          kind = V.Loop S.loop_id;
+          can_end = false;
+          parents = V.AbstractionId.Set.empty;
+          original_parents = [];
+          regions = T.RegionId.Set.singleton rid;
+          ancestors_regions = T.RegionId.Set.empty;
+          avalues;
+        }
+      in
+      push_abs abs;
+
+      (* Return the new borrow *)
+      (sv, bid2)
+
+  let match_mut_borrows (ty : T.ety) (bid0 : V.borrow_id) (bv0 : V.typed_value)
+      (bid1 : V.borrow_id) (bv1 : V.typed_value) (bv : V.typed_value) :
+      V.borrow_id * V.typed_value =
+    if bid0 = bid1 then (bid0, bv)
+    else
+      (* We replace bid0 and bid1 with a fresh borrow id, and introduce
+         an abstraction which links all of them:
+         {[
+           { MB bid0, MB bid1, ML bid2 }
+         ]}
+      *)
+      let rid = C.fresh_region_id () in
+      let bid2 = C.fresh_borrow_id () in
+
+      (* Generate a fresh symbolic value for the borrowed value *)
+      let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty in
+
+      let _, bv_ty, kind = ty_as_ref ty in
+      let borrow_ty =
+        mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind
+      in
+
+      (* Generate the avalues for the abstraction *)
+      let mk_aborrow (bid : V.borrow_id) (bv : V.typed_value) : V.typed_avalue =
+        let bv_ty = ety_no_regions_to_rty bv.V.ty in
+        let value = V.ABorrow (V.AMutBorrow (bv, bid, mk_aignored bv_ty)) in
+        { V.value; ty = borrow_ty }
+      in
+      let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in
+
+      let loan = V.AMutLoan (bid2, mk_aignored (ety_no_regions_to_rty bv_ty)) in
+      (* Note that an aloan has a borrow type *)
+      let loan = { V.value = V.ALoan loan; ty = borrow_ty } in
+
+      let avalues = List.append borrows [ loan ] in
+
+      (* Generate the abstraction *)
+      let abs =
+        {
+          V.abs_id = C.fresh_abstraction_id ();
+          kind = V.Loop S.loop_id;
+          can_end = false;
+          parents = V.AbstractionId.Set.empty;
+          original_parents = [];
+          regions = T.RegionId.Set.singleton rid;
+          ancestors_regions = T.RegionId.Set.empty;
+          avalues;
+        }
+      in
+      push_abs abs;
+
+      (* Return the new borrow *)
+      (bid2, sv)
+
+  let match_shared_loans (ty : T.ety) (ids0 : V.loan_id_set)
+      (ids1 : V.loan_id_set) (sv : V.typed_value) :
+      V.loan_id_set * V.typed_value =
+    (* Check if the ids are the same - Rem.: we forbid the loans to a value
+       to vary. However, we allow to dive inside a data-structure: in this
+       case,
+    *)
+    let extra_ids_left = V.BorrowId.Set.diff ids0 ids1 in
+    let extra_ids_right = V.BorrowId.Set.diff ids1 ids0 in
+    if not (V.BorrowId.Set.is_empty extra_ids_left) then
+      raise (ValueMatchFailure (LoansInLeft extra_ids_left));
+    if not (V.BorrowId.Set.is_empty extra_ids_right) then
+      raise (ValueMatchFailure (LoansInRight extra_ids_right));
+
+    (* *)
+    raise (Failure "Unimplemented")
+
+  let match_mut_loans (ty : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) :
+      V.loan_id =
+    raise (Failure "Unimplemented")
+
+  (** There are no constraints on the input symbolic values *)
+  let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) :
+      V.symbolic_value =
+    raise (Failure "Unimplemented")
+end
+
+(*
 (** This function raises exceptions of kind {!ValueMatchFailue}.
 
     [convertible]: the function updates it to [false] if the result of the
@@ -439,15 +859,16 @@ let rec match_typed_values (config : C.config) (thresh : cnt_thresholds)
         raise (Failure "Unimplemented"))
   | Loan lc, _ -> (
       match lc with
-      | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids))
-      | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id)))
+      | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
+      | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
   | _, Loan lc -> (
       match lc with
-      | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids))
-      | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id)))
+      | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
+      | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
   | Symbolic _, _ -> raise (Failure "Unimplemented")
   | _, Symbolic _ -> raise (Failure "Unimplemented")
   | _ -> raise (Failure "Unreachable")
+ *)
 
 (*(** This function raises exceptions of kind {!ValueMatchFailue} *)
   let rec match_typed_avalues (config : C.config) (thresh : cnt_thresholds)
@@ -563,16 +984,19 @@ let rec match_typed_values (config : C.config) (thresh : cnt_thresholds)
           raise (Failure "Unimplemented"))
     | Loan lc, _ -> (
         match lc with
-        | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids))
-        | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id)))
+        | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
+        | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
     | _, Loan lc -> (
         match lc with
-        | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids))
-        | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id)))
+        | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
+        | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
   | _ -> raise (Failure "Unreachable")*)
 
-(** Apply substitutions in the first abstraction, then merge the abstractions together. *)
-let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
+(** Apply substitutions in the first abstraction, then join the abstractions together.
+
+    TODO: remove?
+ *)
+let subst_join_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
     (rid_map : T.RegionId.InjSubst.t) (bid_map : V.BorrowId.InjSubst.t)
     (sid_map : V.SymbolicValueId.InjSubst.t) (ctx : C.eval_ctx) (abs0 : V.abs)
     (abs1 : V.abs) : V.abs =
@@ -599,7 +1023,7 @@ let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
   (* Merge the two abstractions *)
   let abs_kind = V.Loop loop_id in
   let can_end = false in
-  merge_abstractions abs_kind can_end ctx abs0 abs1
+  merge_abstractions abs_kind can_end None ctx abs0 abs1
 
 (** Merge a borrow with the abstraction containing the associated loan, where
     the abstraction must be a *loop abstraction* (we don't synthesize code during
@@ -750,22 +1174,22 @@ let compute_loop_entry_fixed_point (config : C.config)
         (* Check if the join succeeded, or if we need to end abstractions/borrows
            in the original environment first *)
         match join_ctxs mctx with
-        | Error (EndAbsInSrc id) ->
+        | Error (AbsInLeft id) ->
             let ctx1 =
               InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx
             in
             eval_iteration_then_join { mctx with ctx = ctx1 }
-        | Error (EndBorrowInSrc id) ->
+        | Error (LoanInLeft id) ->
             let ctx1 =
               InterpreterBorrows.end_borrow_no_synth config id mctx.ctx
             in
             eval_iteration_then_join { mctx with ctx = ctx1 }
-        | Error (EndBorrowsInSrc ids) ->
+        | Error (LoansInLeft ids) ->
             let ctx1 =
               InterpreterBorrows.end_borrows_no_synth config ids mctx.ctx
             in
             eval_iteration_then_join { mctx with ctx = ctx1 }
-        | Error (EndBorrowInTgt _ | EndBorrowsInTgt _) ->
+        | Error (LoanInRight _ | LoansInRight _) ->
             (* Shouldn't happen here *)
             raise (Failure "Unreachable")
         | Ok mctx1 ->
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 62dce004..b287de27 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -54,6 +54,12 @@ let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.rty) :
   let value = V.Symbolic value in
   { V.value; V.ty }
 
+(** Create a fresh symbolic value *)
+let mk_fresh_symbolic_typed_value_from_ety (sv_kind : V.sv_kind) (ety : T.ety) :
+    V.typed_value =
+  let ty = TypesUtils.ety_no_regions_to_rty ety in
+  mk_fresh_symbolic_typed_value sv_kind ty
+
 (** Create a typed value from a symbolic value. *)
 let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
     V.typed_value =
@@ -115,7 +121,10 @@ let remove_borrow_from_asb (bid : V.BorrowId.id)
 
 (** We sometimes need to return a value whose type may vary depending on
     whether we find it in a "concrete" value or an abstraction (ex.: loan
-    contents when we perform environment lookups by using borrow ids) *)
+    contents when we perform environment lookups by using borrow ids)
+
+    TODO: change the name "abstract"
+ *)
 type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b
 
 (** Generic loan content: concrete or abstract *)
@@ -221,7 +230,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
 
       method! visit_symbolic_value _ s =
         match s.sv_kind with
-        | V.FunCallRet | V.LoopOutput ->
+        | V.FunCallRet | V.LoopOutput | V.LoopJoin ->
             if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
               raise Found
             else ()
diff --git a/compiler/Values.ml b/compiler/Values.ml
index f206f65a..efb0bb67 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -45,6 +45,8 @@ type sv_kind =
   | LoopOutput  (** The output of a loop (seen as a forward computation) *)
   | LoopGivenBack
       (** A value given back by a loop (when ending abstractions while going backwards) *)
+  | LoopJoin
+      (** The result of a loop join (when computing loop fixed points) *)
 [@@deriving show, ord]
 
 (** A symbolic value *)
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index df00bfb2..470f40ac 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -170,6 +170,24 @@ let value_has_borrows (infos : TA.type_infos) (v : value) : bool =
     false
   with Found -> true
 
+(** Check if a value has loans.
+
+    Note that loans are necessarily concrete (there can't be loans hidden
+    inside symbolic values).
+ *)
+let value_has_loans (v : value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+      method! visit_loan_content _env _ = raise Found
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_value () v;
+    false
+  with Found -> true
+
 (** Check if a value has loans or borrows in **a general sense**.
 
     It checks if: