AILang/docs/plans/0121-eliminate-implicit-mode.md

Eliminate the Implicit ownership default — Implementation Plan

Parent spec: docs/specs/0062-eliminate-implicit-mode.md

For agentic workers: REQUIRED SUB-SKILL: use the implement skill to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Delete ParamMode::Implicit in a single cutover so ParamMode becomes binary {Own, Borrow} and no fn-type slot — authored or synthesised — carries a defaulted ownership mode.

Architecture: Four tasks. Tasks 1–2 add the two new signature-level rejects (borrow-return, borrow-over-value) while Implicit still exists — each leaves a green, independently committable tree. Task 3 builds a throwaway ail migrate-modes subcommand (parse → map Implicit↦Own, keep explicit Own/Borrow → print explicit → write back) and unit-tests it without touching the corpus. Task 4 is the atomic cutover: run the migration tool over the whole .ail corpus, hand-fix the read-only-heap params the now-universal linearity check flags as over-consuming, then delete the variant + all its compile sites (compiler-driven), add the parser bare-slot reject, reset the five hash pins, flip the leak pin, update both affected contracts, and remove the throwaway subcommand.

Tech Stack: ailang-core (ast.rs schema, primitives.rs is_value_type), ailang-surface (parse.rs slot grammar, print.rs slot printer), ailang-check (lib.rs signature checks + CheckError registry, linearity.rs/uniqueness.rs activation gate), ail (throwaway migration subcommand), the .ail corpus, the design ledger contracts 0002/0008.

---

Recon corrections folded into this plan

The spec's enumeration drifted from the tree; the authoritative figures the plan executes against (verified by plan-recon, 2026-06-01):

