Make give_back_symbolic_value fail in case we need to reinsert inside an

AProjLoans: there is something wrong

2 files changed, 16 insertions, 4 deletions

diff --git a/TODO.md b/TODO.md
index b9ae7934..8edb8fe6 100644
--- a/TODO.md
+++ b/TODO.md
@@ -61,8 +61,8 @@
    abstractions) is wrong.
    We get things like :
    `AProjLoans (s0 <: &'a mut T) [AProjBorrows (s1 <: &'a mut T)]`
-   while in the case of `s1` we should ignore the outer borrow (we
-   gave back something because this borrow ended...).
+   while in the case of `s1` we should ignore the outer borrow (what we give
+   back actually has type `T`...)
   
 * write a function to check that the code we are about to synthesize is in the proper
   subset. In particular:
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 24521335..ad7b5b2c 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -437,6 +437,8 @@ let give_back_symbolic_value (_config : C.config)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
   let subst (_abs : V.abs) local_given_back =
+    (* See the below comments: there is something wrong here *)
+    let _ = raise Errors.Unimplemented in
     (* Compute the projection over the given back value *)
     let child_proj =
       match nsv.sv_kind with
@@ -450,11 +452,21 @@ let give_back_symbolic_value (_config : C.config)
            * (and MUST) forget the borrows *)
           V.AIgnoredProjBorrows
       | V.FunCallGivenBack ->
-          (* The value was fed as input to a function, and was given back *)
+          (* TODO: there is something wrong here.
+           * Consider this:
+           * ```
+           * abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
+           * abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
+           * ```
+           *
+           * Upon ending abs1, we give back some fresh symbolic value `s1`,
+           * that we reinsert where the loan for `s0` is. However, the mutable
+           * borrow in the type `&'a mut T` was ended: we give back a value of
+           * type `T`! We thus *mustn't* introduce a projector here.
+           *)
           V.AProjBorrows (nsv, sv.V.sv_ty)
       | _ -> failwith "Unreachable"
     in
-    (* TODO: this actually doesn't work, or at least there is something subtle... *)
     V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
   update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx