fix(borrow): whole-place assignment clears move-record (Refs #177)

`x = e` where LHS is a `PlaceVar` is a *write*, not a read.  Pre-fix,
StmtAssign called `check_use` on the LHS, which fired `UseAfterMove`
whenever `x` had been moved earlier — spuriously rejecting `let mut x;
drop(x); x = …; use(x)`.  This is the assignment-clears-move imprecision
called out in the deferred-items comment at lib/borrow.ml:1483, the
StmtAssign half of the Slice C' pairing.

Whole-place writes now skip `find_move` (keeping the exclusive-borrow
aliasing check) and drop any overlapping move-record after the RHS is
validated, reviving the place for subsequent uses.  Sub-place writes
(`x.f =`, `x[i] =`) keep `check_use` because they navigate through a
parent that must still be live.

Anti-regression preserved:
  - borrow_nll_still_rejects_live_borrow.affine (Slice A): assignment
    to a place with a live shared borrow still errors MoveWhileBorrowed.
  - slice_c_body_move_persists.affine (Slice C): a moved local that is
    NOT reassigned still errors UseAfterMove on later reads.
  - 327 prior tests, all green (328/328 with the new case).

Loop-soundness (Slice C' StmtWhile/StmtFor) can now proceed
independently — comment at lib/borrow.ml:1496 updated accordingly.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

lib/borrow.ml

@@ -1352,8 +1352,27 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
       if not (is_mutable state place) then
         Error (CannotBorrowAsMutable (place, expr_span lhs))
       else
-        (* Check that the place is not moved and not borrowed *)
-        let* () = check_use state place (expr_span lhs) in
+        (* CORE-01 pt3 / #177 deferred-items (lib/borrow.ml:1483):
+           assignment-clears-move.  A whole-place write (`x = e`,
+           LHS is [PlaceVar]) REVIVES the place — the LHS is a write,
+           not a read, so a prior move on it must not raise
+           [UseAfterMove], and after the RHS lands the move-record
+           rooted here is dropped so subsequent uses succeed.
+           Sub-place writes (`x.f = e`, `x[i] = e`) keep [check_use]
+           because they navigate through the parent place, which must
+           still be live.  Unblocks Slice C' loop-soundness. *)
+        let is_whole_place_write =
+          match place with PlaceVar _ -> true | _ -> false
+        in
+        let* () =
+          if is_whole_place_write then
+            match find_aliasing_exclusive state place with
+            | Some b ->
+              Error (UseWhileExclusivelyBorrowed (place, b, expr_span lhs))
+            | None -> Ok ()
+          else
+            check_use state place (expr_span lhs)
+        in
         (* Check for any active borrows of this place *)
         begin match List.find_opt (fun b -> places_overlap place b.b_place) state.borrows with
         | Some borrow ->
@@ -1386,6 +1405,10 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
             | _ -> None
           in
           let* () = check_expr ctx state symbols rhs in
+          if is_whole_place_write then
+            state.moved <-
+              List.filter (fun mr -> not (places_overlap mr.m_place place))
+                state.moved;
           (match pre_release with
            | Some binder_sym ->
              (match ref_source_borrow state symbols rhs with
@@ -1543,10 +1566,10 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
      change to the type system; ADR-gated.
    - Loop soundness (`StmtWhile`/`StmtFor`): a single body pass
      misses multi-iteration move conflicts.  A 2-iteration check
-     would catch them but requires fixing the assignment-clears-
-     move imprecision first (assignment is currently treated as a
-     read of LHS, so `x = …` after a prior move spuriously fails).
-     Couple Slice C' with the StmtAssign clear-on-rewrite fix.
+     would catch them.  Slice C''s StmtAssign clear-on-rewrite
+     half is now landed (see [StmtAssign] above and the
+     [is_whole_place_write] gate); the loop-soundness half can
+     proceed independently.
    - Tighter integration with the quantity checker for captured
      linears (Slice D).
 *)

test/e2e/fixtures/borrow_assign_clears_move.affine

@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 / #177 deferred-items: assignment-clears-move.
+// Pre-fix, `x = …` after a prior move of `x` was rejected with
+// UseAfterMove because StmtAssign treated the LHS as a read.  A
+// whole-place write must REVIVE the place: the assignment must
+// not fail, and subsequent reads of `x` must succeed.
+// Expected: Ok.
+
+module BorrowAssignClearsMove;
+
+fn drop_int(x: own Int) -> Unit = ();
+fn read_int(x: Int) -> Int = 0;
+
+fn revive_after_move() -> Int {
+  let mut x = 1;
+  drop_int(x);
+  x = 2;
+  read_int(x)
+}

test/test_e2e.ml

@@ -4454,6 +4454,21 @@ let test_ref_to_ref_assign_aliases () =
                     the subsequent write to `x` was spuriously \
                     rejected: " ^ Borrow.format_borrow_error e)
 
+(* CORE-01 pt3 / #177 deferred-items: assignment-clears-move.
+   Whole-place write `x = …` after a prior move on `x` revives the
+   place; the move-record is dropped after the RHS lands so the
+   subsequent read of `x` succeeds.  Anti-regression for the
+   sub-place case is covered by [test_slice_c_body_move_persists]
+   (which still expects UseAfterMove for a read of a moved local
+   that was *not* reassigned). *)
+let test_borrow_assign_clears_move () =
+  match borrow_result (fixture "borrow_assign_clears_move.affine") with
+  | Ok () -> ()
+  | Error e ->
+    Alcotest.fail ("assignment-clears-move: `x = …` after `drop_int(x)` \
+                    spuriously rejected — whole-place write should revive \
+                    the moved place: " ^ Borrow.format_borrow_error e)
+
 let borrow_tests = [
   Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block"
     `Quick test_borrow_outlives_owner;
@@ -4495,6 +4510,8 @@ let borrow_tests = [
     `Quick test_ref_to_ref_protects_owner;
   Alcotest.test_case "ref-to-ref assign-path: `r = s` releases + aliases (#177 pt3)"
     `Quick test_ref_to_ref_assign_aliases;
+  Alcotest.test_case "assignment-clears-move: whole-place write revives moved place (#177)"
+    `Quick test_borrow_assign_clears_move;
 ]
 
 (* ============================================================================