AILang/docs/specs/0020-effect-op-borrow.md

Effect-op arguments are borrowed — Design Spec

Date: 2026-05-12 Status: Draft — awaiting user spec review Authors: Brummel (orchestrator) + Claude

Goal

Codify and implement the language rule that arguments to a Term::Do (effect-op call) are evaluated in borrow position, not consume position. The uniqueness and linearity passes today treat them as consumes, which both contradicts the intended semantics ("effects observe; they do not transfer ownership of their arguments") and produces a concrete bug: every heap-Str slab handed back by int_to_str / float_to_str and immediately printed via io/print_str leaks at scope close under --alloc=rc.

The two RED tests at crates/ail/tests/e2e.rs::int_to_str_drop_balances_rc_stats and ::str_field_in_adt_drops_heap_str_correctly (commit 592d87b) pin the leak; this milestone closes them. By doing so it also closes the heap-str-abi milestone's outstanding hs.5 work (DESIGN anchor + WhatsNew + audit-close), which was held up waiting for this gap to be named and fixed.

Architecture

The rule is symmetric with the already-shipped rule for Term::Ctor.args:

AST node	arg position	reason
Term::Ctor.args	Consume	constructor packs values into the cell; the cell owns them afterwards
Term::Do.args	Borrow (new)	effect-op observes; the caller still owns whatever pointer it passed in

This is a language rule, not a per-op annotation. EffectOpSig (crates/ailang-check/src/builtins.rs:32) deliberately stays as it is: no param_modes, no ret_mode. The kind is the ownership default — having an EffectOpSig at all means "borrow in, no out-ownership", just as having a Ctor at all means "consume in".

The rule lives at three check-time sites

• crates/ailang-check/src/uniqueness.rs:289-292 — today walks Term::Do { args, .. } with Position::Consume. Changes to Position::Borrow. Consequence: consume_count of a bare-Var argument is no longer bumped by the effect-op call, which is the signal the let-arm dec emission at crates/ailang-codegen/src/lib.rs:1430-1466 reads when deciding whether to free the binder at scope close.
• crates/ailang-check/src/linearity.rs:506-510 — today walks Term::Do { args, .. } with Position::Consume. Changes to Position::Borrow. Consequence: a binder passed only to effect-ops no longer triggers use-after-consume on a second effect-op use. Two io/print_str(s) calls in sequence become a normal double-borrow, not a linearity error.
• crates/ailang-check/src/linearity.rs:42 — doc comment that lists per-arm consume/borrow positions. The bullet Term::Ctor.args[*], Term::Do.args[*] — Consume splits: Term::Ctor.args[*] stays in the Consume bullet; Term::Do.args[*] moves to the Borrow bullet alongside Term::Match.scrutinee and Term::Clone.value.

The third site is a doc comment, but it is part of the rule: the documentation that lies about the analyser is itself the bug we are fixing.

DESIGN.md anchor

docs/DESIGN.md gets a new bullet under the uniqueness / effect section naming the rule symmetrically with the existing Ctor rule. This is the artefact the architect agent reads at audit time, so the rule has a single named home that future analyser code paths cannot accidentally diverge from.

Heap-Str-specific consequences

The rule alone does not close the heap-Str leak. Two ABI-level fixes follow from the rule's interaction with hs.4's runtime additions:

