Make minor modifications

4 files changed, 25 insertions, 19 deletions

diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 3bef7b30..0469d58e 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -256,12 +256,12 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
       method! visit_aloan_content env lc =
         match lc with
         | AMutLoan (pm, bid, av) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGLoanContent (Abstract lc))
             else super#visit_AMutLoan env pm bid av
         | ASharedLoan (pm, bids, v, av) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if BorrowId.Set.mem l bids then
               raise (FoundGLoanContent (Abstract lc))
@@ -401,11 +401,11 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
       method! visit_aloan_content env lc =
         match lc with
         | AMutLoan (pm, bid, av) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then update () else super#visit_AMutLoan env pm bid av
         | ASharedLoan (pm, bids, v, av) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if BorrowId.Set.mem l bids then update ()
             else super#visit_ASharedLoan env pm bids v av
@@ -462,12 +462,12 @@ let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind)
       method! visit_aborrow_content env bc =
         match bc with
         | AMutBorrow (pm, bid, av) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
             else super#visit_AMutBorrow env pm bid av
         | ASharedBorrow (pm, bid) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
             else super#visit_ASharedBorrow env pm bid
@@ -584,12 +584,12 @@ let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
       method! visit_ABorrow env bc =
         match bc with
         | AMutBorrow (pm, bid, av) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then update ()
             else ABorrow (super#visit_AMutBorrow env pm bid av)
         | ASharedBorrow (pm, bid) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then update ()
             else ABorrow (super#visit_ASharedBorrow env pm bid)
@@ -1199,11 +1199,11 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
       method! visit_aloan_content env lc =
         match lc with
         | AMutLoan (pm, bid, _) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             raise (FoundBorrowIds (Borrow bid))
         | ASharedLoan (pm, bids, _, _) ->
-            (* Sanity check: markers can only appear when we're doing a join *)
+            (* Sanity check: projection markers can only appear when we're doing a join *)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             raise (FoundBorrowIds (Borrows bids))
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index a74017d1..b2de3b22 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -198,7 +198,7 @@ let rec access_projection (span : Meta.span) (access : projection_access)
                     craise __FILE__ __LINE__ span
                       "Expected a shared (abstraction) loan"
                 | _, Abstract (ASharedLoan (pm, bids, sv, _av)) -> (
-                    (* Sanity check: markers can only appear when we're doing a join *)
+                    (* Sanity check: projection markers can only appear when we're doing a join *)
                     sanity_check __FILE__ __LINE__ (pm = PNone) span;
                     (* Explore the shared value *)
                     match access_projection span access ctx update p' sv with
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index fc882423..50e6e87f 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -497,14 +497,14 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
         | VBorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | VSharedBorrow bid, RShared | VReservedMutBorrow bid, RMut -> (
-                (* Lookup the borrowed value to check it has the proper type *)
+                (* Lookup the borrowed value to check it has the proper type.
+                   Note that we ignore the marker: we will check it when
+                   checking the loan itself. *)
                 let _, glc = lookup_loan span ek_all bid ctx in
                 match glc with
-                | Concrete (VSharedLoan (_, sv)) ->
+                | Concrete (VSharedLoan (_, sv))
+                | Abstract (ASharedLoan (_, _, sv, _)) ->
                     sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span
-                | Abstract (ASharedLoan (pm, _, sv, _)) ->
-                    sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span;
-                    sanity_check __FILE__ __LINE__ (pm = PNone) span
                 | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
             | VMutBorrow (_, bv), RMut ->
                 sanity_check __FILE__ __LINE__
@@ -517,12 +517,13 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
             | VSharedLoan (_, sv) ->
                 sanity_check __FILE__ __LINE__ (sv.ty = ty) span
             | VMutLoan bid -> (
-                (* Lookup the borrowed value to check it has the proper type *)
+                (* Lookup the borrowed value to check it has the proper type. *)
                 let glc = lookup_borrow span ek_all bid ctx in
                 match glc with
                 | Concrete (VMutBorrow (_, bv)) ->
                     sanity_check __FILE__ __LINE__ (bv.ty = ty) span
                 | Abstract (AMutBorrow (pm, _, sv)) ->
+                    (* The marker check is redundant, but doesn't cost much *)
                     sanity_check __FILE__ __LINE__ (pm = PNone) span;
                     sanity_check __FILE__ __LINE__
                       (Substitute.erase_regions sv.ty = ty)
@@ -655,7 +656,9 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
                       = Substitute.erase_regions borrowed_aty)
                       span
                 | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
-            | AMutLoan (_, _, _) -> internal_error __FILE__ __LINE__ span
+            | AMutLoan (_, _, _) ->
+                (* We get there if the projection marker is not [PNone] *)
+                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
@@ -667,7 +670,9 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
                   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
+            | ASharedLoan (_, _, _, _) ->
+                (* We get there if the projection marker is not [PNone] *)
+                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/Print.ml b/compiler/Print.ml
index 9a3a7d16..7495d6bf 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -148,6 +148,7 @@ module Values = struct
     | AEndedProjBorrows _mv -> "_"
     | AIgnoredProjBorrows -> "_"
 
+  (** Wrap a value inside its marker, if there is one *)
   let add_proj_marker (pm : proj_marker) (s : string) : string =
     match pm with
     | PNone -> s