Add markers everywhere, do not use them yet

10 files changed, 302 insertions, 139 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index ef958d2c..93238729 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -135,17 +135,19 @@ let end_borrow_get_borrow (span : Meta.span)
          * need it to properly instantiate the backward functions when generating
          * the pure translation. *)
         match lc with
-        | AMutLoan (_, _) ->
+        | AMutLoan (pm, _, _) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Nothing special to do *)
             super#visit_ALoan outer lc
-        | ASharedLoan (bids, v, av) ->
+        | ASharedLoan (pm, bids, v, av) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Explore the shared value - we need to update the outer borrows *)
             let souter = update_outer_borrows outer (Borrows bids) in
             let v = super#visit_typed_value souter v in
             (* Explore the child avalue - we keep the same outer borrows *)
             let av = super#visit_typed_avalue outer av in
             (* Reconstruct *)
-            ALoan (ASharedLoan (bids, v, av))
+            ALoan (ASharedLoan (pm, bids, v, av))
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan _
         (* The loan has ended, so no need to update the outer borrows *)
@@ -159,7 +161,8 @@ let end_borrow_get_borrow (span : Meta.span)
 
       method! visit_ABorrow outer bc =
         match bc with
-        | AMutBorrow (bid, _) ->
+        | AMutBorrow (pm, bid, _) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Check if this is the borrow we are looking for *)
             if bid = l then (
               (* TODO: treat this case differently. We should not introduce
@@ -188,7 +191,8 @@ let end_borrow_get_borrow (span : Meta.span)
               (* Update the outer borrows before diving into the child avalue *)
               let outer = update_outer_borrows outer (Borrow bid) in
               super#visit_ABorrow outer bc
-        | ASharedBorrow bid ->
+        | ASharedBorrow (pm, bid) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Check if this is the borrow we are looking for *)
             if bid = l then (
               (* Check there are outer borrows, or if we need to end the whole
@@ -338,7 +342,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
               match nv.value with
               | VSymbolic sv ->
                   let abs = Option.get opt_abs in
-                  (* Remember the given back value as a span-value
+                  (* Remember the given back value as a meta-value
                    * TODO: it is a bit annoying to have to deconstruct
                    * the value... Think about a more elegant way. *)
                   let given_back_span = as_symbolic span nv.value in
@@ -377,14 +381,15 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
           ty
         in
         match lc with
-        | AMutLoan (bid', child) ->
+        | AMutLoan (pm, bid', child) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid' = bid then (
               (* This is the loan we are looking for: apply the projection to
                * the value we give back and replaced this mutable loan with
                * an ended loan *)
               (* Register the insertion *)
               set_replaced ();
-              (* Remember the given back value as a span-value *)
+              (* Remember the given back value as a meta-value *)
               let given_back_span = nv in
               (* Apply the projection *)
               let given_back =
@@ -397,7 +402,8 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
               ALoan (AEndedMutLoan { child; given_back; given_back_span }))
             else (* Continue exploring *)
               super#visit_ALoan opt_abs lc
-        | ASharedLoan (_, _, _) ->
+        | ASharedLoan (pm, _, _, _) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* We are giving back a value to a *mutable* loan: nothing special to do *)
             super#visit_ALoan opt_abs lc
         | AEndedMutLoan { child = _; given_back = _; given_back_span = _ }
@@ -408,7 +414,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
             (* This loan is ignored, but we may have to project on a subvalue
              * of the value which is given back *)
             if opt_bid = Some bid then
-              (* Remember the given back value as a span-value *)
+              (* Remember the given back value as a meta-value *)
               let given_back_span = nv in
               (* Note that we replace the ignored mut loan by an *ended* ignored
                * mut loan. Also, this is not the loan we are looking for *per se*:
@@ -453,7 +459,7 @@ let give_back_symbolic_value (_config : config) (span : Meta.span)
   sanity_check __FILE__ __LINE__
     (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty)
     span;
-  (* Store the given-back value as a span-value for synthesis purposes *)
+  (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
   let subst (_abs : abs) local_given_back =
@@ -531,7 +537,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span)
       method visit_typed_ALoan (opt_abs : abs option) (ty : rty)
           (lc : aloan_content) : avalue =
         match lc with
-        | AMutLoan (bid', child) ->
+        | AMutLoan (pm, bid', child) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid' = bid then (
               (* Sanity check - about why we need to call {!ty_get_ref}
                * (and don't do the same thing as in {!give_back_value})
@@ -553,12 +560,13 @@ let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span)
                 (AEndedMutLoan { given_back = nv; child; given_back_span = nsv }))
             else (* Continue exploring *)
               super#visit_ALoan opt_abs lc
-        | ASharedLoan (_, _, _)
+        | ASharedLoan (PNone, _, _, _)
         (* We are giving back a value to a *mutable* loan: nothing special to do *)
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _) ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
+        | ASharedLoan (_, _, _, _) -> internal_error __FILE__ __LINE__ span
         | AIgnoredMutLoan (bid_opt, child) ->
             (* This loan is ignored, but we may have to project on a subvalue
              * of the value which is given back *)
@@ -631,10 +639,12 @@ let give_back_shared _config (span : Meta.span) (bid : BorrowId.id)
 
       method! visit_ALoan opt_abs lc =
         match lc with
-        | AMutLoan (bid, av) ->
+        | AMutLoan (pm, bid, av) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Nothing special to do (we are giving back a *shared* borrow) *)
-            ALoan (super#visit_AMutLoan opt_abs bid av)
-        | ASharedLoan (bids, shared_value, child) ->
+            ALoan (super#visit_AMutLoan opt_abs pm bid av)
+        | ASharedLoan (pm, bids, shared_value, child) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if BorrowId.Set.mem bid bids then (
               (* This is the loan we are looking for *)
               set_replaced ();
@@ -646,7 +656,7 @@ let give_back_shared _config (span : Meta.span) (bid : BorrowId.id)
               else
                 ALoan
                   (ASharedLoan
-                     (BorrowId.Set.remove bid bids, shared_value, child)))
+                     (pm, BorrowId.Set.remove bid bids, shared_value, child)))
             else
               (* Not the loan we are looking for: continue exploring *)
               super#visit_ALoan opt_abs lc
@@ -700,13 +710,14 @@ let reborrow_shared (span : Meta.span) (original_bid : BorrowId.id)
           VSharedLoan (bids', sv))
         else super#visit_VSharedLoan env bids sv
 
-      method! visit_ASharedLoan env bids v av =
+      method! visit_ASharedLoan env pm bids v av =
+        sanity_check __FILE__ __LINE__ (pm = PNone) span;
         (* This case is similar to the {!SharedLoan} case *)
         if BorrowId.Set.mem original_bid bids then (
           set_ref ();
           let bids' = BorrowId.Set.add new_bid bids in
-          ASharedLoan (bids', v, av))
-        else super#visit_ASharedLoan env bids v av
+          ASharedLoan (pm, bids', v, av))
+        else super#visit_ASharedLoan env pm bids v av
     end
   in
 
@@ -789,8 +800,9 @@ let give_back (config : config) (span : Meta.span) (l : BorrowId.id)
         span;
       (* Update the context *)
       give_back_shared config span l ctx
-  | Abstract (AMutBorrow (l', av)) ->
+  | Abstract (AMutBorrow (pm, l', av)) ->
       (* Sanity check *)
+      sanity_check __FILE__ __LINE__ (pm = PNone) span;
       sanity_check __FILE__ __LINE__ (l' = l) span;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
       sanity_check __FILE__ __LINE__
@@ -806,8 +818,9 @@ let give_back (config : config) (span : Meta.span) (l : BorrowId.id)
       give_back_avalue_to_same_abstraction config span l av
         (mk_typed_value_from_symbolic_value sv)
         ctx
-  | Abstract (ASharedBorrow l') ->
+  | Abstract (ASharedBorrow (pm, l')) ->
       (* Sanity check *)
+      sanity_check __FILE__ __LINE__ (pm = PNone) span;
       sanity_check __FILE__ __LINE__ (l' = l) span;
       (* Check that the borrow is somewhere - purely a sanity check *)
       sanity_check __FILE__ __LINE__
@@ -827,7 +840,7 @@ let give_back (config : config) (span : Meta.span) (l : BorrowId.id)
 
 let check_borrow_disappeared (span : Meta.span) (fun_name : string)
     (l : BorrowId.id) (ctx0 : eval_ctx) (ctx : eval_ctx) : unit =
-  (match lookup_borrow_opt ek_all l ctx with
+  (match lookup_borrow_opt span ek_all l ctx with
   | None -> () (* Ok *)
   | Some _ ->
       log#ltrace
@@ -1205,7 +1218,8 @@ and end_abstraction_borrows (config : config) (span : Meta.span)
           ^ aborrow_content_to_string ~span:(Some span) ctx bc));
       let ctx =
         match bc with
-        | AMutBorrow (bid, av) ->
+        | AMutBorrow (pm, bid, av) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* First, convert the avalue to a (fresh symbolic) value *)
             let sv = convert_avalue_to_given_back_value span av in
             (* Replace the mut borrow to register the fact that we ended
@@ -1215,7 +1229,8 @@ and end_abstraction_borrows (config : config) (span : Meta.span)
             (* Give the value back *)
             let sv = mk_typed_value_from_symbolic_value sv in
             give_back_value config span bid sv ctx
-        | ASharedBorrow bid ->
+        | ASharedBorrow (pm, bid) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Replace the shared borrow to account for the fact it ended *)
             let ended_borrow = ABorrow AEndedSharedBorrow in
             let ctx = update_aborrow span ek_all bid ended_borrow ctx in
@@ -1637,7 +1652,8 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
     | ALoan lc -> (
         (* Explore the loan content *)
         match lc with
-        | ASharedLoan (bids, sv, child_av) ->
+        | ASharedLoan (pm, bids, sv, child_av) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (value_has_borrows ctx sv.value))
@@ -1648,7 +1664,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
             in
             (* Push a value *)
             let ignored = mk_aignored span child_av.ty in
-            let value = ALoan (ASharedLoan (bids, sv, ignored)) in
+            let value = ALoan (ASharedLoan (pm, bids, sv, ignored)) in
             push { value; ty };
             (* Explore the child *)
             list_avalues false push_fail child_av;
@@ -1659,12 +1675,13 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
                exactly the same way as [list_avalues] (i.e., with a similar
                signature) *)
             List.iter push avl
-        | AMutLoan (bid, child_av) ->
+        | AMutLoan (pm, bid, child_av) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Explore the child *)
             list_avalues false push_fail child_av;
             (* Explore the whole loan *)
             let ignored = mk_aignored span child_av.ty in
-            let value = ALoan (AMutLoan (bid, ignored)) in
+            let value = ALoan (AMutLoan (pm, bid, ignored)) in
             push { value; ty }
         | AIgnoredMutLoan (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
@@ -1691,14 +1708,16 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
         sanity_check __FILE__ __LINE__ allow_borrows span;
         (* Explore the borrow content *)
         match bc with
-        | AMutBorrow (bid, child_av) ->
+        | AMutBorrow (pm, bid, child_av) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Explore the child *)
             list_avalues false push_fail child_av;
             (* Explore the borrow *)
             let ignored = mk_aignored span child_av.ty in
-            let value = ABorrow (AMutBorrow (bid, ignored)) in
+            let value = ABorrow (AMutBorrow (pm, bid, ignored)) in
             push { value; ty }
-        | ASharedBorrow _ ->
+        | ASharedBorrow (pm, _) ->
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Nothing specific to do: keep the value as it is *)
             push av
         | AIgnoredMutBorrow (opt_bid, child_av) ->
@@ -1777,7 +1796,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
                 let sv = mk_value_with_fresh_sids sv in
                 (* Create the new avalue *)
                 let value =
-                  ALoan (ASharedLoan (bids, sv, mk_aignored span ty))
+                  ALoan (ASharedLoan (PNone, bids, sv, mk_aignored span ty))
                 in
                 { value; ty }
               in
@@ -1900,7 +1919,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span
               "Nested borrows are not supported yet";
             let ty = TRef (RFVar r_id, ref_ty, kind) in
-            let value = ABorrow (ASharedBorrow bid) in
+            let value = ABorrow (ASharedBorrow (PNone, bid)) in
             ([ { value; ty } ], v)
         | VMutBorrow (bid, bv) ->
             let r_id = if group then r_id else fresh_region_id () in
@@ -1911,7 +1930,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let ignored = mk_aignored span ref_ty in
-            let av = ABorrow (AMutBorrow (bid, ignored)) in
+            let av = ABorrow (AMutBorrow (PNone, bid, ignored)) in
             let av = { value = av; ty } in
             (* Continue exploring, looking for loans (and forbidding borrows,
                because we don't support nested borrows for now) *)
@@ -1937,7 +1956,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             let ignored = mk_aignored span ty in
             (* Rem.: the shared value might contain loans *)
             let avl, sv = to_avalues false true true r_id sv in
-            let av = ALoan (ASharedLoan (bids, sv, ignored)) in
+            let av = ALoan (ASharedLoan (PNone, bids, sv, ignored)) in
             let av = { value = av; ty } in
             (* Continue exploring, looking for loans (and forbidding borrows,
                because we don't support nested borrows for now) *)
@@ -1954,7 +1973,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
               "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RMut in
             let ignored = mk_aignored span ty in
-            let av = ALoan (AMutLoan (bid, ignored)) in
+            let av = ALoan (AMutLoan (PNone, bid, ignored)) in
             let av = { value = av; ty } in
             ([ av ], v))
     | VSymbolic _ ->
@@ -2085,8 +2104,14 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
         in
         (* Register the loans *)
         (match lc with
-        | ASharedLoan (bids, _, _) -> push_loans bids (Abstract (ty, lc))
-        | AMutLoan (bid, _) -> push_loan bid (Abstract (ty, lc))
+        | 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))
         | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ ->
             (* The abstraction has been destructured, so those shouldn't appear *)
@@ -2102,8 +2127,14 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
         in
         (* Explore the borrow content *)
         (match bc with
-        | AMutBorrow (bid, _) -> push_borrow bid (Abstract (ty, bc))
-        | ASharedBorrow bid -> push_borrow bid (Abstract (ty, bc))
+        | 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))
         | AProjSharedBorrow asb ->
             let register asb =
               match asb with
@@ -2140,29 +2171,50 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
 
 type merge_duplicates_funcs = {
   merge_amut_borrows :
-    borrow_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue;
+    borrow_id ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
+          - [pm0]
           - [child0]
           - [ty1]
+          - [pm1]
           - [child1]
 
           The children should be [AIgnored].
        *)
-  merge_ashared_borrows : borrow_id -> rty -> rty -> typed_avalue;
+  merge_ashared_borrows :
+    borrow_id -> rty -> proj_marker -> rty -> proj_marker -> typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
+          - [pm0]
           - [ty1]
+          - [pm1]
        *)
   merge_amut_loans :
-    loan_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue;
+    loan_id ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
+          - [pm0]
           - [child0]
           - [ty1]
+          - [pm1]
           - [child1]
 
           The children should be [AIgnored].
@@ -2170,18 +2222,22 @@ type merge_duplicates_funcs = {
   merge_ashared_loans :
     loan_id_set ->
     rty ->
+    proj_marker ->
     typed_value ->
     typed_avalue ->
     rty ->
+    proj_marker ->
     typed_value ->
     typed_avalue ->
     typed_avalue;
       (** Parameters:
           - [ids]
           - [ty0]
+          - [pm0]
           - [sv0]
           - [child0]
           - [ty1]
+          - [pm1]
           - [sv1]
           - [child1]
        *)
@@ -2301,10 +2357,19 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
   let merge_aborrow_contents (ty0 : rty) (bc0 : aborrow_content) (ty1 : rty)
       (bc1 : aborrow_content) : typed_avalue =
     match (bc0, bc1) with
-    | AMutBorrow (id, child0), AMutBorrow (_, child1) ->
-        (Option.get merge_funs).merge_amut_borrows id ty0 child0 ty1 child1
-    | ASharedBorrow id, ASharedBorrow _ ->
-        (Option.get merge_funs).merge_ashared_borrows id ty0 ty1
+    | 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"
@@ -2330,12 +2395,21 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
   let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty)
       (lc1 : aloan_content) : typed_avalue option =
     match (lc0, lc1) with
-    | AMutLoan (id, child0), AMutLoan (_, child1) ->
+    | 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 id;
+        set_loan_as_merged id0;
         (* Merge *)
-        Some ((Option.get merge_funs).merge_amut_loans id ty0 child0 ty1 child1)
-    | ASharedLoan (ids0, sv0, child0), ASharedLoan (ids1, sv1, child1) ->
+        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
@@ -2368,8 +2442,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
           set_loans_as_merged ids;
           (* Merge *)
           Some
-            ((Option.get merge_funs).merge_ashared_loans ids ty0 sv0 child0 ty1
-               sv1 child1))
+            ((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 *)
@@ -2471,7 +2545,9 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
                           craise __FILE__ __LINE__ span "Unreachable"
                       | Abstract (ty, lc) -> (
                           match lc with
-                          | ASharedLoan (bids, sv, child) ->
+                          | 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
                               sanity_check __FILE__ __LINE__
                                 (not (BorrowId.Set.is_empty bids))
@@ -2481,7 +2557,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
                               sanity_check __FILE__ __LINE__
                                 (not (value_has_loans_or_borrows ctx sv.value))
                                 span;
-                              let lc = ASharedLoan (bids, sv, child) in
+                              let lc = ASharedLoan (pm, bids, sv, child) in
                               set_loans_as_merged bids;
                               Some { value = ALoan lc; ty }
                           | AMutLoan _ ->
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 56df9344..c119311f 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -138,29 +138,50 @@ val convert_value_to_abstractions :
   *)
 type merge_duplicates_funcs = {
   merge_amut_borrows :
-    borrow_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue;
+    borrow_id ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
+          - [pm0]
           - [child0]
           - [ty1]
+          - [pm1]
           - [child1]
 
           The children should be [AIgnored].
        *)
-  merge_ashared_borrows : borrow_id -> rty -> rty -> typed_avalue;
+  merge_ashared_borrows :
+    borrow_id -> rty -> proj_marker -> rty -> proj_marker -> typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
+          - [pm0]
           - [ty1]
+          - [pm1]
        *)
   merge_amut_loans :
-    loan_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue;
+    loan_id ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    rty ->
+    proj_marker ->
+    typed_avalue ->
+    typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
+          - [pm0]
           - [child0]
           - [ty1]
+          - [pm1]
           - [child1]
 
           The children should be [AIgnored].
@@ -168,18 +189,22 @@ type merge_duplicates_funcs = {
   merge_ashared_loans :
     loan_id_set ->
     rty ->
+    proj_marker ->
     typed_value ->
     typed_avalue ->
     rty ->
+    proj_marker ->
     typed_value ->
     typed_avalue ->
     typed_avalue;
       (** Parameters:
           - [ids]
           - [ty0]
+          - [pm0]
           - [sv0]
           - [child0]
           - [ty1]
+          - [pm1]
           - [sv1]
           - [child1]
        *)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 776cb6fa..7714f5bb 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -144,7 +144,7 @@ let eval_loop_symbolic (config : config) (span : span)
         ^ eval_ctx_to_string ~span:(Some span) ctx));
 
     (* Compute the end expression, that is the expresion corresponding to the
-       end of the functin where we call the loop (for now, when calling a loop
+       end of the function where we call the loop (for now, when calling a loop
        we never get out) *)
     let res_fun_end =
       comp cf_prepare
@@ -255,10 +255,13 @@ let eval_loop_symbolic (config : config) (span : span)
         List.filter_map
           (fun (av : typed_avalue) ->
             match av.value with
-            | ABorrow (AMutBorrow (bid, child_av)) ->
+            | ABorrow (AMutBorrow (pm, bid, child_av)) ->
+                sanity_check __FILE__ __LINE__ (pm = PNone) span;
                 sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span;
                 Some (bid, child_av.ty)
-            | ABorrow (ASharedBorrow _) -> None
+            | ABorrow (ASharedBorrow (pm, _)) ->
+                sanity_check __FILE__ __LINE__ (pm = PNone) span;
+                None
             | _ -> craise __FILE__ __LINE__ span "Unreachable")
           borrows
       in
@@ -268,10 +271,13 @@ let eval_loop_symbolic (config : config) (span : span)
         List.filter_map
           (fun (av : typed_avalue) ->
             match av.value with
-            | ALoan (AMutLoan (bid, child_av)) ->
+            | ALoan (AMutLoan (pm, bid, child_av)) ->
+                sanity_check __FILE__ __LINE__ (pm = PNone) span;
                 sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span;
                 Some bid
-            | ALoan (ASharedLoan _) -> None
+            | ALoan (ASharedLoan (pm, _, _, _)) ->
+                sanity_check __FILE__ __LINE__ (pm = PNone) span;
+                None
             | _ -> craise __FILE__ __LINE__ span "Unreachable")
           loans
       in
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 991f259f..675dc544 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -65,7 +65,7 @@ module type PrimMatcher = sig
   val match_distinct_adts :
     eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value
 
-  (** The span-value is the result of a match.
+  (** The meta-value is the result of a match.
 
       We take an additional function as input, which acts as a matcher over
       typed values, to be able to lookup the shared values and match them.
@@ -158,8 +158,10 @@ module type PrimMatcher = sig
 
   (** Parameters:
       [ty0]
+      [pm0]
       [bid0]
       [ty1]
+      [pm1]
       [bid1]
       [ty]: result of matching ty0 and ty1
    *)
@@ -167,17 +169,21 @@ module type PrimMatcher = sig
     eval_ctx ->
     eval_ctx ->
     rty ->
+    proj_marker ->
     borrow_id ->
     rty ->
+    proj_marker ->
     borrow_id ->
     rty ->
     typed_avalue
 
   (** Parameters:
       [ty0]
+      [pm0]
       [bid0]
       [av0]
       [ty1]
+      [pm1]
       [bid1]
       [av1]
       [ty]: result of matching ty0 and ty1
@@ -187,9 +193,11 @@ module type PrimMatcher = sig
     eval_ctx ->
     eval_ctx ->
     rty ->
+    proj_marker ->
     borrow_id ->
     typed_avalue ->
     rty ->
+    proj_marker ->
     borrow_id ->
     typed_avalue ->
     rty ->
@@ -198,10 +206,12 @@ module type PrimMatcher = sig
 
   (** Parameters:
       [ty0]
+      [pm0]
       [ids0]
       [v0]
       [av0]
       [ty1]
+      [pm1]
       [ids1]
       [v1]
       [av1]
@@ -213,10 +223,12 @@ module type PrimMatcher = sig
     eval_ctx ->
     eval_ctx ->
     rty ->
+    proj_marker ->
     loan_id_set ->
     typed_value ->
     typed_avalue ->
     rty ->
+    proj_marker ->
     loan_id_set ->
     typed_value ->
     typed_avalue ->
@@ -227,9 +239,11 @@ module type PrimMatcher = sig
 
   (** Parameters:
       [ty0]
+      [pm0]
       [id0]
       [av0]
       [ty1]
+      [pm1]
       [id1]
       [av1]
       [ty]: result of matching ty0 and ty1
@@ -239,9 +253,11 @@ module type PrimMatcher = sig
     eval_ctx ->
     eval_ctx ->
     rty ->
+    proj_marker ->
     borrow_id ->
     typed_avalue ->
     rty ->
+    proj_marker ->
     borrow_id ->
     typed_avalue ->
     rty ->
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 1a0bb090..599fabfd 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -153,13 +153,19 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span)
     *)
     let get_borrow_id (av : typed_avalue) : BorrowId.id =
       match av.value with
-      | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid
+      | ABorrow (AMutBorrow (pm, bid, _) | ASharedBorrow (pm, bid)) ->
+          sanity_check __FILE__ __LINE__ (pm = PNone) span;
+          bid
       | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     let get_loan_id (av : typed_avalue) : BorrowId.id =
       match av.value with
-      | ALoan (AMutLoan (lid, _)) -> lid
-      | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids
+      | ALoan (AMutLoan (pm, lid, _)) ->
+          sanity_check __FILE__ __LINE__ (pm = PNone) span;
+          lid
+      | ALoan (ASharedLoan (pm, lids, _, _)) ->
+          sanity_check __FILE__ __LINE__ (pm = PNone) span;
+          BorrowId.Set.min_elt lids
       | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     (* We use ordered maps to reorder the borrows and loans *)
@@ -245,7 +251,8 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
        SL {l0, l1} s0
      ]}
 
-     and introduce the corresponding abstraction:
+     and introduce the corresponding abstraction for the borrow l0
+     (and we do something similar for l1):
      {[
        abs'2 { SB l0, SL {l2} s2 }
      ]}
@@ -283,13 +290,13 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     (* Create the shared loan *)
     let loan_rty = TRef (RFVar nrid, rty, RShared) in
     let loan_value =
-      ALoan (ASharedLoan (BorrowId.Set.singleton nlid, nsv, child_av))
+      ALoan (ASharedLoan (PNone, BorrowId.Set.singleton nlid, nsv, child_av))
     in
     let loan_value = mk_typed_avalue span loan_rty loan_value in
 
     (* Create the shared borrow *)
     let borrow_rty = loan_rty in
-    let borrow_value = ABorrow (ASharedBorrow lid) in
+    let borrow_value = ABorrow (ASharedBorrow (PNone, lid)) in
     let borrow_value = mk_typed_avalue span borrow_rty borrow_value in
 
     (* Create the abstraction *)
@@ -344,11 +351,11 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
           (* Continue the exploration *)
           super#visit_VSharedLoan env lids sv
 
-        method! visit_ASharedLoan env lids sv av =
+        method! visit_ASharedLoan env pm lids sv av =
           collect_shared_value lids sv;
 
           (* Continue the exploration *)
-          super#visit_ASharedLoan env lids sv av
+          super#visit_ASharedLoan env pm lids sv av
 
         (** Check that there are no symbolic values with *borrows* inside the
             abstraction - shouldn't happen if the symbolic values are greedily
@@ -905,7 +912,9 @@ let compute_fixed_point_id_correspondance (span : Meta.span)
     let lookup_shared_loan lid ctx : typed_value =
       match snd (lookup_loan span ek_all lid ctx) with
       | Concrete (VSharedLoan (_, v)) -> v
-      | Abstract (ASharedLoan (_, v, _)) -> v
+      | Abstract (ASharedLoan (pm, _, v, _)) ->
+          sanity_check __FILE__ __LINE__ (pm = PNone) span;
+          v
       | _ -> craise __FILE__ __LINE__ span "Unreachable"
     in
     let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
@@ -1044,7 +1053,7 @@ let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx)
       object (self)
         inherit [_] iter_env
 
-        method! visit_ASharedLoan inside_shared _ sv child_av =
+        method! visit_ASharedLoan inside_shared _ _ sv child_av =
           self#visit_typed_value true sv;
           self#visit_typed_avalue inside_shared child_av
 
@@ -1094,7 +1103,9 @@ let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx)
           let v =
             match snd (lookup_loan span ek_all bid fp_ctx) with
             | Concrete (VSharedLoan (_, v)) -> v
-            | Abstract (ASharedLoan (_, v, _)) -> v
+            | Abstract (ASharedLoan (pm, _, v, _)) ->
+                sanity_check __FILE__ __LINE__ (pm = PNone) span;
+                v
             | _ -> craise __FILE__ __LINE__ span "Unreachable"
           in
           self#visit_typed_value env v
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index c67869ac..7ea442db 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -39,13 +39,13 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span)
     *)
     let get_borrow_id (av : typed_avalue) : BorrowId.id =
       match av.value with
-      | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid
+      | ABorrow (AMutBorrow (_, bid, _) | ASharedBorrow (_, bid)) -> bid
       | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     let get_loan_id (av : typed_avalue) : BorrowId.id =
       match av.value with
-      | ALoan (AMutLoan (lid, _)) -> lid
-      | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids
+      | ALoan (AMutLoan (_, lid, _)) -> lid
+      | ALoan (ASharedLoan (_, lids, _, _)) -> BorrowId.Set.min_elt lids
       | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     (* We use ordered maps to reorder the borrows and loans *)
@@ -314,11 +314,14 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
      Note that the join matcher doesn't implement match functions for avalues
      (see the comments in {!MakeJoinMatcher}.
   *)
-  let merge_amut_borrows id ty0 child0 _ty1 child1 =
+  let merge_amut_borrows id ty0 pm0 child0 _ty1 pm1 child1 =
     (* 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;
+
     (* 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
@@ -326,11 +329,11 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
     *)
     let ty = ty0 in
     let child = child0 in
-    let value = ABorrow (AMutBorrow (id, child)) in
+    let value = ABorrow (AMutBorrow (PNone, id, child)) in
     { value; ty }
   in
 
-  let merge_ashared_borrows id ty0 ty1 =
+  let merge_ashared_borrows id ty0 pm0 ty1 pm1 =
     (* Sanity checks *)
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
@@ -343,23 +346,28 @@ 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 id) in
+    let value = ABorrow (ASharedBorrow (PNone, id)) in
     { value; ty }
   in
 
-  let merge_amut_loans id ty0 child0 _ty1 child1 =
+  let merge_amut_loans id ty0 pm0 child0 _ty1 pm1 child1 =
     (* 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
-    let value = ALoan (AMutLoan (id, child)) in
+    let value = ALoan (AMutLoan (PNone, id, child)) in
     { value; ty }
   in
-  let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1
+  let merge_ashared_loans ids ty0 pm0 (sv0 : typed_value) child0 _ty1 pm1
       (sv1 : typed_value) child1 =
     (* Sanity checks *)
     sanity_check __FILE__ __LINE__ (is_aignored child0.value) span;
@@ -375,10 +383,13 @@ 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
     let sv = M.match_typed_values ctx ctx sv0 sv1 in
-    let value = ALoan (ASharedLoan (ids, sv, child)) in
+    let value = ALoan (ASharedLoan (PNone, ids, sv, child)) in
     { value; ty }
   in
   {
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index e25adb2c..729b248f 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -353,10 +353,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
     | ABorrow bc0, ABorrow bc1 -> (
         log#ldebug (lazy "match_typed_avalues: borrows");
         match (bc0, bc1) with
-        | ASharedBorrow bid0, ASharedBorrow bid1 ->
+        | ASharedBorrow (pm0, bid0), ASharedBorrow (pm1, bid1) ->
             log#ldebug (lazy "match_typed_avalues: shared borrows");
-            M.match_ashared_borrows ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty
-        | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) ->
+            M.match_ashared_borrows ctx0 ctx1 v0.ty pm0 bid0 v1.ty pm1 bid1 ty
+        | AMutBorrow (pm0, bid0, av0), AMutBorrow (pm1, bid1, av1) ->
             log#ldebug (lazy "match_typed_avalues: mut borrows");
             log#ldebug
               (lazy
@@ -364,7 +364,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
             let av = match_arec av0 av1 in
             log#ldebug
               (lazy "match_typed_avalues: mut borrows: matched children values");
-            M.match_amut_borrows ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av
+            M.match_amut_borrows ctx0 ctx1 v0.ty pm0 bid0 av0 v1.ty pm1 bid1 av1
+              ty av
         | AIgnoredMutBorrow _, AIgnoredMutBorrow _ ->
             (* The abstractions are destructured: we shouldn't get there *)
             craise __FILE__ __LINE__ M.span "Unexpected"
@@ -393,23 +394,25 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
         (* TODO: maybe we should enforce that the ids are always exactly the same -
            without matching *)
         match (lc0, lc1) with
-        | ASharedLoan (ids0, sv0, av0), ASharedLoan (ids1, sv1, av1) ->
+        | ASharedLoan (pm0, ids0, sv0, av0), ASharedLoan (pm1, ids1, sv1, av1)
+          ->
             log#ldebug (lazy "match_typed_avalues: shared loans");
             let sv = match_rec sv0 sv1 in
             let av = match_arec av0 av1 in
             sanity_check __FILE__ __LINE__
               (not (value_has_borrows sv.value))
               M.span;
-            M.match_ashared_loans ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1
-              av1 ty sv av
-        | AMutLoan (id0, av0), AMutLoan (id1, av1) ->
+            M.match_ashared_loans ctx0 ctx1 v0.ty pm0 ids0 sv0 av0 v1.ty pm1
+              ids1 sv1 av1 ty sv av
+        | AMutLoan (pm0, id0, av0), AMutLoan (pm1, id1, av1) ->
             log#ldebug (lazy "match_typed_avalues: mut loans");
             log#ldebug
               (lazy "match_typed_avalues: mut loans: matching children values");
             let av = match_arec av0 av1 in
             log#ldebug
               (lazy "match_typed_avalues: mut loans: matched children values");
-            M.match_amut_loans ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av
+            M.match_amut_loans ctx0 ctx1 v0.ty pm0 id0 av0 v1.ty pm1 id1 av1 ty
+              av
         | AIgnoredMutLoan _, AIgnoredMutLoan _
         | AIgnoredSharedLoan _, AIgnoredSharedLoan _ ->
             (* Those should have been filtered when destructuring the abstractions -
@@ -504,13 +507,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
       (* Generate the avalues for the abstraction *)
       let mk_aborrow (bid : borrow_id) : typed_avalue =
-        let value = ABorrow (ASharedBorrow bid) in
+        let value = ABorrow (ASharedBorrow (PNone, bid)) in
         { value; ty = borrow_ty }
       in
       let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in
 
       let loan =
-        ASharedLoan (BorrowId.Set.singleton bid2, sv, mk_aignored span bv_ty)
+        ASharedLoan
+          (PNone, BorrowId.Set.singleton bid2, sv, mk_aignored span bv_ty)
       in
       (* Note that an aloan has a borrow type *)
       let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in
@@ -604,13 +608,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
         let borrow_av =
           let ty = borrow_ty in
-          let value = ABorrow (AMutBorrow (bid0, mk_aignored span bv_ty)) in
+          let value =
+            ABorrow (AMutBorrow (PNone, bid0, mk_aignored span bv_ty))
+          in
           mk_typed_avalue span ty value
         in
 
         let loan_av =
           let ty = borrow_ty in
-          let value = ALoan (AMutLoan (nbid, mk_aignored span bv_ty)) in
+          let value = ALoan (AMutLoan (PNone, nbid, mk_aignored span bv_ty)) in
           mk_typed_avalue span ty value
         in
 
@@ -654,12 +660,12 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
         let bv_ty = bv.ty in
         cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span
           "Nested borrows are not supported yet";
-        let value = ABorrow (AMutBorrow (bid, mk_aignored span bv_ty)) in
+        let value = ABorrow (AMutBorrow (PNone, bid, mk_aignored span bv_ty)) in
         { value; ty = borrow_ty }
       in
       let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in
 
-      let loan = AMutLoan (bid2, mk_aignored span bv_ty) in
+      let loan = AMutLoan (PNone, bid2, mk_aignored span bv_ty) in
       (* Note that an aloan has a borrow type *)
       let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in
 
@@ -1213,26 +1219,30 @@ struct
   let match_distinct_aadts _ _ _ _ _ _ _ =
     raise (Distinct "match_distinct_adts")
 
-  let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty
-      =
+  let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _ty1 pm1
+      bid1 ty =
+    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     let bid = match_borrow_id bid0 bid1 in
-    let value = ABorrow (ASharedBorrow bid) in
+    let value = ABorrow (ASharedBorrow (PNone, bid)) in
     { value; ty }
 
-  let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1
-      _av1 ty av =
+  let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _av0 _ty1
+      pm1 bid1 _av1 ty av =
+    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     let bid = match_borrow_id bid0 bid1 in
-    let value = ABorrow (AMutBorrow (bid, av)) in
+    let value = ABorrow (AMutBorrow (PNone, bid, av)) in
     { value; ty }
 
-  let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1
-      ids1 _v1 _av1 ty v av =
+  let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 ids0 _v0 _av0
+      _ty1 pm1 ids1 _v1 _av1 ty v av =
+    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     let bids = match_loan_ids ids0 ids1 in
-    let value = ALoan (ASharedLoan (bids, v, av)) in
+    let value = ALoan (ASharedLoan (PNone, bids, v, av)) in
     { value; ty }
 
-  let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1
-      id1 _av1 ty av =
+  let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0 id0 _av0
+      _ty1 pm1 id1 _av1 ty av =
+    sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     log#ldebug
       (lazy
         ("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: "
@@ -1241,7 +1251,7 @@ struct
         ^ typed_avalue_to_string ~span:(Some span) ctx1 av));
 
     let id = match_loan_id id0 id1 in
-    let value = ALoan (AMutLoan (id, av)) in
+    let value = ALoan (AMutLoan (PNone, id, av)) in
     { value; ty }
 
   let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 =
@@ -1706,7 +1716,9 @@ let match_ctx_with_target (config : config) (span : Meta.span)
     let lookup_shared_loan lid ctx : typed_value =
       match snd (lookup_loan span ek_all lid ctx) with
       | Concrete (VSharedLoan (_, v)) -> v
-      | Abstract (ASharedLoan (_, v, _)) -> v
+      | Abstract (ASharedLoan (pm, _, v, _)) ->
+          sanity_check __FILE__ __LINE__ (pm = PNone) span;
+          v
       | _ -> craise __FILE__ __LINE__ span "Unreachable"
     in
     let lookup_in_src id = lookup_shared_loan id src_ctx in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index bcf92b25..fc882423 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -150,8 +150,8 @@ let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) :
       method! visit_aloan_content inside_abs lc =
         let _ =
           match lc with
-          | AMutLoan (bid, _) -> register_mut_loan inside_abs bid
-          | ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
+          | AMutLoan (_, bid, _) -> register_mut_loan inside_abs bid
+          | ASharedLoan (_, bids, _, _) -> register_shared_loan inside_abs bids
           | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan RMut bid
           | AIgnoredMutLoan (None, _)
           | AIgnoredSharedLoan _
@@ -522,7 +522,8 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
                 match glc with
                 | Concrete (VMutBorrow (_, bv)) ->
                     sanity_check __FILE__ __LINE__ (bv.ty = ty) span
-                | Abstract (AMutBorrow (_, sv)) ->
+                | Abstract (AMutBorrow (pm, _, sv)) ->
+                    sanity_check __FILE__ __LINE__ (pm = PNone) span;
                     sanity_check __FILE__ __LINE__
                       (Substitute.erase_regions sv.ty = ty)
                       span
@@ -612,15 +613,17 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
         | ABottom, _ -> (* Nothing to check *) ()
         | ABorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
-            | AMutBorrow (_, av), RMut ->
+            | AMutBorrow (pm, _, av), RMut ->
+                sanity_check __FILE__ __LINE__ (pm = PNone) span;
                 (* Check that the child value has the proper type *)
                 sanity_check __FILE__ __LINE__ (av.ty = ref_ty) span
-            | ASharedBorrow bid, RShared -> (
+            | ASharedBorrow (pm, bid), RShared -> (
+                sanity_check __FILE__ __LINE__ (pm = PNone) span;
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan span ek_all bid ctx in
                 match glc with
                 | Concrete (VSharedLoan (_, sv))
-                | Abstract (ASharedLoan (_, sv, _)) ->
+                | Abstract (ASharedLoan (_, _, sv, _)) ->
                     sanity_check __FILE__ __LINE__
                       (sv.ty = Substitute.erase_regions ref_ty)
                       span
@@ -635,8 +638,8 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
             | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
         | ALoan lc, aty -> (
             match lc with
-            | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
-              -> (
+            | AMutLoan (PNone, bid, child_av)
+            | AIgnoredMutLoan (Some bid, child_av) -> (
                 let borrowed_aty = aloan_get_expected_child_type aty in
                 sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span;
                 (* Lookup the borrowed value to check it has the proper type *)
@@ -646,22 +649,25 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
                     sanity_check __FILE__ __LINE__
                       (bv.ty = Substitute.erase_regions borrowed_aty)
                       span
-                | Abstract (AMutBorrow (_, sv)) ->
+                | Abstract (AMutBorrow (_, _, sv)) ->
                     sanity_check __FILE__ __LINE__
                       (Substitute.erase_regions sv.ty
                       = Substitute.erase_regions borrowed_aty)
                       span
                 | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
+            | AMutLoan (_, _, _) -> internal_error __FILE__ __LINE__ span
             | AIgnoredMutLoan (None, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
                 sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span
-            | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) ->
+            | ASharedLoan (PNone, _, sv, child_av)
+            | AEndedSharedLoan (sv, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
                 sanity_check __FILE__ __LINE__
                   (sv.ty = Substitute.erase_regions borrowed_aty)
                   span;
                 (* TODO: the type of aloans doesn't make sense, see above *)
                 sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span
+            | ASharedLoan (_, _, _, _) -> internal_error __FILE__ __LINE__ span
             | AEndedMutLoan { given_back; child; given_back_span = _ }
             | AEndedIgnoredMutLoan { given_back; child; given_back_span = _ } ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 8dfe0abe..71f8e4fc 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1666,7 +1666,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
   value
 
 (** Explore an abstraction value and convert it to a consumed value
-    by collecting all the span-values from the ended *loans*.
+    by collecting all the meta-values from the ended *loans*.
 
     Consumed values are rvalues because when an abstraction ends we
     introduce a call to a backward function in the synthesized program,
@@ -1720,10 +1720,10 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
 and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
     (lc : V.aloan_content) : texpression option =
   match lc with
-  | AMutLoan (_, _) | ASharedLoan (_, _, _) ->
+  | AMutLoan (_, _, _) | ASharedLoan (_, _, _, _) ->
       craise __FILE__ __LINE__ ctx.span "Unreachable"
   | AEndedMutLoan { child = _; given_back = _; given_back_span } ->
-      (* Return the span-value *)
+      (* Return the meta-value *)
       Some (typed_value_to_texpression ctx ectx given_back_span)
   | AEndedSharedLoan (_, _) ->
       (* We don't dive into shared loans: there is nothing to give back
@@ -1744,7 +1744,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
 and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
     texpression option =
   match bc with
-  | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
+  | V.AMutBorrow (_, _, _) | ASharedBorrow (_, _) | AIgnoredMutBorrow (_, _) ->
       craise __FILE__ __LINE__ _ctx.span "Unreachable"
   | AEndedMutBorrow (_, _) ->
       (* We collect consumed values: ignore *)
@@ -1804,7 +1804,7 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
   match p with None -> None | Some p -> Some (translate_mplace p)
 
 (** Explore an abstraction value and convert it to a given back value
-    by collecting all the span-values from the ended *borrows*.
+    by collecting all the meta-values from the ended *borrows*.
 
     Given back values are patterns, because when an abstraction ends, we
     introduce a call to a backward function in the synthesized program,
@@ -1867,7 +1867,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
 and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
     (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match lc with
-  | AMutLoan (_, _) | ASharedLoan (_, _, _) ->
+  | AMutLoan (_, _, _) | ASharedLoan (_, _, _, _) ->
       craise __FILE__ __LINE__ ctx.span "Unreachable"
   | AEndedMutLoan { child = _; given_back = _; given_back_span = _ }
   | AEndedSharedLoan (_, _) ->
@@ -1886,7 +1886,7 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
 and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
     (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match bc with
-  | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
+  | V.AMutBorrow (_, _, _) | ASharedBorrow (_, _) | AIgnoredMutBorrow (_, _) ->
       craise __FILE__ __LINE__ ctx.span "Unreachable"
   | AEndedMutBorrow (msv, _) ->
       (* Return the span-symbolic-value *)
@@ -1912,7 +1912,7 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
         ctx.span "Nested borrows are not supported yet";
       (ctx, None)
   | AEndedProjBorrows mv ->
-      (* Return the span-value *)
+      (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv ctx in
       (ctx, Some (mk_typed_pattern_from_var var mp))
   | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 96d61f88..ca33604d 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -153,7 +153,7 @@ and typed_value = { value : value; ty : ty }
 
 (** "Meta"-value: information we store for the synthesis.
 
-     Note that we never automatically visit the span-values with the
+     Note that we never automatically visit the meta-values with the
      visitors: they really are span information, and shouldn't be considered
      as part of the environment during a symbolic execution.
 
@@ -166,7 +166,7 @@ type mvalue = typed_value [@@deriving show, ord]
 
      See the explanations for {!mvalue}
 
-     TODO: we may want to create wrappers, to prevent mixing span values
+     TODO: we may want to create wrappers, to prevent mixing meta values
      and regular values.
  *)
 type msymbolic_value = symbolic_value [@@deriving show, ord]
@@ -278,7 +278,7 @@ and aproj =
           'a and one for 'b.
           
           We accumulate those values in the list of projections (note that
-          the span value stores the value which was given back).
+          the meta value stores the value which was given back).
           
           We can later end the projector of loans if [s@0] is not referenced
           anywhere in the context below a projector of borrows which intersects
@@ -290,14 +290,14 @@ and aproj =
           
           Also note that once given to a borrow projection, a symbolic value
           can't get updated/expanded: this means that we don't need to save
-          any span-value here.
+          any meta-value here.
        *)
   | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list
       (** An ended projector of loans over a symbolic value.
       
           See the explanations for {!AProjLoans}
           
-          Note that we keep the original symbolic value as a span-value.
+          Note that we keep the original symbolic value as a meta-value.
        *)
   | AEndedProjBorrows of msymbolic_value
       (** The only purpose of {!AEndedProjBorrows} is to store, for synthesis
@@ -621,7 +621,7 @@ and aborrow_content =
        *)
   | AEndedMutBorrow of msymbolic_value * typed_avalue
       (** The sole purpose of {!AEndedMutBorrow} is to store the (symbolic) value
-          that we gave back as a span-value, to help with the synthesis.
+          that we gave back as a meta-value, to help with the synthesis.
        *)
   | AEndedSharedBorrow
       (** We don't really need {!AEndedSharedBorrow}: we simply want to be