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

# 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<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).