• Kernel migration path: the spec/issue cite crates/ailang-kernel/src/kernel_stub/source.ail — that path does not exist (kernel_stub retired in raw-buf.4 per CLAUDE.md). The live kernel-tier source is crates/ailang-kernel/src/raw_buf/source.ail.
• Hash pins: FIVE, not two. The spec named crates/ailang-core/tests/hash_pin.rs and crates/ailang-surface/tests/prelude_module_hash_pin.rs. Three more carry fn-type-bearing hex pins that the mode-serialisation change shifts: crates/ailang-core/tests/embed_export_hash_stable.rs:32, crates/ail/tests/eq_ord_e2e.rs:139, crates/ail/tests/mono_hash_stability.rs (the eq__/compare__/ show__ block, :63-68,:107-110).
• Second contract. The spec's acceptance criterion 7 names only design/contracts/0008-memory-model.md. design/contracts/0002-data-model.md also documents the "implicit" JSON form and implicit ≡ own, and is drift-anchored by design_schema_drift.rs:design_md_anchors_every_parammode_variant. The honesty rule forces it to update in the same iteration. Both contracts update.
• Counts: ~261 example fixtures carry (fn-type slots (spec said ~208); fn_implicit has 16 call sites + 1 def = 17 references (spec said 16). The compiler is the authoritative enumerator for the synthesis-site Own migration; do not hand-count.
• Lambda annotations are NOT moded slots. parse_lam (parse.rs:1518) reads (typed name type) params and (ret type) via parse_type(), not parse_param_with_mode. The bare-slot reject (Task 4) therefore hits (fn-type …) slots only; lambda type annotations stay bare and are untouched by the migration.

Files this plan creates or modifies

• Create: examples/borrow_return_reject.ail — RED fixture, borrow-return reject (Task 1)
• Create: examples/borrow_value_reject.ail — RED fixture, borrow-over-value reject (Task 4 Step B2)
• Modify: crates/ailang-codegen/src/subst.rs:165 — mono-coercion (borrow value-type)→(own value-type) (Task 4 Step B1)
• Create: examples/bare_slot_reject.ail — RED fixture, parser bare-slot reject (Task 4)
• Create: examples/own_return_provenance_reject.ail (+ _let, _ctor variants) — already-green consume-while-borrowed regression pins (Task 4)
• Create: examples/ownership_total.ail — post-cutover authoring-surface GREEN fixture (Task 4)
• Modify: crates/ailang-check/src/lib.rs — two new CheckError variants + code() entries + signature-check wiring (:2240); the ~50 ret_mode: ParamMode::Implicit synthesis literals → Own (Task 4)
• Modify: crates/ailang-core/src/ast.rs:778-953 — ParamMode enum, Type::Fn serde, fn_implicit→fn_owned, helper deletion, PartialEq (Task 4)
• Modify: crates/ailang-surface/src/parse.rs:1180-1222 — bare-slot reject + elision deletion (Task 4)
• Modify: crates/ailang-surface/src/print.rs:357-360,:408 — delete Implicit arm (Task 4)
• Modify: crates/ailang-codegen/src/{drop.rs:467-478,lambda.rs:164,lib.rs} — Implicit→Own synthesis + comment (Task 4)
• Modify: crates/ailang-core/src/{desugar.rs,pretty.rs} — synthesis literals → Own (Task 4)
• Modify: crates/ailang-prose/src/lib.rs:456,… — delete Implicit arm + synthesis literals (Task 4)
• Modify: crates/ailang-check/src/{linearity.rs:356,385,reuse_shape.rs:110,uniqueness.rs} — dead activation-gate arm collapse (Task 4)
• Modify: examples/*.ail (261), examples/prelude.ail, crates/ailang-kernel/src/raw_buf/source.ail — corpus migration (Task 4)
• Modify: the five hash-pin test files (Task 4)
• Modify: examples/rc_let_implicit_returning_app.ail + crates/ail/tests/print_no_leak_pin.rs — leak flip (Task 4)
• Modify: crates/ailang-core/tests/{schema_coverage.rs,design_schema_drift.rs} — delete ParamModeImplicit tag + exemplar (Task 4)
• Modify: design/contracts/0008-memory-model.md, design/contracts/0002-data-model.md — binary-model prose (Task 4)
• Create (throwaway, removed in Task 4): ail migrate-modes subcommand in crates/ail/src/main.rs (Task 3)
• Test: crates/ail/tests/migrate_modes.rs — migration-tool unit test (Task 3, removed in Task 4)

---

Task 1: New check — borrow-return rejection

(ret (borrow T)) becomes a check error. Independent of Implicit; the tree stays green and this task is independently committable.

Files:

• Create: examples/borrow_return_reject.ail

• Modify: crates/ailang-check/src/lib.rs (CheckError enum ~:404, code() ~:837, signature check ~:2275)

• Test: crates/ail/tests/mode_signature_rejects.rs (new, CLI-boundary E2E)

• Step 1: Write the RED fixture

Create examples/borrow_return_reject.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)))

• Step 2: Write the failing test (CLI-boundary, the project's reject-pin pattern)

Create crates/ail/tests/mode_signature_rejects.rs — modelled verbatim on crates/ail/tests/raw_buf_new_type_arg_pin.rs (run ail check on the fixture, assert non-zero exit + stderr carries the code):

//! Signature-level mode rejects added by spec 0062: borrow-return
//! (`(ret (borrow T))`) and borrow-over-value (`(borrow value-type)`).
//! CLI-boundary E2E (the project's reject-pin pattern): the diagnostic
//! is the observable exit behaviour of `ail check`.
use std::path::{Path, PathBuf};
use std::process::Command;

fn repo_root() -> PathBuf {
    Path::new(env!("CARGO_MANIFEST_DIR")).parent().unwrap().parent().unwrap().to_path_buf()
}

fn check_rejects_with(fixture: &str, code: &str) {
    let path = repo_root().join("examples").join(fixture);
    let out = Command::new(env!("CARGO_BIN_EXE_ail"))
        .arg("check").arg(&path).output().expect("ail check spawn");
    assert!(!out.status.success(),
        "expected `ail check {fixture}` to REJECT, but it passed: stdout={}",
        String::from_utf8_lossy(&out.stdout));
    let stderr = String::from_utf8_lossy(&out.stderr);
    assert!(stderr.contains(code), "expected code `{code}`, got: {stderr}");
}

/// `(ret (borrow T))` is rejected with code `borrow-return-not-permitted`.
#[test]
fn borrow_return_is_rejected() {
    check_rejects_with("borrow_return_reject.ail", "borrow-return-not-permitted");
}

• Step 3: Run the test to verify it fails

Run: cargo test -p ail --test mode_signature_rejects borrow_return_is_rejected Expected: FAIL — today the fixture checks clean (no return check exists), so ail check exits 0 and the !out.status.success() assert fires.

• Step 4: Add the CheckError variant

In crates/ailang-check/src/lib.rs, in pub enum CheckError (after the last variant Internal(_)'s neighbours — place next to the other signature rejects), add:

    /// A fn-type return slot is `(borrow T)`. Borrow-returns are
    /// refcount-invisible and can outlive their source; re-enabling
    /// them needs the escape/liveness axis (out of scope, spec 0062
    /// §"Out of scope"). Code: `borrow-return-not-permitted`.
    #[error("borrow-return not permitted for `{0}`: a (borrow …) return is refcount-invisible and can outlive its source; this language version forbids it (the escape/liveness axis that would make it sound is not yet built)")]
    BorrowReturnNotPermitted(String),

• Step 5: Register the code

In fn code(&self), add before CheckError::Internal(_) => "internal",:

            CheckError::BorrowReturnNotPermitted(_) => "borrow-return-not-permitted",

• Step 6: Fire the check at the fn signature

In check_def (crates/ailang-check/src/lib.rs), the fn signature is destructured at :2240:

    let (param_tys, ret_ty, declared_effs) = match &inner_ty {
        Type::Fn { params, ret, effects, .. } => {
            (params.clone(), (**ret).clone(), effects.clone())
        }

Change the pattern to also bind ret_mode (leave param_modes under .. — Task 1 does not read it; Task 4 Step B2 widens further), and after the existing check_type_well_formed(&ret_ty, &env)?; line (:2275) add the reject. First, widen the destructure:

    let (param_tys, ret_ty, ret_mode, declared_effs) = match &inner_ty {
        Type::Fn { params, ret, ret_mode, effects, .. } => {
            (params.clone(), (**ret).clone(), *ret_mode, effects.clone())
        }
        other => {
            return Err(CheckError::FnTypeRequired(
                f.name.clone(),
                ailang_core::pretty::type_to_string(other),
            ));
        }
    };

Then immediately after check_type_well_formed(&ret_ty, &env)?;:

    // spec 0062: borrow-returns are refcount-invisible — forbidden in
    // this language version (the escape/liveness axis is unbuilt).
    if matches!(ret_mode, ParamMode::Borrow) {
        return Err(CheckError::BorrowReturnNotPermitted(f.name.clone()));
    }

Ensure ParamMode is in scope in lib.rs (it is — param_modes are already referenced elsewhere in the file). Task 1 binds only ret_mode, leaving param_modes under .., so there is no unused binding. Task 4 Step B2 widens this same destructure to also bind param_modes (its borrow-over-value loop is the first reader).

• Step 7: Run the test to verify it passes

Run: cargo build -p ail && cargo test -p ail --test mode_signature_rejects borrow_return_is_rejected Expected: PASS

• Step 8: Confirm no corpus fixture regresses

Run: cargo build -p ail && python3 bench/check.py Expected: 0 regressions (no checked-in fixture has a (ret (borrow …)) — the spec asserts none survive, and consume-while-borrowed already rejects the body shapes that would force one).

---

Task 2: New signature reject — borrow-over-value — FOLDED INTO TASK 4

Finding during implementation (2026-06-01), re-staged. The borrow-over-value reject CANNOT land green in isolation before the cutover. The prelude's polymorphic comparison builtins are declared (fn-type (params (borrow a) (borrow a)) (ret …)) (eq, compare, lt/le/gt/ge, …). When the mono pass specialises a := Int (or Bool/Float), apply_subst_to_type (subst.rs:165) produces compare__Int(borrow Int, borrow Int) — i.e. the language's OWN generated code is in the forbidden (borrow value-type) shape. The standalone check broke compare_{int,bool}_mono_symbol_emits_branch_ladder (ailang-codegen lib tests) with borrow over value type in compare__Int.

The spec's rule is universal ("value types always own", model §3.2), so the language's generated code must honour it too — the principled fix is that the mono pass coerces (borrow value-type) → (own value-type) when specialising a polymorphic borrow param onto a value type (semantically a no-op: value types are never refcounted, so own vs borrow emits no inc/dec and the branch-ladder IR is unchanged). The check and the coercion are therefore a matched pair and land together in Task 4 (which touches the mono/codegen path anyway), not as a standalone pre-cutover task.

Spec gap to record at the next brainstorm touch of 0062: the borrow-over-value rule needs the mono-coercion clause spelled out; the spec tested only the authored case.

The borrow-over-value variant + check + fixture + the borrow_over_value_is_rejected test + the mono-coercion now live in Task 4 Phase B Steps B1–B2 below.

---

Task 3: Throwaway migration tool — ail migrate-modes

A parse → Implicit↦Own → print-explicit → write-back pass, run over the corpus in Task 4. Own/Borrow are preserved verbatim. This is semantically invisible today (PartialEq treats Implicit == Own, ast.rs:mode_eq), so the migrated corpus still typechecks identically — but it materialises the modes so the post-cutover parser (which rejects bare slots) accepts the sources. Throwaway: removed in Task 4 once Implicit is deleted (the subcommand would not compile).

Files:

• Modify: crates/ail/src/main.rs (add MigrateModes subcommand)

• Test: crates/ail/tests/migrate_modes.rs (new)

• Step 1: Write the failing tool test

Create crates/ail/tests/migrate_modes.rs:

//! Throwaway migration-tool test (spec 0062). Asserts the
//! parse→Implicit↦Own→print pass materialises bare slots as `(own …)`
//! and leaves explicit `(borrow …)` untouched. Deleted in the cutover.
use ailang_surface::{parse, print};
use ailang_core::ast::ParamMode;

/// Re-implements the tool's core transform for the unit test so the
/// assertion does not depend on the CLI I/O wrapper.
fn migrate_text(src: &str) -> String {
    let mut m = parse(src).expect("parse");
    ailang_core::ast::for_each_fn_type_mut(&mut m, &mut |params_len, pm, rm| {
        pm.resize(params_len, ParamMode::Own);
        for x in pm.iter_mut() {
            if matches!(x, ParamMode::Implicit) { *x = ParamMode::Own; }
        }
        if matches!(rm, ParamMode::Implicit) { *rm = ParamMode::Own; }
    });
    print(&m)
}

#[test]
fn bare_slot_becomes_own_borrow_preserved() {
    let src = "(module m\n  (fn f\n    (doc \"d\")\n    (type (fn-type (params (con Int) (borrow (con Int))) (ret (con Int))))\n    (params x y)\n    (body x)))\n";
    let out = migrate_text(src);
    assert!(out.contains("(params (own (con Int)) (borrow (con Int)))"), "got: {out}");
    assert!(out.contains("(ret (own (con Int)))"), "got: {out}");
}

ailang_surface::parse (parse.rs:125, -> Result<Module, ParseError>) and ailang_surface::print (print.rs:17, -> String) are the verified public entry points. for_each_fn_type_mut is introduced in Step 2.

• Step 2: Add the AST fn-type walker

In crates/ailang-core/src/ast.rs, add a public mutator that visits every Type::Fn reachable from a module's defs (signatures incl. Forall bodies, and nested fn-types inside param/ret/arg types). The callback receives the param count, a &mut Vec<ParamMode>, and a &mut ParamMode:

/// Visit every `Type::Fn` in `m`, letting `f` rewrite its modes.
/// `f(params_len, param_modes, ret_mode)`. Used by the throwaway
/// `migrate-modes` tool (spec 0062); has no other caller and is
/// removed if the migration machinery is retired.
pub fn for_each_fn_type_mut(
    m: &mut Module,
    f: &mut impl FnMut(usize, &mut Vec<ParamMode>, &mut ParamMode),
) {
    fn walk_ty(t: &mut Type, f: &mut impl FnMut(usize, &mut Vec<ParamMode>, &mut ParamMode)) {
        match t {
            Type::Fn { params, param_modes, ret, ret_mode, .. } => {
                let n = params.len();
                for p in params.iter_mut() { walk_ty(p, f); }
                walk_ty(ret, f);
                f(n, param_modes, ret_mode);
            }
            Type::Con { args, .. } => { for a in args.iter_mut() { walk_ty(a, f); } }
            Type::Forall { body, .. } => walk_ty(body, f),
            Type::Var { .. } => {}
        }
    }
    for def in m.defs.iter_mut() {
        if let Def::Fn(fd) = def {
            walk_ty(&mut fd.ty, f);
        }
    }
}

The implementer confirms the Module/Def/FnDef field names (m.defs, Def::Fn(fd), fd.ty) against the actual ast.rs; the recon-confirmed shape is Def::Fn(f) => f.ty (lib.rs:1427).

• Step 3: Run the tool test to verify it fails

Run: cargo test -p ail --test migrate_modes Expected: FAIL — for_each_fn_type_mut is new; before Step 2 it does not compile, after Step 2 the test should compile and pass. (If it passes immediately after Step 2, that is the GREEN; the RED was the compile failure pinning the missing walker.)

• Step 4: Add the throwaway CLI subcommand

In crates/ail/src/main.rs, add a MigrateModes { path: PathBuf } arm to enum Cmd and a handler that reads the file, runs the same transform as migrate_text (factored into a shared fn or duplicated — this is throwaway), and writes the printed result back in place:

    /// THROWAWAY (spec 0062): rewrite every bare fn-type slot in a
    /// `.ail` file as `(own …)`, preserving explicit `(own)`/`(borrow)`.
    /// Removed in the Implicit-deletion cutover.
    MigrateModes { path: std::path::PathBuf },

Handler (in the match on Cmd):

        Cmd::MigrateModes { path } => {
            let src = std::fs::read_to_string(&path)?;
            let mut m = ailang_surface::parse(&src)?;
            ailang_core::ast::for_each_fn_type_mut(&mut m, &mut |n, pm, rm| {
                pm.resize(n, ailang_core::ast::ParamMode::Own);
                for x in pm.iter_mut() {
                    if matches!(x, ailang_core::ast::ParamMode::Implicit) {
                        *x = ailang_core::ast::ParamMode::Own;
                    }
                }
                if matches!(rm, ailang_core::ast::ParamMode::Implicit) {
                    *rm = ailang_core::ast::ParamMode::Own;
                }
            });
            std::fs::write(&path, ailang_surface::print(&m))?;
            Ok(())
        }

Match the handler's error type / Ok(()) shape to the sibling arms in main.rs; the recon confirms enum Cmd at main.rs:63.

• Step 5: Build the tool

Run: cargo build -p ail Expected: 0 errors. target/debug/ail migrate-modes <file> now exists.

• Step 6: Full-suite gate (no corpus touched yet)

Run: cargo test --workspace Expected: green — Task 3 is purely additive; no corpus file or schema changed.

---

Task 4: The atomic cutover

Everything that cannot land except together: run the migration over the corpus, delete the variant + all compile sites, parser reject, hash resets, leak flip, contract updates, drift-pin updates, new fixtures. A deleted variant makes the whole workspace fail to compile until every site is migrated, and the parser reject breaks every bare slot until the corpus is migrated — so all of it is one task with a single green gate at the end. The compiler is the authoritative site enumerator.

Files: all under "Files this plan creates or modifies" tagged (Task 4), plus removal of the Task 3 throwaway.

Phase A — migrate the corpus (Implicit still present, tree green)

• Step 1: Run the migration tool over the whole corpus

Run:

cargo build -p ail
for f in (find examples -name '*.ail') examples/prelude.ail crates/ailang-kernel/src/raw_buf/source.ail
  ./target/debug/ail migrate-modes $f
end

(fish syntax; the implementer adapts to the available shell. The find already includes examples/prelude.ail, so the explicit repeat is harmless — dedupe if preferred.) Expected: every .ail file rewritten with explicit modes on every fn-type slot; bare slots gone.

• Step 2: Verify the migrated corpus parses and round-trips

Run: cargo build -p ail && python3 bench/check.py Expected: 0 regressions. (Sources are now explicit own/borrow; bare slots are still legal under the current parser, so anything the tool missed still parses — but check.py must stay green. The round-trip invariant is enforced by the build deriving JSON via parse.)

• Step 3: Activate the strict check early via the migration, fix over-consuming params

Migrating a fn to explicit modes turns on the (today gated-off) strict linearity check for it — exactly the universal activation #56 hardened. A bare heap param the tool set to (own …) that the body only reads, and which a caller passes while retaining, now trips consume-while-borrowed / use-after-consume.

Run: cargo test --workspace 2>&1 | grep -iE 'consume-while-borrowed|use-after-consume|over-strict' For each flagged fn: change the offending param's (own …) to (borrow …) in its .ail source (the suggested_mode: "borrow" diagnostic names the param). Re-run until the grep is empty. Expected (final): no linearity errors; the corpus encodes the derived modes (consumed ⇒ own, read-only-heap ⇒ borrow, value ⇒ own).

This is the spec's "derived from the existing uniqueness/consume analysis … reviewed by the orchestrator" — the tool drafts blanket own, the universal check flags the read-only-heap params, and the fix is mechanical and check-gated. The orchestrator reviews the full mode diff before commit (the derivation is a drafting aid, not a surviving default).

Phase B — delete the variant (compiler-driven site set)

Phase B order: Steps 4–8 (schema + compiler-driven migration + parser

• printer + drift tag) first, THEN Steps B1–B2 (mono-coercion + borrow-over-value), because B1 relies on Step 4's length invariant (param_modes.len() == params.len(), the elision gone) and B2's check must not fire until B1 has coerced the generated value-type-borrow instances. Final Phase-B gate is at B2.

• Step 4: Edit ParamMode and Type::Fn serde in ast.rs

In crates/ailang-core/src/ast.rs:

Replace the Type::Fn field attributes (:780, :783) — drop the elision:

    Fn {
        params: Vec<Type>,
        param_modes: Vec<ParamMode>,
        ret: Box<Type>,
        ret_mode: ParamMode,
        #[serde(default)]
        effects: Vec<String>,
    },

Replace fn fn_implicit (:837) with fn_owned:

    /// Build a `Type::Fn` with every parameter mode and the return
    /// mode set to `ParamMode::Own`. The synthesis form for every
    /// typechecker / desugar / codegen site that builds a fn-type;
    /// `Own` is correct by construction (spec 0062 Data flow: the old
    /// typechecker made `Implicit ≡ Own`, so synthesised fn-types were
    /// already semantically `Own`).
    pub fn fn_owned(params: Vec<Type>, ret: Type, effects: Vec<String>) -> Type {
        let n = params.len();
        Type::Fn {
            params,
            param_modes: vec![ParamMode::Own; n],
            ret: Box::new(ret),
            ret_mode: ParamMode::Own,
            effects,
        }
    }

Replace the ParamMode enum (:860) — drop Default + Implicit:

/// Per-parameter / return mode marker on a [`Type::Fn`]. Full
/// contract lives in `design/contracts/0008-memory-model.md`.
/// Ownership has no default: every fn-type slot carries an explicit
/// `Own` or `Borrow` (spec 0062).
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "lowercase")]
pub enum ParamMode {
    /// `(own T)` — caller transfers ownership; callee consumes.
    Own,
    /// `(borrow T)` — caller retains ownership; callee may not consume.
    Borrow,
}

Delete impl ParamMode { fn is_implicit } (:872-878), fn all_implicit (:880-887), fn mode_eq (:889-901), and fn mode_slices_eq (:903-919).

In impl PartialEq for Type, replace the Type::Fn arm's mode comparison (:946-947):

                ap == bp
                    && ar == br
                    && apm == bpm
                    && arm == brm
                    && {
                        let mut a = ae.clone();
                        let mut b = be.clone();
                        a.sort();
                        b.sort();
                        a == b
                    }

• Step 5: Compiler-driven migration of all remaining sites

Run: cargo build --workspace 2>&1 | rg 'ParamMode::Implicit|fn_implicit|mode_eq|all_implicit|is_implicit|mode_slices_eq'

Apply the deterministic decision rule to every reported site (no judgement calls):

• ret_mode: ParamMode::Implicit / param_modes: vec![ParamMode::Implicit; n] / .insert(_, ParamMode::Implicit) — a synthesis site → replace Implicit with Own.
• .unwrap_or(ParamMode::Implicit) — modes are always present now → the .unwrap_or(...)/.get(i).copied().unwrap_or(...) becomes a direct index (param_modes[i]) or .unwrap_or(ParamMode::Own) if a fallback is structurally still needed; prefer the direct index where the length invariant (param_modes.len() == params.len()) holds.
• matches!(m, ParamMode::Implicit) in an activation gate (linearity.rs:356, reuse_shape.rs:110) — the any(Implicit) disjunct is now always false → delete that disjunct (gate reduces to its other condition, e.g. params.is_empty()).
• ParamMode::Own | ParamMode::Implicit => … match arm (linearity.rs:385) → collapse to ParamMode::Own => ….
• ParamMode::Implicit => write_type(out, t) (printer print.rs:360, prose lib.rs:456) → delete the arm (the match mode is now exhaustive over {Own, Borrow}).
• fn_implicit( callers (17 references) → fn_owned(.
• mode_eq / mode_slices_eq callers → already handled in Step 4 (only caller was PartialEq).

Repeat cargo build --workspace until 0 errors. Expected (final): cargo build --workspace 0 errors, and git grep -nE 'ParamMode::Implicit|fn_implicit|is_implicit|all_implicit|mode_eq|mode_slices_eq' crates/ is empty (acceptance criterion 1).

• Step 6: Parser — reject bare slots, delete elision

In crates/ailang-surface/src/parse.rs, replace the bare fallthrough in parse_param_with_mode (:1220-1221):

        // bare type in a fn-type slot is no longer permitted (spec 0062):
        // every slot must carry (own …) or (borrow …).
        let tok = self.peek().cloned();
        Err(self.error_at(tok, "fn-type slot requires a mode: write (own T) or (borrow T)"))

The implementer uses the crate's actual ParseError constructor (the helper the sibling parse errors in this file already use); the load-bearing behaviour is "bare slot → Err", verified by Step 12's fixture.

In parse_fn_type, delete the all-Implicit elision (:1180-1187) — store param_modes directly:

        Ok(Type::Fn {
            params,
            ret: Box::new(ret),
            effects,
            param_modes,
            ret_mode,
        })

• Step 7: Printer — drop the Implicit arm

In crates/ailang-surface/src/print.rs, write_fn_type_slot (:357) becomes exhaustive over {Own, Borrow} (Step 5 already deleted the Implicit arm); change the param_modes.get(i).copied().unwrap_or(ParamMode::Implicit) at :408 to a direct index param_modes[i] (length invariant holds post-cutover).

• Step 8: Delete the ParamModeImplicit drift tag + exemplar

• crates/ailang-core/tests/schema_coverage.rs:70,114,345 — delete the VariantTag::ParamModeImplicit enum value and its exhaustive-match arm so the coverage test no longer expects an "implicit" form.

• crates/ailang-core/tests/design_schema_drift.rs:385,392 — delete the "implicit" exemplar row and the match arm that asserts it serialises and is doc-anchored.

• Step B1: Mono-coercion — (borrow value-type) → (own value-type)

The prelude's polymorphic comparison builtins are (params (borrow a) …) (eq/compare/lt/…); specialising a to a value type would emit compare__Int(borrow Int, …), which Step B2's check forbids. Coerce at the mono specialisation site so the language's generated code honours "value types always own". In crates/ailang-codegen/src/subst.rs, apply_subst_to_type's Type::Fn arm (:165), recompute the modes after substituting the slot types:

        Type::Fn { params, ret, effects, param_modes, ret_mode } => {
            let new_params: Vec<Type> = params.iter().map(|p| apply_subst_to_type(p, subst)).collect();
            let new_ret = apply_subst_to_type(ret, subst);
            // spec 0062: a polymorphic (borrow a) specialised onto a
            // value type becomes (own value-type) — borrow-over-value is
            // forbidden and is a no-op for unboxed types (no RC).
            let coerce = |ty: &Type, m: &ParamMode| -> ParamMode {
                if matches!(m, ParamMode::Borrow) {
                    if let Type::Con { name, args } = ty {
                        if args.is_empty() && ailang_core::primitives::is_value_type(name) {
                            return ParamMode::Own;
                        }
                    }
                }
                *m
            };
            let new_param_modes: Vec<ParamMode> = new_params.iter().zip(param_modes.iter())
                .map(|(t, m)| coerce(t, m)).collect();
            let new_ret_mode = coerce(&new_ret, ret_mode);
            Type::Fn {
                params: new_params,
                ret: Box::new(new_ret),
                effects: effects.clone(),
                param_modes: new_param_modes,
                ret_mode: new_ret_mode,
            }
        }

Runs after Step 4, so the length invariant param_modes.len() == params.len() is in force (the elision is gone) and the .zip is total. ParamMode is already in scope in subst.rs (the arm binds param_modes/ret_mode).

• Step B2: borrow-over-value reject (corpus re-mode + check + fixture + test)

First re-mode any authored (borrow value-type) left in the corpus (the migration tool left explicit Borrow untouched in Phase A, so e.g. examples/mq3_class_eq_vs_fn_eq_fnmod.ail's (params (borrow (con Int)) (borrow (con Int))) is still present):

Run: git grep -lE '\(borrow \(con (Int|Bool|Float|Unit)\)' examples crates/ailang-kernel For each hit, replace (borrow (con <Value>)) with (own (con <Value>)). Re-run the grep until empty.

Add the CheckError variant to pub enum CheckError (crates/ailang-check/src/lib.rs):

    /// A fn-type slot is `(borrow V)` where `V` is an unboxed value
    /// type (`Int`/`Bool`/`Float`/`Unit`). Borrow is meaningless over
    /// a value type — it has no refcount and is copied by value
    /// (model §3.2). Code: `borrow-over-value`.
    #[error("borrow over value type in `{def}`: `{ty}` is an unboxed value type and cannot be borrowed; use `(own {ty})`")]
    BorrowOverValueType { def: String, ty: String },

Register the code in fn code(&self) before CheckError::Internal(_):

            CheckError::BorrowOverValueType { .. } => "borrow-over-value",

In check_def, first widen Task 1's destructure to also bind param_modes (it was left under .. in Task 1 Step 6):

    let (param_tys, param_modes, ret_ty, ret_mode, declared_effs) = match &inner_ty {
        Type::Fn { params, param_modes, ret, ret_mode, effects } => (
            params.clone(), param_modes.clone(), (**ret).clone(), *ret_mode, effects.clone(),
        ),
        other => {
            return Err(CheckError::FnTypeRequired(
                f.name.clone(),
                ailang_core::pretty::type_to_string(other),
            ));
        }
    };

Then, after the borrow-return check, add the borrow-over-value loop:

    // spec 0062: borrow over an unboxed value type is meaningless.
    // Fired on the signature, before body dataflow. The mono-coercion
    // (subst.rs, Step B1) guarantees no generated value-type-borrow
    // instance reaches here.
    for (ty, mode) in param_tys.iter().zip(param_modes.iter()) {
        if matches!(mode, ParamMode::Borrow) {
            if let Type::Con { name, args } = ty {
                if args.is_empty() && ailang_core::primitives::is_value_type(name) {
                    return Err(CheckError::BorrowOverValueType {
                        def: f.name.clone(),
                        ty: name.clone(),
                    });
                }
            }
        }
    }

Create examples/borrow_value_reject.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)))

Add to crates/ail/tests/mode_signature_rejects.rs (the check_rejects_with helper is created in Task 1 Step 2):

/// `(borrow value-type)` is rejected with code `borrow-over-value`.
#[test]
fn borrow_over_value_is_rejected() {
    check_rejects_with("borrow_value_reject.ail", "borrow-over-value");
}

Gate: cargo test -p ailang-codegen --lib compare — the compare_{int,bool}_mono_symbol_emits_branch_ladder tests PASS (the mono-coercion makes their value-type params own; branch-ladder IR is unchanged — value types emit no RC ops). And cargo test -p ail --test mode_signature_rejects PASS (all three: borrow-return, borrow-over-value, provenance pins).

Phase C — pins, fixtures, contracts

• Step 9: Reset all five hash pins

For each pin, regenerate the expected hex from the migrated module and re-assert (do not hand-edit blindly — recompute):

• crates/ailang-core/tests/hash_pin.rs — sum, IntList, and :257/:266/:275.
• crates/ailang-surface/tests/prelude_module_hash_pin.rs:50.
• crates/ailang-core/tests/embed_export_hash_stable.rs:32.
• crates/ail/tests/eq_ord_e2e.rs:139.
• crates/ail/tests/mono_hash_stability.rs:63-68,107-110.

Procedure per pin: run the test, read the assertion failed: left == right actual value, paste the new hex into the pin, re-run.

Run: cargo test --workspace 2>&1 | rg 'hash|pin' until the pin tests pass. Expected: each pin holds the post-migration hash; this is the one-time corpus-wide reset (spec §6, "the single irreversible step").

• Step 10: Flip the leak pin

• examples/rc_let_implicit_returning_app.ail — its return is now (own …) (migrated in Phase A). Rewrite the file header and the property-3 assertion from "Implicit leaks by design" / live=1 to "own-return frees correctly" / live=0.

• crates/ail/tests/print_no_leak_pin.rs — change the pinned AILANG_RC_STATS expectation for this fixture from live=1 to live=0; update the doc comment (:26) that mentions ParamMode::Implicit.

Run: cargo test -p ail --test print_no_leak_pin Expected: PASS with live=0 (acceptance criterion 5).

• Step 11: Add the regression-pin + authoring-surface fixtures

Create these (each verified to ail check at the stated exit code — see "Spec fixture parse-gate" below):

examples/own_return_provenance_reject.ail (exit 1, consume-while-borrowed):

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

examples/own_return_provenance_let.ail (exit 1) — body (let y b y); examples/own_return_provenance_ctor.ail (exit 1) — adds (data Wrap (doc "Wraps a Box.") (ctor Wrap (con Box))) and body (term-ctor Wrap Wrap b) with ret (own (con Wrap)) (regime A).

examples/ownership_total.ail (exit 0) — the post-cutover authoring-surface module verbatim from spec 0062 §"User-facing" (list_length borrows, sum_list owns, main builds [1,2,3]).

Add a test asserting each provenance fixture still exits 1 under the post-cutover check (extend crates/ail/tests/mode_signature_rejects.rs, reusing the check_rejects_with helper from Task 1 Step 2):

/// The own-return-provenance / regime-A shapes stay rejected by
/// `consume-while-borrowed` after the schema deletion (spec 0062
/// already-green pins — these are NOT new checks).
#[test]
fn own_return_provenance_still_rejected() {
    for f in ["own_return_provenance_reject.ail",
              "own_return_provenance_let.ail",
              "own_return_provenance_ctor.ail"] {
        check_rejects_with(f, "consume-while-borrowed");
    }
}

• Step 12: Add the parser bare-slot RED fixture + test

Create examples/bare_slot_reject.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)))

Add a parser test (in crates/ailang-surface/tests/) asserting this source now fails to parse:

#[test]
fn bare_fn_type_slot_is_a_parse_error() {
    let src = include_str!("../../../examples/bare_slot_reject.ail");
    assert!(ailang_surface::parse(src).is_err(), "bare slot must not parse");
}

A CLI-boundary variant is also acceptable (assert ail check bare_slot_reject.ail exits non-zero with a parse-error stderr) if the implementer prefers consistency with the other reject pins; the load-bearing behaviour is "bare slot → error".

Also extend the round-trip test suite with a case proving a previously round-tripping bare-slot input now fails to parse (spec Testing §"Round-trip invariant").

• Step 13: Update both contracts

design/contracts/0008-memory-model.md:

Replace :57-59:

`Own` and `Borrow` are the two modes; every fn-type slot carries one
explicitly. Ownership has no default — there is no bare/unannotated
mode (spec 0062 deleted the legacy `Implicit` state).

Replace :62-65:

JSON canonical form: `param_modes` and `ret_mode` are always present
(one mode per slot). The pre-0062 elision (skipping all-`Implicit`
vectors for hash stability) is gone with the variant; the
corpus-wide hash reset that accompanied the deletion is a one-time
event recorded in `git log`.

Replace the :249-251 bullet (Iter B):

  param itself. `Borrow` parameters are skipped: `Borrow` retains the
  caller's ownership by contract. (There is no `Implicit` parameter
  any longer — every param is `Own` or `Borrow`.)

Replace the :260 clause (Iter A):

  the dec — only `Own`-mode scrutinees enable it; a `Borrow` scrutinee
  would let the arm dec memory the caller still references.

Replace the :297 clause (ret_mode):

  holds a view, not an own ref). Every `Term::App` callee now carries
  an explicit `Own`/`Borrow` `ret_mode`; an `Own`-returning call is
  trackable for scope-close drop, a `Borrow`-returning call is not
  (and is in any case rejected at the signature — borrow-returns are
  out of scope, spec 0062).

design/contracts/0002-data-model.md:

Replace the comment :272-273:

// `paramModes` and `retMode` are always present (one mode per slot).
// Full mode contract lives in contracts/0008-memory-model.md.

Replace the ParamMode block :297-302:

"own"        — (own T) — caller transfers ownership; callee consumes.
"borrow"     — (borrow T) — caller retains ownership; callee may not consume.

and the trailing prose (:302-…):

Every fn-type slot carries `own` or `borrow`; ownership has no default
(spec 0062 deleted the legacy `implicit` state). The full mode contract
(codegen consequences, the over-strict-mode lint, the `Suppress`
mechanism) lives in [memory model](0008-memory-model.md); the four
language-design preconditions that make RC sound live in
[language constraints](0015-language-constraints.md).

Phase D — remove throwaway, final gate

• Step 14: Remove the throwaway migration tool

Delete the MigrateModes arm + handler from crates/ail/src/main.rs, delete crates/ail/tests/migrate_modes.rs, and delete for_each_fn_type_mut from ast.rs (it has no other caller). (It references ParamMode::Implicit and would not compile anyway.)

• Step 15: Final workspace gate

Run: cargo build --workspace && cargo test --workspace Expected: 0 errors, all tests green (acceptance criterion 6).

• Step 16: Regression scripts + grep-clean gate

Run:

python3 bench/check.py
python3 bench/compile_check.py
python3 bench/cross_lang.py
git grep -nE 'ParamMode::Implicit|fn_implicit|is_implicit|all_implicit|mode_eq|mode_slices_eq' crates/
git grep -nE 'ParamModeImplicit' crates/

Expected: 0 regressions on all three scripts; both greps empty (acceptance criteria 1).

---

Spec fixture parse-gate (planner self-review item 9 attestation)

Every surface-language fixture inlined above was run through ail check against current HEAD (2026-06-01, target/debug/ail):

ownership_total.ail                  : exit 0   ok (36 symbols)
borrow_return_reject.ail             : exit 0   (legal today; check error post-cutover)
borrow_value_reject.ail              : exit 0   (legal today; sig error post-cutover)
bare_slot_reject.ail                 : exit 0   (legal today; parse error post-cutover)
own_return_provenance_reject.ail     : exit 1   [consume-while-borrowed] passthrough: `b` …
own_return_provenance_let.ail        : exit 1   [consume-while-borrowed] passthrough: `b` …
own_return_provenance_ctor.ail       : exit 1   [consume-while-borrowed] escape: `b` …  (regime A)

All seven match the spec's claimed exit codes. The migration-tool unit test fixture (Task 3 Step 1) is a Rust string literal, not a corpus fixture, and is exercised by cargo test -p ail --test migrate_modes.

Commit shape (orchestrator note, not an implement step)

Task 1 (borrow-return reject) and Task 3 (throwaway migration tool) each leave a green, independent tree and may be committed separately before the cutover (feat(check): borrow-return reject, chore: throwaway mode-migration tool). The borrow-over-value reject is NOT a standalone pre-cutover task — it is folded into Task 4 (Steps B1–B2) because it is entangled with the mono pass (see the Task 2 finding note). Task 4 is the single irreversible cutover commit (feat: delete ParamMode::Implicit — binary ownership modes (#55)) carrying the one-time hash reset and the borrow-over-value reject + mono-coercion. main only ever advances on a green tree; nothing half-migrated is committed.