feat(borrow): CORE-01 Slice D (#177 pt3) — reject @linear capture by closure at borrow check

[hyperpolymath]

Summary

Tighter integration with the quantity checker for captured linears: the borrow checker now refuses to let a closure capture a @linear (QOne) binding. Pre-Slice-D, this case fell only to the quantity checker (which scales lambda captures by QOmega and emits `LinearVariableUsedMultiple`); now the same constraint fires earlier in the pipeline (Typecheck → Borrow → Quantity) with a diagnostic that points at the lambda span — the actual capture site — rather than the downstream "used multiple times" message.

Mechanism

• New `state.linear_bindings` tracks sym-ids of @linear bindings declared in the current function: explicit `@linear` annotations on `let`-statements and `let`-expressions, `@linear` function params, and `let x: Cmd[T] = …` (linear-by-construction per ADR-002).
• At `ExprLambda`, the free-var walk now also looks up each captured name's symbol and rejects with `LinearCapturedByClosure(name, lambda_span)` if the sym-id is in `linear_bindings`.
• The Shared-borrow creation for non-linear captures is unchanged.

Refs

• CORE-01: complete borrow checker Phase-3 (borrow-graph validation) #177 (CORE-01 pt3)
• Third of three small slices being landed today; feat(borrow): CORE-01 ref-to-ref binding (#177 pt3) — let r2 = r / r = s alias the borrow-graph #395 (ref-to-ref) and feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177) #396 (Slice C') are in flight. Slice C-full (Polonius) is being handed off to a separate Claude — prompt incoming separately.

Test plan

• `dune runtest --force` — 327 → 330 tests, 0 failures
• 3 new e2e fixtures + handlers:
  • `slice_d_captured_linear_let_rejected.affine` — `@linear let x; fn() => x + 1` → `LinearCapturedByClosure("x", _)`
  • `slice_d_captured_linear_param_rejected.affine` — `fn foo(@linear y: Int) { let f = fn() => y + 1; … }` → `LinearCapturedByClosure("y", _)`
  • `slice_d_captured_nonlinear_ok.affine` — anti-regression: non-linear capture must still pass

🤖 Generated with Claude Code

[hyperpolymath]

Parallel-work review (Slice D audit)

Slice D is the one deferred-items entry I didn't duplicate — I had no parallel PR open here. This is a fresh audit of the diff against the soundness story in the comment.

Two real bugs, two hygiene items, three suggested fixture adds.

---

1. Cmd _-typed parameters slip through the linear-capture check

Two paths populate state.linear_bindings:

Let-statements / let-expressions use the shared helper:

if let_is_linear lb.el_quantity lb.el_ty then
  state.linear_bindings <- sym.Symbol.sym_id :: state.linear_bindings

let_is_linear correctly falls back to borrow_quantity_of_ty ty_opt when the explicit quantity is None, so let x: Cmd[Int] = … (no explicit @linear) is tracked.

Parameters in check_function:

if p.p_quantity = Some QOne then
  state.linear_bindings <-
    sym.sym_id :: state.linear_bindings

This checks ONLY the explicit p_quantity = Some QOne annotation. A param c: Cmd[Int] (Cmd-typed, no explicit @linear) is QOne by Cmd _ inference but never reaches linear_bindings — the same call to borrow_quantity_of_ty that the let path makes is missing here.

Result: a closure capturing a Cmd-typed param silently slips through. The companion quantity-checker pass would still flag downstream "used multiple times" but the early borrow-side error that the PR comment promises does not fire.

Suggested fix — make the param path symmetric:

let p_is_linear =
  match p.p_quantity with
  | Some q -> q = QOne
  | None -> borrow_quantity_of_ty (Some p.p_ty) = QOne
in
if p_is_linear then
  state.linear_bindings <- sym.sym_id :: state.linear_bindings

(p.p_ty is not an option, so wrap in Some.)

2. The helper borrow_quantity_of_ty is unexercised by fixtures

Three fixtures, all using explicit @linear — none uses Cmd[T] to drive the inference branch of let_is_linear. So the helper's Some (TyApp ({ name = "Cmd"; _ }, _)) -> QOne arm is unreached by CI. If somebody later renames "Cmd" to "Linear" (or whatever the canonical name is) the linear inference silently breaks and no test catches it.

A fourth fixture along the lines of:

fn capture_cmd_let() -> Int {
  let c: Cmd[Int] = make_cmd();
  let f = fn() => use_cmd(c);
  f()
}

— expected LinearCapturedByClosure — would pin this path.

---

3. linear_bindings is not snapshot/restored at block exit

check_block snapshots borrows, block_local_syms, ref_bindings at entry and restores them at exit. linear_bindings is not in the snapshot:

let borrows_at_entry = state.borrows in
let block_locals_at_entry = state.block_local_syms in
let ref_bindings_at_entry = state.ref_bindings in
(* no linear_bindings_at_entry *)
...
state.borrows <- borrows_at_entry;
state.block_local_syms <- block_locals_at_entry;
state.ref_bindings <- ref_bindings_at_entry;
(* no restore of linear_bindings *)

So a @linear let x declared inside a nested block stays in linear_bindings after the block ends. Benign in practice because sym_ids don't recycle to in-scope symbols, but inconsistent with the rest of the state-field discipline and a foot-gun if a future change ever does mutate the linear_bindings list during block exit cleanup.

4. merge_arm_results does not unify linear_bindings

Same character as #3 — when match/try/handle arms merge, borrows/moved are unioned but linear_bindings entries created in arm $i$ aren't reconciled. Same benign-but-inconsistent footprint.

---

Coverage gaps in fixtures

Three adds that round out the matrix:

1. Cmd _ let captured (positive rejection via inference) — exercises borrow_quantity_of_ty's Cmd arm.
2. Cmd _ param captured (currently slips through per ci: Bump actions/setup-node from 4.0.2 to 6.3.0 #1) — would fail against the unfixed PR, pass against the patched version. The strongest regression for the param-path fix.
3. Shadowing: @linear let x = …; let x = 100; let f = fn() => x + 1; f() — the closure captures the inner non-linear x. Expected: Ok. Pins that the rejection scopes to the sym-id in linear_bindings, not the name.

---

What's architecturally fine

• The borrow_quantity_of_ty / let_is_linear helpers are sensibly duplicated in borrow.ml with the comment pointing at the canonical helper in quantity.ml.
• The lambda capture rejection fires before the existing shared-borrow loop — early exit and good span attribution.
• LinearCapturedByClosure (name, lam_span) carries enough context for a clean diagnostic, and the formatter is good.
• The deferred-items comment is correctly updated to remove the Slice D entry.

Nothing blocking — the only must-fix is #1 (param-path symmetry). Items #3 and #4 are hygiene; can land separately.