Fix more bugs

2 files changed, 14 insertions, 7 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index ca1f87f1..fbd958ef 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -5,6 +5,7 @@ module Subst = Substitute
 module L = Logging
 open Utils
 open ValuesUtils
+open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 open InterpreterProjectors
@@ -265,6 +266,11 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
           | None -> failwith "Unreachable"
           | Some abs -> abs.V.regions
         in
+        (* Rk.: there is a small issue with the types of the aloan values *)
+        let borrowed_value_aty =
+          let _, ty, _ = ty_get_ref ty in
+          ty
+        in
         match lc with
         | V.AMutLoan (bid', child) ->
             if bid' = bid then (
@@ -276,7 +282,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               (* Apply the projection *)
               let given_back =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  regions nv ty
+                  regions nv borrowed_value_aty
               in
               (* Return the new value *)
               V.ALoan (V.AEndedMutLoan { given_back; child }))
@@ -302,7 +308,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
                * (i.e., we don't call [set_replaced]) *)
               let given_back =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  regions nv ty
+                  regions nv borrowed_value_aty
               in
               V.ALoan (V.AEndedIgnoredMutLoan { given_back; child })
             else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index b723d861..11b00381 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -523,14 +523,15 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 | _ -> failwith "Inconsistent context")
             | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
               ->
-                let ty = Subst.erase_regions aty in
-                assert (sv.V.ty = ty);
+                let borrowed_aty = aloan_get_expected_child_type aty in
+                assert (sv.V.ty = Subst.erase_regions borrowed_aty);
                 (* TODO: the type of aloans doesn't make sense, see above *)
-                assert (child_av.V.ty = aloan_get_expected_child_type aty)
+                assert (child_av.V.ty = borrowed_aty)
             | V.AEndedMutLoan { given_back; child }
             | V.AEndedIgnoredMutLoan { given_back; child } ->
-                assert (given_back.V.ty = aloan_get_expected_child_type aty);
-                assert (child.V.ty = aloan_get_expected_child_type aty)
+                let borrowed_aty = aloan_get_expected_child_type aty in
+                assert (given_back.V.ty = borrowed_aty);
+                assert (child.V.ty = borrowed_aty)
             | V.AIgnoredSharedLoan child_av ->
                 assert (child_av.V.ty = aloan_get_expected_child_type aty))
         | V.ASymbolic aproj, ty ->