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:

(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:

(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:

(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:

(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:

(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:

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:

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:

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:

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):

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):

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):

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