1. int_to_str and float_to_str switch to ret_mode: Own. The two functions allocate a fresh heap-Str slab via str_alloc (runtime/str.c, iter hs.3) and hand the only outstanding pointer back to the caller. The codegen trackability gate at crates/ailang-codegen/src/drop.rs:464-475 (iter 18g.2: is_rc_heap_allocated for a Term::App checks the callee's ret_mode == Own) is what tells the let-arm to emit a dec at scope close. Today both functions carry ret_mode: Implicit at crates/ailang-check/src/builtins.rs:203-212 (and the float counterpart at :193-202) plus the codegen-side synth-replay at crates/ailang-codegen/src/synth.rs:167-172 (float_to_str) and :174-180 (int_to_str). All four sites switch to Own.

2. drop_symbol_for_binder App arm gets a Str carve-out. With ret_mode: Own, the let-binder is tracked, and at scope close codegen routes through drop_symbol_for_binder(value=App, val_ssa=s) at crates/ailang-codegen/src/drop.rs:534-549. That arm reads the call's static return type and forms drop_<m>_<T>. For T = Str there is no such drop fn — Str is a built-in pointer type with no recursive children, the same case the field-drop arm already handles at crates/ailang-codegen/src/drop.rs:372-394 by returning "ailang_rc_dec". The carve-out adds the symmetric arm in the App branch: Type::Con { name: "Str", .. } → "ailang_rc_dec".

These two fixes are not part of the language rule. They are the shape the heap-Str realisation needs in order to benefit from the rule. A spec that named only the rule would leave the RED tests still red.

Components

Touched files:

• crates/ailang-check/src/uniqueness.rs:289-292 — Term::Do arg walk: Position::Consume → Position::Borrow.
• crates/ailang-check/src/linearity.rs:506-510 — Term::Do arg walk: Position::Consume → Position::Borrow.
• crates/ailang-check/src/linearity.rs:42 — doc-comment update: move Term::Do.args[*] from the Consume bullet to the Borrow bullet.
• crates/ailang-check/src/builtins.rs:193-202 — float_to_str signature: ret_mode: Implicit → Own.
• crates/ailang-check/src/builtins.rs:203-212 — int_to_str signature: ret_mode: Implicit → Own.
• crates/ailang-codegen/src/synth.rs:167-172 — float_to_str synth-replay: ret_mode: Implicit → Own.
• crates/ailang-codegen/src/synth.rs:174-180 — int_to_str synth-replay: ret_mode: Implicit → Own.
• crates/ailang-codegen/src/drop.rs:534-549 — App arm of drop_symbol_for_binder: add Type::Con { name: "Str", .. } → "ailang_rc_dec" carve-out before the generic format!("drop_{m}_{name}") fallthrough.
• docs/DESIGN.md — new bullet anchoring the Term::Do.args[*] = Borrow rule under the uniqueness / effect section.
• crates/ail/tests/e2e.rs::int_to_str_drop_balances_rc_stats — existing RED test; turns GREEN unchanged.
• crates/ail/tests/e2e.rs::str_field_in_adt_drops_heap_str_correctly — existing RED test; turns GREEN unchanged.
• crates/ail/tests/snapshots/ — IR snapshots affected by the new let-arm dec at int_to_str callsites may need regeneration. No snapshot in the current crates/ail/tests/snapshots/ directory invokes int_to_str directly, so this is expected to be a no-op; flagged here in case planner-recon finds otherwise.

Data flow

The change does not affect canonical-JSON bytes. ret_mode: Own is already a serialised ParamMode variant; Implicit is the back-compat default which serialises via skip_serializing_if = "ParamMode::is_implicit". Switching the value does not change the schema or the existing-fixture hashes, because no fixture in the workspace carries an explicit ret_mode: Implicit annotation on int_to_str or float_to_str (both are typechecker-installed, never user-written).

The change affects IR shape at exactly one class of callsite: let x = (app int_to_str ...) in body (and float variant). The new IR emits a call void @ailang_rc_dec(ptr %x) at scope close. Non-binding sites — (do io/print_str (app int_to_str ...)) without an intervening let — are unaffected because no let-binder exists for the dec to attach to.

Error handling

No new diagnostics. One existing diagnostic — over-strict-mode (Iter 19a / 19a.1) — becomes more sensitive: a (own T) parameter whose only use in the fn body is passing it to an effect-op now correctly fires the lint, because the body no longer counts that use as a consume.

This is the intended behaviour of the lint — the lint asks "is this (own T) annotation actually justified by a consume in the body?", and an effect-op call is not a consume. The flip surfaces parameters that were silently mis-annotated and is part of the milestone, not a regression.

Fixtures that fail the tightened lint will be re-annotated as part of this milestone's implementation iteration (planner will enumerate which ones during recon). If the planner finds the sweep nontrivial (more than a handful of fixtures), the re-annotation moves to its own follow-up iter rather than bloating the milestone.

Testing strategy

1. Existing RED tests flip to GREEN. int_to_str_drop_balances_rc_stats and str_field_in_adt_drops_heap_str_correctly at e2e.rs (commit 592d87b). No fixture or assertion changes — the strict allocs == frees && live == 0 invariants stay.
2. One new positive test: non-pointer effect-op arg. Bind a let-Int, pass it to io/print_int, run with --alloc=rc and AILANG_RC_STATS=1. Confirms the rule does not introduce spurious bookkeeping on primitive arguments (Int is not a pointer; there is no slab to free; allocs and frees stay at zero).
3. One new positive test: repeated effect-op borrow. Bind a let-Str (heap-allocated via int_to_str), pass it to io/print_str twice in sequence, confirm the fixture typechecks (no use-after-consume) and that the RC trace reports allocs == frees && live == 0.
4. Workspace-wide regression. cargo test --workspace, bench/cross_lang.py, bench/compile_check.py, bench/check.py all green. Any over-strict-mode-driven fixture re-annotations land in the same milestone.

Acceptance criteria

• Both existing RED tests at crates/ail/tests/e2e.rs pass with allocs == frees && live == 0.
• Two new positive tests added (Int-arg primitive, repeated Str-arg borrow) — both green.
• cargo test --workspace, bench/cross_lang.py, bench/compile_check.py, bench/check.py all green; any over-strict-mode failures resolved by fixture re-annotation inside the milestone.
• docs/DESIGN.md carries a new bullet under the uniqueness / effect section naming the Term::Do.args[*] = Borrow rule, symmetric with the existing Term::Ctor.args[*] = Consume treatment.
• docs/WhatsNew.md carries one entry written for the user-as-reader covering both the heap-Str RC close and the effect-op argument rule, in plain prose, no internals.
• The heap-str-abi milestone is effectively closed by this milestone — hs.5's "DESIGN anchor + WhatsNew + audit-close" rolls in here. No separate hs.5 ships.