spec: eliminate the Implicit ownership default (0062)

Design spec for #55, superseding #54. Deletes ParamMode::Implicit in a
single cutover -> binary {Own, Borrow}; no defaulted ownership mode
survives on any fn-type slot, authored or compiler-synthesised.

The grounding pass corrected the central architecture claim. Both #55
and the first draft assumed a new return-provenance check was needed to
reject an own-return aliasing a borrowed binder, "silently accepted
today". Running the candidate fixtures through the live `ail check`
falsified that: consume-while-borrowed already rejects all three
provenance paths -- direct passthrough, let-indirection, and borrow
escaping into a returned constructor (regime A). Own-return soundness
and regime A are already-green properties. The cutover therefore adds
exactly one new check (borrow-return rejection) plus one signature-level
reject (borrow-over-value), not two new provenance analyses.

Scope decisions ratified: keyword stays verbal (own/borrow), ParamMode
keeps its name; totality is strict including value-type slots (every
slot moded, (own value) trivial, (borrow value) an error, bare slot a
parse error) so an LLM author needs no heap/value knowledge.

The leak fix (spec 0061 symptom) falls out of Implicit->Own at the
synthesis sites: the old typechecker made Implicit and Own
indistinguishable (mode_eq), so setting Own changes no typecheck
outcome -- it only flips the codegen dec gate from skip to emit.

Out of scope: re-enabling borrow-returns (needs the escape/liveness
axis), multi-return, mode polymorphism.

grounding-check: PASS (7 assumptions ratified against named green tests;
all fenced ail blocks validated against the live tool).

refs #55

docs/specs/0062-eliminate-implicit-mode.md

@@ -0,0 +1,490 @@
+# Eliminate the Implicit ownership default — Design Spec
+
+**Date:** 2026-06-01
+**Status:** Draft — awaiting user spec review
+**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<ParamMode>,
+  #[serde(default, skip_serializing_if = "ParamMode::is_implicit")] ret_mode: ParamMode,
+
+after:
+  param_modes: Vec<ParamMode>,   // 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).