# Eliminate the Implicit ownership default — Design Spec **Date:** 2026-06-01 **Status:** Approved (user, 2026-06-01). Soundness re-validated against post-#56 HEAD: the three own-return-provenance / regime-A fixtures still exit 1 under `[consume-while-borrowed]` — #56's application-is-a-borrow change does not weaken them (none is an application of a borrowed binder; all are return/let/ctor consume positions, untouched by #56). **Authors:** orchestrator + Claude ## Goal Delete `ParamMode::Implicit` from the language in a single cutover. `ParamMode` becomes binary `{Own, Borrow}`. After this cycle no fn-type slot — parameter or return, authored or compiler-synthesised — carries a defaulted ownership mode. Every authored slot reads `(own T)` or `(borrow T)`; every compiler-synthesised fn-type carries a concrete `Own`. This closes #55 and supersedes #54. It also fixes the typed-MIR fieldtest leak (spec 0061): the leak is the observable symptom of the real defect, which is that `Implicit` is read two ways — the typechecker treats `Implicit ≡ Own` (`mode_eq`, `crates/ailang-core/src/ast.rs:894`), while codegen omits the caller `dec` for it (`crates/ailang-codegen/src/drop.rs:476`), so the same fn-type means two different things. Removing the variant removes the fork. The design rationale is `design/models/0008-ownership-totality.md` §§1–3 (the totality principle: a default cannot be half-removed) and the 2026-06-01 design review (full totality is not atomically shippable *because of* borrow-returns; this spec carves them out). The model is `status: Design exploration` — its claims are validated against the live tool by this spec, not assumed. ### What the grounding work changed in this spec Both #55 and the first draft of this spec assumed a **new return-provenance check** was needed to reject an `own` return that aliases a borrowed binder (the `fn f(x: (borrow T)) -> (own T) { x }` passthrough), and that this passthrough is "silently accepted today". Running the candidate fixtures through the live `ail check` (traces in the Testing section) **falsified that assumption**: the existing `consume-while-borrowed` analysis already rejects all three provenance paths — - direct passthrough `(body b)` → rejected today; - let-indirection `(body (let y b y))` → rejected today; - borrow escaping into a returned constructor `(body (term-ctor Wrap Wrap b))` (regime A, model §5.1) → rejected today. A borrow parameter holds a live borrow for the whole function body, so *any* use of it at a consume position (own-return, ctor arg, own-param arg) trips `consume-while-borrowed`. **Own-return soundness and regime A are therefore already-green properties, not new work.** The cutover adds exactly **one** new check (borrow-return rejection) plus one signature-level reject (borrow-over-value), not two new provenance analyses. This is the central correction the grounding pass produced. ### Scope decisions ratified here 1. **Keyword form stays verbal** (`own` / `borrow`, today's surface). No adjectival rename, no keyword churn. The internal type keeps the name `ParamMode`. *(User decision, 2026-06-01.)* 2. **Totality is strict, including value-type slots.** Every fn-type slot carries `(own T)` or `(borrow T)`, value types included. `(own (con Int))` is trivial-own (no inc/dec ever emitted); `(borrow (con Int))` is a check error (§3.2 of the model). Bare type in a fn-type slot is rejected by the parser everywhere. Rationale: this gives an LLM author a heap/value-agnostic rule — *always write a mode; `own` is always safe; reach for `borrow` only when you want a heap view* — so the author never needs to know which types are boxed. The alternative (bare = trivial-own for value types only) forces exactly that heap/value classification on every slot and is rejected. ### Out of scope - **Re-enabling borrow-returns.** `(ret (borrow T))` is a check error in this cut, with a diagnostic naming the liveness/escape gap. The escape/liveness axis that would make borrow-returns sound is separate later work (model §5.2, §8). - **Multi-return** (model §5.3, §7-Q4). - **Mode polymorphism** (model §4). A type-variable slot takes a concrete `own`/`borrow`; the surface already cannot express a mode variable, so no change is needed. ## Architecture The cutover has four schema/representation edits, one new check, one new signature-level reject, and one corpus migration. They land together: a deleted `Implicit` means returns must be `own`/`borrow`, every checked-in `.ail` source carries `Implicit` slots today, and the hash shift is one-time for the whole corpus. **Schema / representation (`crates/ailang-core`):** 1. `ParamMode` loses the `Implicit` variant and `#[derive(Default)]` — ownership has no default, so the type has no default. 2. `Type::Fn::param_modes` / `ret_mode` lose their `skip_serializing_if` elision. Modes are always serialised. This is the one-time canonical-JSON hash shift for the whole corpus. 3. `mode_eq` (the `Implicit ≡ Own` interchange) is deleted; mode equality becomes structural `==`. 4. `Type::fn_implicit` is renamed `Type::fn_owned` and sets `Own` on every synthesised slot (justified in Data flow). **New check (`crates/ailang-check`):** 5. **Borrow-return rejection.** `(ret (borrow T))` is a check error with a diagnostic pointing at the out-of-scope liveness axis. This is the *only* genuinely new ownership analysis in the cycle. **New signature-level reject (`crates/ailang-check`):** 6. **Borrow-over-value.** `(borrow value-type)` in any slot is a check error, fired on the signature before body analysis so it does not depend on the body tripping `consume-while-borrowed`. Specified by model §3.2; this cycle makes it reachable now that every value slot is moded. **Parser (`crates/ailang-surface`):** 7. A bare type in a fn-type slot is a parse error. The slot grammar becomes `fn-type-param ::= "(" ("borrow" | "own") type ")"` — the bare-`type` alternative is removed. **Migration:** 8. Every `.ail` source (prelude, kernel `raw_buf`, the ~208 example fixtures) gets explicit modes. Param modes are derived from the existing uniqueness/consume analysis (consumed ⇒ `own`, read-only ⇒ `borrow`; value types always `own`); return modes are `own` everywhere (no borrow-return survives). The hash-pin tests reset their pinned hashes once. **Already-green, pinned not built:** own-return provenance and regime A are enforced by the existing `consume-while-borrowed` check. The cycle adds regression pins (Testing) proving the schema deletion does not weaken them, but builds no new analysis for them. ## Concrete code shapes Every block below was run through the configured `ail check`; the exit-code traces are in the Testing section. ### User-facing: the post-cutover authoring surface (checks clean today) The canonical form an LLM author writes after this cycle. Every slot carries a mode; value-type slots use trivial-`own`: ```ail (module ownership_total (data List (doc "Monomorphic singly-linked Int list — boxed, recursive.") (ctor Nil) (ctor Cons (con Int) (con List))) (fn list_length (doc "Borrow the list, count its elements.") (type (fn-type (params (borrow (con List))) (ret (own (con Int))))) (params xs) (body (match xs (case (pat-ctor Nil) 0) (case (pat-ctor Cons h t) (app + 1 (app list_length t)))))) (fn sum_list (doc "Consume the list, sum its elements.") (type (fn-type (params (own (con List))) (ret (own (con Int))))) (params xs) (body (match xs (case (pat-ctor Nil) 0) (case (pat-ctor Cons h t) (app + h (app sum_list t)))))) (fn main (doc "Build [1,2,3]; print length (3) then sum (6).") (type (fn-type (params) (ret (own (con Unit))) (effects IO))) (params) (body (let xs (term-ctor List Cons 1 (term-ctor List Cons 2 (term-ctor List Cons 3 (term-ctor List Nil)))) (seq (seq (app print (app list_length xs)) (do io/print_str "\n")) (seq (app print (app sum_list xs)) (do io/print_str "\n"))))))) ``` This is the feature-acceptance evidence: an LLM author writes a mode on every slot, never a bare type, and never needs to know that `Int` is unboxed and `List` is boxed — `own` is the always-safe choice, `borrow` the deliberate heap-view on `list_length`'s parameter. ### New RED fixture: borrow-return rejection The one new check. Wellformed today (no return check exists), a check error post-cutover; the diagnostic names the liveness gap and the out-of-scope status: ```ail (module borrow_return_reject (data Box (doc "Heap cell holding one Int.") (ctor Box (con Int))) (fn peek (doc "MUST FAIL post-cutover: borrow-return is refcount-invisible and can outlive its source; re-enabling needs the escape axis.") (type (fn-type (params (own (con Box))) (ret (borrow (con Box))))) (params b) (body b))) ``` ### New RED fixture: borrow-over-value Wellformed today, a signature-level check error post-cutover. The body ignores the param so the rejection is unambiguously about the signature, not a body-level consume: ```ail (module borrow_value_reject (fn ignore (doc "MUST FAIL post-cutover: borrow over a value type is meaningless.") (type (fn-type (params (borrow (con Int))) (ret (own (con Int))))) (params n) (body 0))) ``` ### New parser reject: bare type in a fn-type slot Wellformed today (bare = `Implicit`), a parse error post-cutover: ```ail (module bare_slot_reject (fn id (doc "MUST FAIL post-cutover: bare `(con Int)` slot carries no mode.") (type (fn-type (params (con Int)) (ret (con Int)))) (params x) (body x))) ``` ### Already-green regression pin: own-return provenance + regime A These are **rejected today** by `consume-while-borrowed`. They are pinned as regressions to prove the schema deletion does not weaken the existing guard — not as new checks: ```ail (module own_return_provenance_reject (data Box (doc "Heap cell holding one Int.") (ctor Box (con Int))) (fn passthrough (doc "Already rejected today (consume-while-borrowed): own-return aliases a borrowed binder.") (type (fn-type (params (borrow (con Box))) (ret (own (con Box))))) (params b) (body b))) ``` ### North-star: the fixed leak `examples/rc_let_implicit_returning_app.ail` asserts `live=1` today as an intentional Implicit back-compat lane. Post-cutover its return is `own`, the caller `dec` is emitted, and the property flips to `live=0`. The fixture header and its property-3 assertion are rewritten from "Implicit leaks by design" to "own-return frees correctly". ### Secondary: implementation shapes (before → after) *Supporting detail, not the headline.* **`crates/ailang-core/src/ast.rs` — `ParamMode`:** ```text before: #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)] #[serde(rename_all = "lowercase")] pub enum ParamMode { #[default] Implicit, Own, Borrow } after: #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] #[serde(rename_all = "lowercase")] pub enum ParamMode { Own, // (own T) — caller transfers ownership; callee consumes Borrow, // (borrow T) — caller retains ownership; callee may not consume } // no #[derive(Default)]: ownership has no default. ``` **`crates/ailang-core/src/ast.rs` — `Type::Fn` serde:** ```text before: #[serde(default, skip_serializing_if = "all_implicit")] param_modes: Vec, #[serde(default, skip_serializing_if = "ParamMode::is_implicit")] ret_mode: ParamMode, after: param_modes: Vec, // always present, len == params.len() ret_mode: ParamMode, // always present // all_implicit / is_implicit helpers deleted. ``` **`crates/ailang-core/src/ast.rs` — `mode_eq` deleted:** ```text before: fn mode_eq(a, b) { Implicit and Own interchangeable; Borrow distinct } after: removed; modes compared with derived PartialEq (a == b) ``` **`crates/ailang-core/src/ast.rs` — `fn_implicit` → `fn_owned`:** ```text before: pub fn fn_implicit(params, ret, effects) -> Type // sets Implicit after: pub fn fn_owned(params, ret, effects) -> Type // sets Own // 16 call sites updated; Own is correct by the Data-flow argument. ``` **`crates/ailang-codegen/src/drop.rs` — App ret-mode gate (`:467–478`):** ```text before: matches!(m, ParamMode::Own) with Implicit/Borrow → no dec (the leak) after: matches!(m, ParamMode::Own) unchanged in form; the Implicit case no longer exists, so every former-Implicit return now matches Own and is dec'd. Comment updated to drop the Implicit back-compat language. ``` **`crates/ailang-surface/src/parse.rs` — slot grammar (`:32`, `parse_param_with_mode`):** ```text before: fn-type-param ::= type | "(" "borrow" type ")" | "(" "own" type ")" after: fn-type-param ::= "(" "borrow" type ")" | "(" "own" type ")" // bare type → ParseError (no mode on slot) ``` ## Components - **`ailang-core::ast`** — the enum, the `Type::Fn` fields, the constructor, equality. Blast-radius origin. - **`ailang-surface::parse` / `print`** — slot grammar gains a reject arm; printer drops the `Implicit` arm (`print.rs:360`). - **`ailang-check::uniqueness` / `linearity`** — host the borrow-return reject and the borrow-over-value reject (both signature inspections). The migration mode-derivation reuses `consume_count`. No new provenance analysis — `consume-while-borrowed` (`linearity.rs:1272`) already covers own-return provenance and regime A. - **`ailang-codegen::drop` / `lambda` / `match_lower` / `lib`** — every `ParamMode::Implicit` match arm deleted; gate logic unchanged in form. - **`.ail` corpus** — prelude, `raw_buf`, examples; mechanically re-moded then reviewed. ## Data flow **Why `Own` is correct for every synthesised slot (`fn_owned`).** `Implicit` had two roles: the authoring default (bare type) and the internal marker for fn-types the compiler builds (lambda types, builtin signatures, inferred application results). The authoring role is deleted. The synthesis role resolves to `Own` with no behaviour change: the old typechecker made `Implicit` and `Own` indistinguishable (`mode_eq` true for every `Implicit`/`Own` pairing), so every synthesised fn-type was already semantically `Own` under typechecking — no check ever depended on a slot being `Implicit` rather than `Own`. Setting `Own` at synthesis changes no typecheck outcome. It changes exactly one thing: the codegen gate (`drop.rs:476`) flips from "skip the caller `dec`" to "emit it" for those former-`Implicit` returns — precisely the leak fix. The synthesis sites do not need the consume analysis (that is for *authored* params during migration); `Own` is correct for them by construction. The corpus typecheck/codegen suite is the regression net for this claim (Testing). **Migration mode-derivation.** For each authored param: run the uniqueness pass, read `consume_count` — `> 0 ⇒ (own T)`, `== 0 ⇒ (borrow T)` for heap types, `(own T)` for value types. For each return: `(own T)` (no borrow-return survives; any borrow-passthrough body is now rejected and must be restructured — and is already rejected today, so the corpus contains none). Derived sources are reviewed by the orchestrator before commit — the author owns the annotations; the derivation is a drafting aid, not a surviving default. **Check flow for the new rejects.** Both the borrow-return reject and the borrow-over-value reject are signature inspections on the fn-type, fired before body dataflow — no new tracking. Own-return provenance and regime A need no flow here: `consume-while-borrowed` already fires because a borrow parameter's borrow is live across the whole body, so any consume of it (return-as-own, ctor arg) is caught. Ctor args are `Position::Consume` (`linearity.rs:527`), which is why regime A holds — a borrowed value cannot escape into a returned constructor. ## Error handling - **Bare slot (parse error).** `parse_param_with_mode` returns a `ParseError` when a slot is a bare type, naming the slot and requiring `(own …)` or `(borrow …)`. Rendered in AILang syntax. - **Borrow-return (check error, new).** New `CheckError` variant. States `(ret (borrow …))` is not permitted in this language version and points at the liveness/escape axis — an honest "not yet". - **Borrow-over-value (check error, new).** New `CheckError` variant. Signature-level: borrow is meaningless over an unboxed value type. - **Own-return provenance.** No new diagnostic — `consume-while-borrowed` already covers it; its message is unchanged. Each new `CheckError` variant gets a stable code via the existing `CheckError::code()` registry (the diagnostic registry — not a separate doc list). ## Testing strategy Live `ail check` traces of the spec's fixtures (run 2026-06-01, `target/debug/ail`): ```text ownership_total.ail : exit 0 ok (surface checks + runs) bare_slot_reject.ail : exit 0 (legal today; parser reject post-cutover) borrow_return_reject.ail : exit 0 (legal today; new check post-cutover) borrow_value_reject.ail : exit 0 (legal today; new sig reject post-cutover) own_return_provenance_reject.ail : exit 1 error: [consume-while-borrowed] passthrough: `b` ... let-indirection (let y b y) : exit 1 error: [consume-while-borrowed] f: `b` ... ctor-escape (term-ctor Wrap b) : exit 1 error: [consume-while-borrowed] f: `b` ... (regime A) ``` - **New RED fixtures** (`borrow_return_reject`, `borrow_value_reject`, `bare_slot_reject`) land under `examples/`, each asserting the specific diagnostic fires post-cutover. These are the RED side of the one new check, the one new signature reject, and the parser reject. - **Already-green regression pins** (`own_return_provenance_reject` and the let-indirection / ctor-escape variants) assert `consume-while-borrowed` still fires after the schema deletion. They protect the own-return-soundness and regime-A properties the cycle relies on but does not build. - **North-star leak flip.** `rc_let_implicit_returning_app.ail` and its pin family (`crates/ail/tests/print_no_leak_pin.rs`) flip from `live=1` to `live=0` under `AILANG_RC_STATS`. - **Hash-pin reset.** `crates/ailang-core/tests/hash_pin.rs` and `crates/ailang-surface/tests/prelude_module_hash_pin.rs` get their pinned hashes regenerated once and re-asserted (memory: hash-pin blast-radius audit — both sites). - **Round-trip invariant.** `ailang-surface` round-trip tests stay green with modes always present; add a case proving a bare-slot input now fails to parse. - **Synthesis-site behaviour.** The corpus typecheck/codegen suite is the regression net for `fn_implicit → fn_owned`: if any synthesised slot was not semantically `Own`, a test breaks. Green corpus ratifies the Data-flow argument. - **Full workspace suite**, not just e2e — typed-MIR re-synth strictness (memory) means mode changes surface in `lower_to_mir` re-unification; run `cargo test --workspace`. ## Acceptance criteria 1. `ParamMode` has exactly two variants `{Own, Borrow}`, no `Default`, no `Implicit` anywhere in `crates/` (grep clean). 2. The parser rejects a bare type in any fn-type slot; round-trip tests prove it. 3. `borrow_return_reject` and `borrow_value_reject` fail their checks with the specified diagnostics; the post-cutover authoring-surface module checks and runs clean. 4. The own-return-provenance / regime-A pins stay red (`consume-while-borrowed` fires) after the deletion. 5. `rc_let_implicit_returning_app.ail` reports `live=0` under `AILANG_RC_STATS` (leak fixed). 6. `cargo test --workspace` green, with hash-pins regenerated once and re-asserted. 7. `design/contracts/0008-memory-model.md` sections describing `Implicit` (`:180-182`, `:288-298`) are updated to the binary model as part of this cycle (a contract change rides with the feature that forces it).