feat(lang): eliminate the Implicit ownership default — totality + the drop-soundness it demasks (#55)

Deletes `ParamMode::Implicit`. `ParamMode` is now `{Own, Borrow}`:
every fn-type slot on every signature carries an explicit `own` or
`borrow`, no defaulted position survives anywhere (model 0008 §2,
spec 0062). The parser rejects a bare fn-type slot; `borrow-return`
and `borrow-over-value` reject at the signature; the corpus is
migrated to minimal-ownership modes (consumed ⇒ own, read-only-heap
⇒ borrow, value ⇒ trivial-own). The documented `Implicit`-ret-mode
leak is fixed: an owned heap return now drops exactly once (live=0,
acceptance criterion 5).

This was the easy half. Removing the default ACTIVATED a family of
drop paths that `Implicit` had silently skipped — the pre-cutover
language was leaking (and in places mis-dropping) here rather than
crashing, because an Implicit scrutinee turned the drop off. Making
the modes explicit (Own) turned those paths on and exposed two
latent-bug clusters, all fixed RED-first as part of this cutover:

Drop-soundness family (four legs):
  A. lit-sub-pattern double-free — the desugar re-matched the same
     owned scrutinee in the lit fall-through; fixed by grouping
     consecutive same-ctor arms into one match (bind fields once),
     in ailang-core desugar.
  B. Cons-husk leak on non-tail arm bodies — the lit-sub-pattern
     desugar rebound the owned scrutinee via `Let $mp = xs`, which
     bumped consume_count and suppressed the existing fn-return
     partial_drop. Fixed by not rebinding a bare-Var scrutinee
     (one husk-freeing mechanism, not two).
  C. polymorphic `drop_<T>` rc_dec'd monomorphised value fields —
     the per-ADT drop fn was emitted once from the polymorphic
     TypeDef, defaulting type-var fields to ptr and rc_dec'ing
     inline Ints (segfault). Fixed with per-monomorph drop
     functions (new ailang-codegen::dropmono): the drop set is
     collected from the lowered MIR, value-type fields are skipped,
     heap fields still freed once; monomorphic-concrete ADTs keep
     their byte-identical un-suffixed drop symbol.
  D. static Str literal passed to an `(own Str)` param — the
     literal lowers to a header-less rodata constant; the callee's
     now-active rc_dec read its length field as a refcount and
     freed a static address (segfault). Fixed with the missing
     fourth StrRep::Static→Heap promotion in lower_to_mir's App arm,
     gated on Own mode (borrow args stay static, no regression).

over-strict-mode lint over-fired: it suggested `(borrow V)` for
value-typed params (which `borrow-over-value` rejects — own is the
only legal mode there) and fired on `(intrinsic)` bodies (whose
consumption the linearity walk cannot observe). Tightened to skip
both; contract 0008 updated to the narrowed firing scope.

Irreversible step — canonical-form hash reset (model 0008 §6,
acceptance criterion 6). Every signature now carries explicit modes,
so the hashable canonical JSON changed for every module. RATIFY:
the corpus-wide hash-pin reset (hash_pin, prelude_module_hash_pin,
mono_hash_stability, eq_ord_e2e, embed_export_hash_stable, the
ct4/iter*/loop_recur schema-extension pins) and the list ir_snapshot
golden were regenerated once, deliberately, as the intended one-time
consequence of removing the mode elision from the canonical form —
not a regression. Each regenerated hash verified deterministic across
two runs.

Also fixes a pre-existing latent failure surfaced by the verification
gate, unrelated to this cutover: the `every_contract_names_a_resolvable_
ratifying_test` resolver (design_index_pin) could not resolve the
" + " dual-link ratifying-test form (`uniqueness.rs + linearity.rs`)
that the #57 audit-close (dfdc65f) introduced — it shipped red on that
commit. Resolver taught the dual-link form, mirroring its sibling.

Verification: cargo test --workspace = 731 passed, 0 failed (twice,
stable); e2e 102 passed, no binary exits non-zero (corpus crash-free);
grep-clean for Implicit/fn_implicit/mode_eq across crates; every drop
fix confirmed via emitted IR + AILANG_RC_STATS balance on the head==K,
head!=K, and Nil paths. Three BLOCKEDs en route (the unsound first
husk-dec attempt, the over-strict derivation premise, the leg-B fix
direction) were each treated as a real design/spec gap and rediagnosed,
not patched over.

Supersedes #54 (return-position-only leak patch). Precondition #57
(linearity hardening) was already met. Spec docs/specs/0062, plan
docs/plans/0121.

closes #55

bench/orchestrator-stats/2026-06-01-iter-0121-implicit-cutover.json

@@ -0,0 +1,17 @@
+{
+  "iter_id": "0121-implicit-cutover",
+  "date": "2026-06-01",
+  "mode": "standard",
+  "outcome": "PARTIAL",
+  "tasks_total": 1,
+  "tasks_completed": 0,
+  "reloops_per_task": { "4": 0 },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": "worker-blocked",
+  "corpus_files_mode_flipped_this_session": 6,
+  "corpus_files_migrated_total": 280,
+  "test_failures_remaining": 82,
+  "test_failures_at_session_start": 96,
+  "notes": "Continuation. Phase A Step 3 FINISHED: corpus linearity-clean (6 files own->borrow for read-only-heap/HOF params: std_list filter+fold predicate, bench_hof_pipeline, bench_latency_implicit loop/one_op/pin_root, rc_pin_recurse_implicit pin, rc_let_alias pin_aliased, floats_2_average sum_acc/count_acc; std_*_demo import std_list so its fix propagates). Must-fail fixtures (real_consume, c4_double_consume, 3 own_return_provenance) correctly stay RED (criterion 4). Fixed a real codegen index-panic (codegen lib.rs:1341/1494 + surface print.rs:406: param_modes[i] -> .get(i).unwrap_or(Own)) for synthesised fn-defs with empty param_modes (lambda thunks / local-rec lifts) — unblocked local_rec/nested_let_rec/poly_rec demos. Rewrote 2 obsolete linearity in-source tests to binary-model semantics. REMAINING BLOCKER: a real codegen double-free (segfault, exit 139) from the lit-sub-pattern desugar (core/desugar.rs:1221) x arm-close Iter-A drop (codegen/match_lower.rs:788): an (own ADT) param matched with a (Cons (pat-lit K) _) arm double-drops the tail because the lit `else`/fall_k re-matches the same scrutinee and each re-match arm-close drop fires on the same children. Latent pre-cutover (Implicit scrutinees skipped the drop, leaking); the cutover's Own scrutinees activate it. Gates ~7 list demos + cascading mono/rewrite tests. Needs RED-first codegen debugging (debug-skill class), NOT mechanical fixture work. Hash pins deliberately NOT reset (ordering: pins last, only after codegen correct, so the irreversible reset is not baked over a buggy state)."
+}

crates/ail/src/main.rs

@@ -76,10 +76,6 @@ enum Cmd {
     /// `render | parse` reproduces the input's canonical bytes
     /// (gated by `crates/ailang-surface/tests/round_trip.rs`).
     Render { path: PathBuf },
-    /// 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: PathBuf },
     /// Prints a single definition as JSON or pretty text.
     Describe {
         path: PathBuf,
@@ -444,22 +440,6 @@ fn main() -> Result<()> {
             let m = ailang_surface::load_module(&path)?;
             print!("{}", ailang_surface::print(&m));
         }
-        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))?;
-        }
         Cmd::Prose { path } => {
             // load via `load_module` (single-module mode,
             // matching how `render` / `parse` work). Workspace-wide

crates/ail/tests/cli_diag_human_workspace_load_error.rs

@@ -39,7 +39,7 @@ fn tempdir_with_missing_import() -> PathBuf {
     let mut f = std::fs::File::create(&entry).expect("create entry .ail");
     writeln!(
         f,
-        "(module test_missing_import\n  (import this_module_does_not_exist)\n  (fn main\n    (type (fn-type (params) (ret (con Unit)) (effects IO)))\n    (params)\n    (body (do io/print_str \"hello\"))))"
+        "(module test_missing_import\n  (import this_module_does_not_exist)\n  (fn main\n    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))\n    (params)\n    (body (do io/print_str \"hello\"))))"
     ).expect("write fixture");
     entry
 }

crates/ail/tests/drop_value_field_no_segfault_pin.rs

@@ -0,0 +1,122 @@
+//! RED-pin for leg (C) of the drop-soundness bug family the
+//! Implicit-cutover (#55) surfaced: a polymorphic ctor's per-type
+//! drop fn rc_dec's a type-parameter field even when the field is
+//! monomorphised at a value type (Int/Bool/Float/Unit).
+//!
+//! Property protected: under `--alloc=rc`, dropping a value of a
+//! polymorphic ADT whose ctor field is monomorphised at a value type
+//! must NOT emit `ailang_rc_dec` on that field. The field is stored
+//! inline as a raw scalar (an i64 `7`, not a heap pointer), so an
+//! `rc_dec` dereferences the scalar-as-pointer and crashes. The
+//! binary must run to completion, print the inner value, and the
+//! runtime RC stats line must report `live == 0` (the single ADT
+//! slab is freed exactly once, with no spurious dec of the inline
+//! value field).
+//!
+//! Root cause: `crates/ailang-codegen/src/drop.rs`
+//! `emit_drop_fn_for_type` (mirrored in `emit_iterative_drop_fn_for_type`
+//! and `emit_partial_drop_fn_for_type`) emits the per-type drop fn ONCE
+//! from the polymorphic `Def::Type` declaration — never per-monomorph.
+//! For each ctor field it computes `llvm_type(fty)` where `fty` is the
+//! declared field type. For a type-parameter field that type is a
+//! `Type::Var`, which `llvm_type` rejects (synth.rs returns `Err`); the
+//! `.unwrap_or_else(|_| "ptr".into())` at the field loop then silently
+//! treats the var-typed field as a boxed pointer and emits `rc_dec`.
+//! At the `Box Int` monomorph the field is an inline `i64`, so the
+//! emitted `rc_dec` dereferences the integer value -> SIGSEGV.
+//!
+//! As of HEAD (the in-flight Implicit cutover) this test fails: the
+//! binary exits 139 (SIGSEGV) before printing anything. Pre-cutover
+//! the bug was latent — Implicit scrutinees skipped the drop path
+//! entirely, so the mistyped drop never ran (it leaked instead of
+//! crashing).
+//!
+//! A single-field `Box a` at `Int` is the minimal trigger. The fix
+//! must still dec genuinely-heap fields (e.g. a `Box Str` field must
+//! free its slab exactly once) and must hold for the partial-drop and
+//! nested-monomorph variants — see the debugger handoff for the fix
+//! locus and soundness reasoning.
+
+use std::path::Path;
+use std::process::Command;
+
+fn ail_bin() -> &'static str {
+    env!("CARGO_BIN_EXE_ail")
+}
+
+#[test]
+fn alloc_rc_value_type_field_is_not_rc_dec_dropped() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
+    let src = workspace
+        .join("examples")
+        .join("drop_value_field_no_segfault_pin.ail");
+    let tmp = std::env::temp_dir().join(format!(
+        "ailang_drop_value_field_no_segfault_pin_{}",
+        std::process::id()
+    ));
+    std::fs::create_dir_all(&tmp).unwrap();
+    let out = tmp.join("bin");
+    let status = Command::new(ail_bin())
+        .args(["build", src.to_str().unwrap(), "--alloc=rc", "-o"])
+        .arg(&out)
+        .status()
+        .expect("ail build failed to run");
+    assert!(
+        status.success(),
+        "ail build --alloc=rc failed for drop_value_field_no_segfault_pin.ail"
+    );
+    let output = Command::new(&out)
+        .env("AILANG_RC_STATS", "1")
+        .output()
+        .expect("execute binary");
+    assert!(
+        output.status.success(),
+        "binary exited non-zero (status {:?}): the polymorphic drop fn \
+         drop_<m>_Box rc_dec's the type-parameter field, which at the \
+         Box Int monomorph is the inline i64 `7` (not a heap pointer), \
+         so rc_dec(7) dereferences the scalar-as-pointer and SIGSEGVs. \
+         Fix in crates/ailang-codegen/src/drop.rs: do not dec a field \
+         whose monomorphised type is a value type.",
+        output.status
+    );
+    let stdout = String::from_utf8(output.stdout).expect("stdout utf8");
+    assert_eq!(
+        stdout.trim_end(),
+        "7",
+        "unboxing MkBox 7 at Int must print 7; got {stdout:?}"
+    );
+    let stderr = String::from_utf8(output.stderr).expect("stderr utf8");
+    let stats_line = stderr
+        .lines()
+        .find(|l| l.starts_with("ailang_rc_stats:"))
+        .unwrap_or_else(|| {
+            panic!("missing ailang_rc_stats line in stderr; stderr was:\n{stderr}")
+        });
+    let mut allocs: Option<u64> = None;
+    let mut frees: Option<u64> = None;
+    let mut live: Option<i64> = None;
+    for tok in stats_line.split_whitespace() {
+        if let Some(v) = tok.strip_prefix("allocs=") {
+            allocs = v.parse().ok();
+        } else if let Some(v) = tok.strip_prefix("frees=") {
+            frees = v.parse().ok();
+        } else if let Some(v) = tok.strip_prefix("live=") {
+            live = v.parse().ok();
+        }
+    }
+    let allocs = allocs.expect("missing allocs= field");
+    let frees = frees.expect("missing frees= field");
+    let live = live.expect("missing live= field");
+    assert_eq!(
+        live, 0,
+        "RC imbalance after dropping a value-type-field ADT \
+         (allocs={allocs} frees={frees} live={live}); the Box slab \
+         must be freed exactly once and the inline Int field must \
+         never be dec'd."
+    );
+    assert_eq!(
+        allocs, frees,
+        "alloc/free mismatch (allocs={allocs} frees={frees} live={live})"
+    );
+}

crates/ail/tests/e2e.rs

@@ -82,6 +82,80 @@ fn sum_1_to_10_is_55() {
     assert_eq!(stdout.trim(), "55");
 }
 
+/// Property: a static `Str` literal passed by value into an `(own Str)`
+/// parameter that the callee drops must be RC-sound — dropped exactly
+/// once, no double-free, no leak.
+///
+/// RED for the #55-cutover drop-soundness crash. The literal lowers to
+/// `StrRep::Static` (a header-less rodata constant), but the cutover
+/// activates the Own-param drop path, which emits `ailang_rc_dec` on
+/// the unused param. `rc_dec` reads `payload - 8` as a refcount and
+/// `free()`s a static address -> SIGSEGV. `lower_to_mir`'s `Term::App`
+/// arm must flip such an argument to `StrRep::Heap` (str_clone into an
+/// owned slab), the same promotion mir.4 applies to loop-carried Str
+/// literals. Distinct root from legs A/B (the lit-pattern desugar); the
+/// match in eq_demo merely happens to drop its owned Str scrutinee too.
+///
+/// The assertion is robust against the stats-path masking leg A showed:
+/// it runs the binary on the NON-stats path (catching the SIGSEGV via
+/// the exit status) AND on the stats path asserting `live=0` /
+/// `frees==allocs`.
+#[test]
+fn own_str_literal_arg_is_dropped_exactly_once() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
+    let src = workspace.join("examples").join("own_str_arg_drop.ail");
+    let tmp = std::env::temp_dir().join(format!(
+        "ailang_e2e_own_str_arg_drop_{}",
+        std::process::id()
+    ));
+    std::fs::create_dir_all(&tmp).unwrap();
+    let out = tmp.join("bin");
+
+    let status = Command::new(ail_bin())
+        .args(["build", src.to_str().unwrap(), "-o"])
+        .arg(&out)
+        .status()
+        .expect("ail build failed to run");
+    assert!(status.success(), "ail build failed for own_str_arg_drop.ail");
+
+    // NON-stats path: this is the crashing path (SIGSEGV / double-free).
+    let plain = Command::new(&out).output().expect("execute binary");
+    assert!(
+        plain.status.success(),
+        "binary {} exited non-zero (expected success; got {:?}) — \
+         the owned Str literal was dropped on a header-less static",
+        out.display(),
+        plain.status.code()
+    );
+    assert_eq!(
+        String::from_utf8(plain.stdout).expect("stdout utf8").trim(),
+        "0"
+    );
+
+    // Stats path: RC balance must close — no leaked or double-freed Str.
+    let stats = Command::new(&out)
+        .env("AILANG_RC_STATS", "1")
+        .output()
+        .expect("execute binary with RC stats");
+    assert!(
+        stats.status.success(),
+        "binary {} (RC stats) exited non-zero (expected success; got {:?})",
+        out.display(),
+        stats.status.code()
+    );
+    let stderr = String::from_utf8(stats.stderr).expect("stderr utf8");
+    let line = stderr
+        .lines()
+        .find(|l| l.starts_with("ailang_rc_stats:"))
+        .unwrap_or_else(|| panic!("no ailang_rc_stats line in stderr: {stderr:?}"));
+    // Format: `ailang_rc_stats: allocs=N frees=M live=K`
+    assert!(
+        line.contains("live=0"),
+        "RC balance not closed: {line:?} (live != 0 means leak or double-free)"
+    );
+}
+
 #[test]
 fn loop_recur_sum_to_runs_to_value() {
     let stdout = build_and_run("loop_sum_to_run.ail");
@@ -1294,7 +1368,7 @@ fn intrinsic_in_user_module_is_rejected() {
     let src = tmp.join("intr_user.ail");
     std::fs::write(
         &src,
-        "(module intr_user (fn f (type (fn-type (params (con Int)) (ret (con Int)))) (params n) (intrinsic)))",
+        "(module intr_user (fn f (type (fn-type (params (own (con Int))) (ret (own (con Int))))) (params n) (intrinsic)))",
     )
     .unwrap();
 
@@ -1344,6 +1418,88 @@ fn lit_pat_demo() {
     assert_eq!(lines, vec!["100", "200", "999", "-1", "0", "7"]);
 }
 
+/// RED (refs #55, Implicit-cutover double-drop). Property protected:
+/// a ctor arm with a literal sub-pattern in a non-tail field —
+/// `(Cons (pat-lit K) _)` — drops the matched value's owned children
+/// EXACTLY ONCE, on both the head==K and head!=K paths.
+///
+/// The 16c lit-sub-pattern desugar lowers the arm into an outer
+/// Cons-match (binding the fields) wrapping `if (== head K) body
+/// else fall_k`; `fall_k` re-matches the same owned scrutinee, re-
+/// binding its children. Post-#55 the param mode is `Own`, so the
+/// match_lower.rs arm-close Iter-A drop (gated on `scrutinee_is_owned`)
+/// fires on the tail child in BOTH the re-match arm AND the enclosing
+/// lit-arm's join — `arg_xs+16` is dropped twice → double-free →
+/// SIGSEGV on the head!=K path.
+///
+/// Two assertions, so the symptom is pinned independently of the
+/// stats-drop masking divergence:
+///   1. `build_and_run` (no AILANG_RC_STATS): asserts the binary exits
+///      0 AND prints `0` then `7` — surfaces the segfault directly.
+///   2. rc-stats: `live == 0` and `frees == allocs` — pins single-drop
+///      (a double-free would over-count frees / corrupt the heap)
+///      rather than mere exit-0.
+#[test]
+fn lit_pat_ctor_tail_drop_single_drop() {
+    let stdout = build_and_run("lit_pat_ctor_tail_drop.ail");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["0", "7"]);
+
+    let (stats_stdout, allocs, frees, live) =
+        build_and_run_with_rc_stats("lit_pat_ctor_tail_drop.ail");
+    assert_eq!(
+        stats_stdout.lines().collect::<Vec<_>>(),
+        vec!["0", "7"],
+        "stdout under rc-stats must match the non-stats run"
+    );
+    assert_eq!(live, 0, "owned IntList children must all be freed (no leak)");
+    assert_eq!(
+        frees, allocs,
+        "every alloc freed exactly once — a double-free over-counts frees"
+    );
+}
+
+/// RED (refs #55, Implicit-cutover husk leak — leg B, Nil sub-case).
+/// Property protected: an owned scrutinee threaded through the
+/// lit-sub-pattern chain desugar has its OUTER cell freed exactly once
+/// on the Nil return path — the path that matches the Nil arm and
+/// touches neither inner Cons re-match.
+///
+/// The 16c desugar takes `first_or_default` off the `is_flat`
+/// fast-path (it has a lit sub-pattern arm), let-binds the owned
+/// scrutinee into a fresh `$mp` var, and chains single-level matches.
+/// Post-#55 the `Let $mp = xs` consumes `xs` (consume_count := 1),
+/// which trips the codegen fn-return gate (lib.rs ~1522, `if
+/// consume_count != 0 { continue }`) and suppresses the husk free a
+/// single-match owned fn would emit as `partial_drop_<T>(arg_xs, _)`.
+/// The husk obligation also moves to the internal `$mp` binder the
+/// gate never inspects. The Nil cell leaks -> live=1.
+///
+/// Distinct from `lit_pat_ctor_tail_drop_single_drop`, which only
+/// drives the Cons path: a fix that frees the husk on the Cons path
+/// but forgets the Nil path passes that test while still leaking here.
+#[test]
+fn lit_pat_nil_scrutinee_single_drop() {
+    let stdout = build_and_run("lit_pat_nil_scrutinee_drop.ail");
+    assert_eq!(stdout.lines().collect::<Vec<_>>(), vec!["-1"]);
+
+    let (stats_stdout, allocs, frees, live) =
+        build_and_run_with_rc_stats("lit_pat_nil_scrutinee_drop.ail");
+    assert_eq!(
+        stats_stdout.lines().collect::<Vec<_>>(),
+        vec!["-1"],
+        "stdout under rc-stats must match the non-stats run"
+    );
+    assert_eq!(
+        live, 0,
+        "the Nil scrutinee's outer cell must be freed (no husk leak)"
+    );
+    assert_eq!(
+        frees, allocs,
+        "every alloc freed exactly once — a double-free over-counts frees"
+    );
+}
+
 /// `__unreachable__` as an explicit user-callable
 /// primitive. Property protected: a polymorphic `forall a. a` value
 /// reference (a) typechecks against any expected type at the use
@@ -2395,43 +2551,41 @@ fn alloc_rc_let_binder_for_owned_returning_app_drops_at_scope_close() {
     );
 }
 
-/// a let-binder whose value is the
-/// result of an `Implicit`-ret-mode (default, unannotated) call must
-/// NOT be trackable. Implicit is the back-compat lane that 18c.3
-/// documented as "params don't get any dec — leak rather than mis-
-/// dec"; the symmetric carve-out for ret-modes is "Implicit-returning
-/// calls do not flow ownership to the caller, the caller must NOT
-/// dec".
+/// a let-binder whose value is the result of an `(own T)`-ret-mode
+/// call IS trackable for scope-close drop. ParamMode is binary
+/// `{Own, Borrow}`: an unannotated return defaults to `Own`, the
+/// callee's `(own T)` return signs the static contract that the
+/// caller now owns the returned cell, and the let-scope close emits
+/// the caller dec so the cell frees exactly once.
 ///
-/// If `is_rc_heap_allocated` were mistakenly to fire on this shape,
-/// the let-scope close would emit an unjustified dec — refcount
-/// underflow at runtime (the cell's RC reaches zero before any other
-/// owner had a chance to dec). The fixture under `--alloc=rc` must:
+/// The fixture under `--alloc=rc` must:
 ///
 /// (1) Build cleanly (no consume-while-borrowed false positive,
 ///     parse error, or unimplemented).
 /// (2) Exit cleanly with stdout `7` — the unboxed Int from the cell.
-/// (3) Report `live = 1` — the one MkT cell leaks. The leak is the
-///     intentional Implicit-mode behaviour; if codegen ever started
-///     dec'ing this shape it would crash with refcount underflow
-///     before the leak number could even be observed.
+/// (3) Report `live = 0` — the one MkT cell frees. The own-return
+///     contract flows ownership to the caller, which dec's the
+///     binder at scope close. This is the typed-MIR leak fix spec
+///     0062 delivers (acceptance criterion 5): the legacy `Implicit`
+///     back-compat lane that left this shape leaked (`live = 1`) is
+///     gone, so the owned-ret binder is dropped exactly once.
 ///
-/// This test is the negative-side companion to
+/// This test is the positive companion to
 /// `alloc_rc_let_binder_for_owned_returning_app_drops_at_scope_close`:
-/// the asymmetry between (own)-ret-mode (live=0) and Implicit-ret-mode
-/// (live=1) is the documented contract.
+/// both `(own)`-ret-mode shapes free at scope close (`live = 0`).
 #[test]
-fn alloc_rc_let_binder_for_implicit_returning_app_does_not_drop() {
+fn alloc_rc_let_binder_for_owned_returning_app_drops_exactly_once() {
     let (stdout, allocs, frees, live) =
         build_and_run_with_rc_stats("rc_let_implicit_returning_app.ail");
     assert_eq!(stdout.trim(), "7", "alloc(7) -> unbox should print 7");
     assert_eq!(
-        live, 1,
-        "Implicit-ret-mode App must leak (not crash with refcount \
-         underflow); allocs={allocs} frees={frees} live={live}. \
-         A live count of 0 means is_rc_heap_allocated mistakenly \
-         marked Implicit-ret-mode App as trackable; a non-zero exit \
-         means the unjustified dec triggered the underflow guard."
+        live, 0,
+        "owned-ret-mode App binder must drop exactly once at scope \
+         close (post-cutover: no Implicit leak lane); allocs={allocs} \
+         frees={frees} live={live}. A live count of 1 would mean \
+         is_rc_heap_allocated failed to mark the owned-ret App as \
+         trackable; a non-zero exit means an unjustified dec triggered \
+         the underflow guard."
     );
 }
 

crates/ail/tests/eq_ord_e2e.rs

@@ -136,7 +136,7 @@ fn eq_ord_user_adt_eq_intbox_hash_stable() {
     // sweep — the call site symbol name shifts, body hash follows.
     let h = def_hash(&Def::Fn(eq_intbox.clone()));
     assert_eq!(
-        h, "ceb466964df0e8d1",
+        h, "e639d41fc49b1524",
         "eq__IntBox body hash drifted — see mono_hash_stability.rs for the resolution pattern; captured: {h}"
     );
 }

crates/ail/tests/migrate_canonical_types.rs

@@ -50,7 +50,7 @@ fn migrate_canonical_types_rewrites_bare_xmod_term_ctor() {
         "imports": [{ "module": "other" }],
         "defs": [{
             "kind": "fn", "name": "f",
-            "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] },
+            "type": { "k": "fn", "params": [], "param_modes": [], "ret": { "k": "con", "name": "Unit" }, "ret_mode": "own", "effects": [] },
             "params": [],
             "body": { "t": "ctor", "type": "Foo", "ctor": "MkFoo", "args": [] }
         }],
@@ -111,7 +111,7 @@ fn migrate_canonical_types_rewrites_bare_xmod_type_con() {
         "imports": [{ "module": "other" }],
         "defs": [{
             "kind": "fn", "name": "f",
-            "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Foo" }, "effects": [] },
+            "type": { "k": "fn", "params": [], "param_modes": [], "ret": { "k": "con", "name": "Foo" }, "ret_mode": "own", "effects": [] },
             "params": [],
             "body": { "t": "lit", "lit": { "kind": "unit" } }
         }],

crates/ail/tests/migrate_modes.rs

@@ -1,27 +0,0 @@
-//! 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}");
-}

crates/ail/tests/mode_signature_rejects.rs

@@ -25,3 +25,23 @@ fn check_rejects_with(fixture: &str, code: &str) {
 fn borrow_return_is_rejected() {
     check_rejects_with("borrow_return_reject.ail", "borrow-return-not-permitted");
 }
+
+/// `(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");
+}
+
+/// 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");
+    }
+}

crates/ail/tests/mono_hash_stability.rs

@@ -60,12 +60,12 @@ fn primitive_eq_ord_mono_symbol_hashes_stay_bit_identical() {
     // by name; the body is signature-only. The four show__* pins
     // below do NOT move (Show instance bodies are real, unchanged).
     let pins: &[(&str, &str)] = &[
-        ("eq__Int",       "cc7b99b63d1e44ae"),
-        ("eq__Bool",      "fd0412f127986512"),
-        ("eq__Str",       "fa269285754a52da"),
-        ("compare__Int",  "0a02bd9effc9746c"),
-        ("compare__Bool", "d0dc108dacf4e543"),
-        ("compare__Str",  "d1419595dc52a456"),
+        ("eq__Int",       "85be5c2de568b58d"),
+        ("eq__Bool",      "851b24fb1b513bf9"),
+        ("eq__Str",       "ead456ddde7c0cbd"),
+        ("compare__Int",  "f99b792409ee8417"),
+        ("compare__Bool", "bdf90cb462351564"),
+        ("compare__Str",  "752b08fdd12c6a67"),
     ];
 
     for (sym, pin) in pins {

crates/ail/tests/print_no_leak_pin.rs

@@ -12,29 +12,14 @@
 //! `ailang_rc_dec(s)`. The runtime stats line at exit must report
 //! `live == 0` (equivalently `allocs == frees`).
 //!
-//! As of commit 301cbc3 this test fails: stderr reports
-//! `ailang_rc_stats: allocs=1 frees=0 live=1`. The IR for the post-
-//! mono `ail_prelude_print__Int` body contains a `call ptr
-//! @ail_prelude_show__Int(...)` followed by `getelementptr +8` +
-//! `@fputs` + `ret i8 0` — there is no `ailang_rc_dec` on the
-//! show-result before return. Root cause sits at codegen's
-//! `is_rc_heap_allocated` App-arm: it reads the callee's
-//! `Type::Fn.ret_mode` via `synth_callee_ret_mode` and requires
-//! `Own`. The mono'ed `show__Int` inherits its `Type::Fn` from the
-//! `Show` class method declaration in `examples/prelude.ail.json`,
-//! whose `methods[0].type` omits the `ret_mode` key — `serde` defaults
-//! the missing field to `ParamMode::Implicit`. So
-//! `synth_callee_ret_mode(show__Int) == Implicit`, the let-binder is
-//! not flagged trackable, and `drop_symbol_for_binder` is never
-//! called for it.
-//!
-//! Once the underlying issue is fixed (the canonical move is to
-//! recognise that any class-method whose declared `ret` is `Str` /
-//! any pointer-typed user type should round-trip as Own through
-//! mono, OR to install the Show class declaration with explicit
-//! `ret_mode: "own"`, OR to widen `is_rc_heap_allocated`'s App-arm
-//! to also consult the callee's ret type-via-Str-carve-out), this
-//! test must flip GREEN without weakening the assertion.
+//! Codegen's `is_rc_heap_allocated` App-arm reads the callee's
+//! `Type::Fn.ret_mode` via `synth_callee_ret_mode` and tracks the
+//! let-binder iff it is `Own`. The mono'ed `show__Int` inherits its
+//! `Type::Fn` from the `Show` class method declaration in
+//! `examples/prelude.ail.json`, whose `show` carries `ret_mode: own`
+//! (every fn-type slot is moded — spec 0062). So `show__Int` returns
+//! `Own`, the let-binder for the show-result is trackable, and
+//! `drop_symbol_for_binder` emits the scope-close dec — `live == 0`.
 
 use std::path::Path;
 use std::process::Command;
@@ -107,10 +92,9 @@ fn alloc_rc_print_int_does_not_leak_show_result_str() {
         live, 0,
         "`(app print 42)` under --alloc=rc leaks {live} heap-Str cell(s) \
          (allocs={allocs} frees={frees}); print's let-binder for the \
-         show-result must drop at let-scope-close. Show class method \
-         `show` in prelude.ail.json omits `ret_mode`, so mono-synthesised \
-         `show__Int` inherits ret_mode=Implicit and `is_rc_heap_allocated` \
-         declines to track the let-binder."
+         show-result must drop at let-scope-close. The Show class method \
+         `show` carries `ret_mode: own`, so mono-synthesised `show__Int` \
+         is `Own`-returning and `is_rc_heap_allocated` tracks the binder."
     );
     assert_eq!(
         allocs, frees,

crates/ail/tests/roundtrip_cli.rs

@@ -36,6 +36,23 @@ fn examples_dir() -> PathBuf {
     workspace_root().join("examples")
 }
 
+/// Fixtures that intentionally do NOT parse — the `#55` cutover
+/// reject corpus. These are negative fixtures whose whole point is
+/// that the parser rejects them, so `parse∘render∘parse` is not a
+/// meaningful property for them and the harness must skip them.
+///
+/// Scope is deliberately minimal: only fixtures that fail at the
+/// PARSE stage belong here. The other `*reject*.ail` cutover
+/// fixtures (`borrow_return_reject`, `borrow_value_reject`,
+/// `own_return_provenance_reject`, the `embed_export_*_rejected`
+/// set, …) parse cleanly and are rejected only later at CHECK time,
+/// so they round-trip fine and are NOT excluded.
+///
+/// - `bare_slot_reject.ail`: a bare fn-type slot with no mode. The
+///   binary-ParamMode parser rejects it ("fn-type slot requires a
+///   mode: write (own T) or (borrow T)").
+const NON_PARSEABLE_FIXTURES: &[&str] = &["bare_slot_reject.ail"];
+
 fn list_ail_fixtures() -> Vec<PathBuf> {
     let dir = examples_dir();
     let mut paths: Vec<PathBuf> = std::fs::read_dir(&dir)
@@ -45,7 +62,9 @@ fn list_ail_fixtures() -> Vec<PathBuf> {
         .filter(|p| {
             p.file_name()
                 .and_then(|n| n.to_str())
-                .map(|n| n.ends_with(".ail"))
+                .map(|n| {
+                    n.ends_with(".ail") && !NON_PARSEABLE_FIXTURES.contains(&n)
+                })
                 .unwrap_or(false)
         })
         .collect();

crates/ail/tests/snapshots/list.ll

@@ -53,6 +53,7 @@ mdefault.2:
   unreachable
 mjoin.2:
   %v9 = phi i64 [ 0, %marm.2.0 ], [ %v8, %marm.2.1 ]
+  call void @partial_drop_list_IntList(ptr %arg_xs, i64 2)
   ret i64 %v9
 }
 

crates/ail/tests/typeclass_22b3.rs

@@ -208,7 +208,7 @@ fn synthesise_mono_fn_uses_instance_body_lam() {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ailang_core::ast::ParamMode::Implicit,
+                ret_mode: ailang_core::ast::ParamMode::Own,
             },
             default: None,
         }],
@@ -277,7 +277,7 @@ fn synthesise_mono_fn_falls_back_to_class_default() {
                 ret: Box::new(Type::str_()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ailang_core::ast::ParamMode::Implicit,
+                ret_mode: ailang_core::ast::ParamMode::Own,
             },
             default: Some(Term::Lam {
                 params: vec!["_x".into()],

crates/ail/tests/user_adt_new_mono_pin.rs

@@ -54,12 +54,12 @@ const PROG: &str = r#"(module user_adt_new_mono
 
   (fn new
     (doc "Build a Counter initialised to the given value.")
-    (type (fn-type (params (con Int)) (ret (con Counter))))
+    (type (fn-type (params (own (con Int))) (ret (own (con Counter)))))
     (params n)
     (body (term-ctor Counter MkCounter n)))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (let c (new Counter 42)

crates/ailang-check/src/builtins.rs

@@ -65,7 +65,7 @@ pub fn install(env: &mut crate::Env) {
             ret: Box::new(Type::Var { name: "a".into() }),
             effects: vec![],
             param_modes: vec![],
-            ret_mode: ailang_core::ast::ParamMode::Implicit,
+            ret_mode: ailang_core::ast::ParamMode::Own,
         }),
     };
     // 2026-05-21 operator-routing-eq-ord: the `poly_a_a_to_bool`
@@ -78,7 +78,7 @@ pub fn install(env: &mut crate::Env) {
         ret: Box::new(Type::int()),
         effects: vec![],
         param_modes: vec![],
-        ret_mode: ailang_core::ast::ParamMode::Implicit,
+        ret_mode: ailang_core::ast::ParamMode::Own,
     };
     for op in ["+", "-", "*", "/"] {
         env.globals.insert(op.into(), poly_a_a_to_a());
@@ -98,7 +98,7 @@ pub fn install(env: &mut crate::Env) {
             ret: Box::new(Type::bool_()),
             effects: vec![],
             param_modes: vec![],
-            ret_mode: ailang_core::ast::ParamMode::Implicit,
+            ret_mode: ailang_core::ast::ParamMode::Own,
         },
     );
 
@@ -134,7 +134,7 @@ pub fn install(env: &mut crate::Env) {
                 ret: Box::new(Type::Var { name: "a".into() }),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ailang_core::ast::ParamMode::Implicit,
+                ret_mode: ailang_core::ast::ParamMode::Own,
             }),
         },
     );
@@ -145,7 +145,7 @@ pub fn install(env: &mut crate::Env) {
             ret: Box::new(Type::float()),
             effects: vec![],
             param_modes: vec![],
-            ret_mode: ailang_core::ast::ParamMode::Implicit,
+            ret_mode: ailang_core::ast::ParamMode::Own,
         },
     );
     env.globals.insert(
@@ -155,7 +155,7 @@ pub fn install(env: &mut crate::Env) {
             ret: Box::new(Type::int()),
             effects: vec![],
             param_modes: vec![],
-            ret_mode: ailang_core::ast::ParamMode::Implicit,
+            ret_mode: ailang_core::ast::ParamMode::Own,
         },
     );
     env.globals.insert(
@@ -218,7 +218,7 @@ pub fn install(env: &mut crate::Env) {
             ret: Box::new(Type::bool_()),
             effects: vec![],
             param_modes: vec![],
-            ret_mode: ailang_core::ast::ParamMode::Implicit,
+            ret_mode: ailang_core::ast::ParamMode::Own,
         },
     );
 

crates/ailang-check/src/lib.rs

@@ -782,6 +782,13 @@ pub enum CheckError {
     #[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),
 
+    /// 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 },
+
     /// an internal invariant in the typechecker / mono pass
     /// was violated — surfaced as an error so callers can propagate
     /// rather than abort, but in well-formed inputs (typecheck has
@@ -844,6 +851,7 @@ impl CheckError {
             CheckError::ParamNotInRestrictedSet { .. } => "param-not-in-restricted-set",
             CheckError::IntrinsicOutsideKernelTier { .. } => "intrinsic-outside-kernel-tier",
             CheckError::BorrowReturnNotPermitted(_) => "borrow-return-not-permitted",
+            CheckError::BorrowOverValueType { .. } => "borrow-over-value",
             CheckError::Internal(_) => "internal",
         }
     }
@@ -2109,7 +2117,7 @@ fn check_instance(
             .collect();
         let subst_ret_ty = substitute_rigids(ret_ty, &subst_map);
         let subst_body = substitute_rigids_in_term(body, &subst_map);
-        let fn_ty = Type::fn_implicit(
+        let fn_ty = Type::fn_owned(
             subst_param_tys,
             subst_ret_ty,
             effects.clone(),
@@ -2279,10 +2287,14 @@ fn check_fn(
         other => (vec![], other.clone()),
     };
 
-    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())
-        }
+    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(),
@@ -2321,6 +2333,23 @@ fn check_fn(
         return Err(CheckError::BorrowReturnNotPermitted(f.name.clone()));
     }
 
+    // spec 0062: borrow over an unboxed value type is meaningless.
+    // Fired on the signature, before body dataflow. The mono-coercion
+    // (subst.rs) 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(),
+                    });
+                }
+            }
+        }
+    }
+
     // An `(intrinsic)` body is signature-only: the signature is already
     // validated above; codegen supplies the implementation via the
     // intercept registry. The body is `Term::Intrinsic` directly (a
@@ -4168,7 +4197,7 @@ pub(crate) fn synth(
                 ret: Box::new((**ret_ty).clone()),
                 effects: lam_effects.clone(),
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             })
         }
         Term::LetRec { name, ty, params, body, in_term } => {
@@ -5485,7 +5514,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["a", "b"],
                 Term::App {
@@ -5515,7 +5544,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Lit {
@@ -5542,7 +5571,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec![], // !IO missing,
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Do {
@@ -5575,7 +5604,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Let {
@@ -5620,7 +5649,7 @@ mod tests {
                         ret: Box::new(Type::int()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     vec!["m"],
                     Term::Match {
@@ -5673,7 +5702,7 @@ mod tests {
                         ret: Box::new(Type::int()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     vec!["m"],
                     Term::Match {
@@ -5716,7 +5745,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::If {
@@ -5754,7 +5783,7 @@ mod tests {
                         ret: Box::new(Type::Var { name: "a".into() }),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     }),
                 },
                 vec!["x"],
@@ -5780,7 +5809,7 @@ mod tests {
                     ret: Box::new(Type::Var { name: "a".into() }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 }),
             },
             vec!["x"],
@@ -5794,7 +5823,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec![],
             Term::App {
@@ -5811,7 +5840,7 @@ mod tests {
                 ret: Box::new(Type::bool_()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec![],
             Term::App {
@@ -5845,7 +5874,7 @@ mod tests {
                     ret: Box::new(Type::Var { name: "a".into() }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 }),
             },
             vec!["x"],
@@ -5859,7 +5888,7 @@ mod tests {
                 ret: Box::new(Type::bool_()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec![],
             Term::App {
@@ -5897,14 +5926,14 @@ mod tests {
                             ret: Box::new(Type::Var { name: "b".into() }),
                             effects: vec![],
                             param_modes: vec![],
-                            ret_mode: ParamMode::Implicit,
+                            ret_mode: ParamMode::Own,
                         },
                         Type::Var { name: "a".into() },
                     ],
                     ret: Box::new(Type::Var { name: "b".into() }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 }),
             },
             vec!["f", "x"],
@@ -5922,7 +5951,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec!["n"],
             Term::App {
@@ -5941,7 +5970,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec![],
             Term::App {
@@ -5989,7 +6018,7 @@ mod tests {
                 }),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec![],
             Term::Ctor {
@@ -6036,7 +6065,7 @@ mod tests {
                     ret: Box::new(Type::Var { name: "a".into() }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 }),
             },
             params: vec!["b".into()],
@@ -6063,7 +6092,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec![],
             Term::App {
@@ -6083,7 +6112,7 @@ mod tests {
                 ret: Box::new(Type::bool_()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec![],
             Term::App {
@@ -6131,7 +6160,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             vec!["b"],
             Term::Lit { lit: Literal::Int { value: 0 } },
@@ -6165,7 +6194,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Seq {
@@ -6219,7 +6248,7 @@ mod tests {
                         ret: Box::new(Type::Con { name: "L".into(), args: vec![] }),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     vec!["xs"],
                     // Body: C(0, tail-app loop xs) — the recursion is
@@ -6295,7 +6324,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["b"],
                 Term::Lit { lit: Literal::Int { value: 0 } },
@@ -6325,7 +6354,7 @@ mod tests {
                     }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Ctor {
@@ -6362,7 +6391,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["b"],
                 Term::Match {
@@ -6449,7 +6478,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Match {
@@ -6541,7 +6570,7 @@ mod tests {
                                 }),
                                 effects: vec![],
                                 param_modes: vec![],
-                                ret_mode: ParamMode::Implicit,
+                                ret_mode: ParamMode::Own,
                             }),
                         },
                         default: None,
@@ -6590,7 +6619,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Match {
@@ -6681,7 +6710,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             }),
         };
         let out = qualify_local_types(&input, "p", &local_types);
@@ -6735,7 +6764,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec!["IO".into()],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     vec!["xs"],
                     Term::Match {
@@ -6807,7 +6836,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["x".into()],
             body: Box::new(Term::Lit { lit: Literal::Bool { value: true } }),
@@ -6831,7 +6860,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec!["x".into()],
                 body: Box::new(Term::Seq {
@@ -6867,7 +6896,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 body,
@@ -6903,7 +6932,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Let {
@@ -6916,7 +6945,7 @@ mod tests {
                             ret: Box::new(Type::int()),
                             effects: vec![],
                             param_modes: vec![],
-                            ret_mode: ParamMode::Implicit,
+                            ret_mode: ParamMode::Own,
                         },
                         params: vec!["x".into()],
                         body: Box::new(Term::App {
@@ -6960,7 +6989,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             "lifted ty should have capture appended; got {:?}",
             synth.ty
@@ -7031,7 +7060,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["z".into()],
             body: Box::new(Term::App {
@@ -7078,7 +7107,7 @@ mod tests {
                         ret: Box::new(Type::int()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     vec!["p"],
                     outer_body,
@@ -7110,7 +7139,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             "lifted ty should have the match-arm-capture type Int appended; got {:?}",
             synth.ty
@@ -7166,7 +7195,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["x"],
                 body,
@@ -7228,7 +7257,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["x"],
                 Term::Match {
@@ -7296,7 +7325,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["b"],
                 Term::Match {
@@ -7346,7 +7375,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["x"],
                 Term::Match {
@@ -7403,7 +7432,7 @@ mod tests {
                     }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Ctor {
@@ -7469,7 +7498,7 @@ mod tests {
                     }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Ctor {
@@ -7534,7 +7563,7 @@ mod tests {
                     }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::Ctor {
@@ -7578,7 +7607,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec!["n"],
                 Term::Var { name: "n".into() },
@@ -7596,7 +7625,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 vec![],
                 Term::App {
@@ -7846,7 +7875,7 @@ mod tests {
                         param_modes: vec![ParamMode::Borrow],
                         ret: Box::new(Type::Con { name: "Str".to_string(), args: vec![] }),
                         effects: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     default: None,
                 }],
@@ -7913,7 +7942,7 @@ mod tests {
                         param_modes: vec![ParamMode::Borrow],
                         ret: Box::new(Type::str_()),
                         effects: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     default: None,
                 }],
@@ -7925,7 +7954,7 @@ mod tests {
             param_modes: vec![ParamMode::Borrow],
             ret: Box::new(Type::str_()),
             effects: vec![],
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
         };
         let fnmod = Module {
             schema: SCHEMA.into(),
@@ -8032,7 +8061,7 @@ mod tests {
                         param_modes: vec![ParamMode::Borrow],
                         ret: Box::new(Type::Con { name: "Str".to_string(), args: vec![] }),
                         effects: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     default: None,
                 }],
@@ -8172,8 +8201,8 @@ mod tests {
                 {"kind": "fn", "name": "from_maybe",
                  "type": {"k": "forall", "vars": ["a"], "constraints": [], "body":
                      {"k": "fn", "params": [{"k": "var", "name": "a"},
-                                            {"k": "con", "name": "Maybe", "args": [{"k": "var", "name": "a"}]}],
-                      "ret": {"k": "var", "name": "a"}, "effects": []}},
+                                            {"k": "con", "name": "Maybe", "args": [{"k": "var", "name": "a"}]}], "param_modes": ["own", "borrow"],
+                      "ret": {"k": "var", "name": "a"}, "ret_mode": "own", "effects": []}},
                  "params": ["default", "m"],
                  "body": {"t": "var", "name": "default"}}
             ]
@@ -8191,8 +8220,8 @@ mod tests {
             "imports": [{"module": "std_maybe"}],
             "defs": [
                 {"kind": "fn", "name": "f",
-                 "type": {"k": "fn", "params": [{"k": "con", "name": "Int"}],
-                          "ret": {"k": "con", "name": "Int"}, "effects": []},
+                 "type": {"k": "fn", "params": [{"k": "con", "name": "Int"}], "param_modes": ["own"],
+                          "ret": {"k": "con", "name": "Int"}, "ret_mode": "own", "effects": []},
                  "params": ["x"],
                  "body": {"t": "app",
                           "fn": {"t": "var", "name": "Maybe.from_maybe"},
@@ -8240,8 +8269,8 @@ mod tests {
             "imports": [{"module": "std_maybe"}],
             "defs": [
                 {"kind": "fn", "name": "f",
-                 "type": {"k": "fn", "params": [],
-                          "ret": {"k": "con", "name": "Int"}, "effects": []},
+                 "type": {"k": "fn", "params": [], "param_modes": [],
+                          "ret": {"k": "con", "name": "Int"}, "ret_mode": "own", "effects": []},
                  "params": [],
                  "body": {"t": "var", "name": "Maybe.bogus"}}
             ]
@@ -8273,8 +8302,8 @@ mod tests {
             "imports": [],
             "defs": [
                 {"kind": "fn", "name": "f",
-                 "type": {"k": "fn", "params": [],
-                          "ret": {"k": "con", "name": "Int"}, "effects": []},
+                 "type": {"k": "fn", "params": [], "param_modes": [],
+                          "ret": {"k": "con", "name": "Int"}, "ret_mode": "own", "effects": []},
                  "params": [],
                  "body": {"t": "var", "name": "SomethingRandom.x"}}
             ]
@@ -8314,15 +8343,15 @@ mod tests {
                 ]},
                 {"kind": "fn", "name": "new",
                  "type": {"k": "fn",
-                          "params": [{"k": "con", "name": "Int"}],
-                          "ret": {"k": "con", "name": "Counter"},
+                          "params": [{"k": "con", "name": "Int"}], "param_modes": ["own"],
+                          "ret": {"k": "con", "name": "Counter"}, "ret_mode": "own",
                           "effects": []},
                  "params": ["n"],
                  "body": {"t": "ctor", "type": "Counter", "ctor": "MkCounter",
                           "args": [{"t": "var", "name": "n"}]}},
                 {"kind": "fn", "name": "main",
-                 "type": {"k": "fn", "params": [],
-                          "ret": {"k": "con", "name": "Counter"},
+                 "type": {"k": "fn", "params": [], "param_modes": [],
+                          "ret": {"k": "con", "name": "Counter"}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  "body": {"t": "new", "type": "Counter",
@@ -8369,8 +8398,8 @@ mod tests {
                 ]},
                 // No `new` def for T.
                 {"kind": "fn", "name": "main",
-                 "type": {"k": "fn", "params": [],
-                          "ret": {"k": "con", "name": "T"},
+                 "type": {"k": "fn", "params": [], "param_modes": [],
+                          "ret": {"k": "con", "name": "T"}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  "body": {"t": "new", "type": "T",
@@ -8423,17 +8452,17 @@ mod tests {
                 {"kind": "fn", "name": "new",
                  "type": {"k": "forall", "vars": ["a"], "constraints": [],
                           "body": {"k": "fn",
-                                   "params": [{"k": "var", "name": "a"}],
+                                   "params": [{"k": "var", "name": "a"}], "param_modes": ["own"],
                                    "ret": {"k": "con", "name": "T",
-                                           "args": [{"k": "var", "name": "a"}]},
+                                           "args": [{"k": "var", "name": "a"}]}, "ret_mode": "own",
                                    "effects": []}},
                  "params": ["x"],
                  "body": {"t": "ctor", "type": "T", "ctor": "MkT",
                           "args": [{"t": "var", "name": "x"}]}},
                 {"kind": "fn", "name": "main",
-                 "type": {"k": "fn", "params": [],
+                 "type": {"k": "fn", "params": [], "param_modes": [],
                           "ret": {"k": "con", "name": "T",
-                                  "args": [{"k": "con", "name": "Int"}]},
+                                  "args": [{"k": "con", "name": "Int"}]}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  // Wrong: only one NewArg::Value supplied for a sig
@@ -8478,9 +8507,9 @@ mod tests {
                 // Reference `(con StubT (con Str))` in a fn return
                 // type — well-formedness check walks the return type.
                 {"kind": "fn", "name": "bad",
-                 "type": {"k": "fn", "params": [],
+                 "type": {"k": "fn", "params": [], "param_modes": [],
                           "ret": {"k": "con", "name": "StubT",
-                                  "args": [{"k": "con", "name": "Str"}]},
+                                  "args": [{"k": "con", "name": "Str"}]}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  "body": {"t": "lit", "lit": {"kind": "unit"}}}
@@ -8518,9 +8547,9 @@ mod tests {
                  "ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
                  "param-in": {"a": ["Int", "Float"]}},
                 {"kind": "fn", "name": "bad",
-                 "type": {"k": "fn", "params": [],
+                 "type": {"k": "fn", "params": [], "param_modes": [],
                           "ret": {"k": "con", "name": "StubT",
-                                  "args": [{"k": "con", "name": "Str"}]},
+                                  "args": [{"k": "con", "name": "Str"}]}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  "body": {"t": "lit", "lit": {"kind": "unit"}}}
@@ -8563,9 +8592,9 @@ mod tests {
                  "ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
                  "param-in": {"a": ["Int", "Float"]}},
                 {"kind": "fn", "name": "bad",
-                 "type": {"k": "fn", "params": [],
+                 "type": {"k": "fn", "params": [], "param_modes": [],
                           "ret": {"k": "con", "name": "StubT",
-                                  "args": [{"k": "con", "name": "Str"}]},
+                                  "args": [{"k": "con", "name": "Str"}]}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  "body": {"t": "lit", "lit": {"kind": "unit"}}}
@@ -8610,9 +8639,9 @@ mod tests {
                  "ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
                  "param-in": {"a": ["Int", "Float"]}},
                 {"kind": "fn", "name": "good",
-                 "type": {"k": "fn", "params": [],
+                 "type": {"k": "fn", "params": [], "param_modes": [],
                           "ret": {"k": "con", "name": "StubT",
-                                  "args": [{"k": "con", "name": "Int"}]},
+                                  "args": [{"k": "con", "name": "Int"}]}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  "body": {"t": "lit", "lit": {"kind": "unit"}}}
@@ -8667,8 +8696,8 @@ mod tests {
                 // shape is irrelevant.
                 {"kind": "fn", "name": "value",
                  "type": {"k": "fn",
-                          "params": [{"k": "con", "name": "Counter"}],
-                          "ret": {"k": "con", "name": "Int"},
+                          "params": [{"k": "con", "name": "Counter"}], "param_modes": ["borrow"],
+                          "ret": {"k": "con", "name": "Int"}, "ret_mode": "own",
                           "effects": []},
                  "params": ["c"],
                  "body": {"t": "lit", "lit": {"kind": "int", "value": 0}}},
@@ -8677,8 +8706,8 @@ mod tests {
                 // Per spec § prep.1 "Canonical form decision" this
                 // is the canonical form and must check.
                 {"kind": "fn", "name": "main",
-                 "type": {"k": "fn", "params": [],
-                          "ret": {"k": "con", "name": "Int"},
+                 "type": {"k": "fn", "params": [], "param_modes": [],
+                          "ret": {"k": "con", "name": "Int"}, "ret_mode": "own",
                           "effects": []},
                  "params": [],
                  "body": {"t": "let", "name": "c",
@@ -8750,8 +8779,8 @@ mod tests {
                 {"kind": "fn", "name": "unwrap_int",
                  "type": {"k": "fn",
                           "params": [{"k": "con", "name": "StubT",
-                                      "args": [{"k": "con", "name": "Int"}]}],
-                          "ret": {"k": "con", "name": "Int"},
+                                      "args": [{"k": "con", "name": "Int"}]}], "param_modes": ["borrow"],
+                          "ret": {"k": "con", "name": "Int"}, "ret_mode": "own",
                           "effects": []},
                  "params": ["s"],
                  "body": {"t": "lit", "lit": {"kind": "int", "value": 0}}}

crates/ailang-check/src/lift.rs

@@ -561,7 +561,7 @@ impl<'a> Lifter<'a> {
                             ret: ret.clone(),
                             effects: effects.clone(),
                             param_modes: vec![],
-                            ret_mode: ParamMode::Implicit,
+                            ret_mode: ParamMode::Own,
                         }
                     }
                     Type::Forall { .. } => panic!(
@@ -933,7 +933,7 @@ fn substitute_rigids_local(t: &Type, mapping: &BTreeMap<String, Type>) -> Type {
             ret: Box::new(substitute_rigids_local(ret, mapping)),
             effects: effects.clone(),
             param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
         },
         Type::Forall { vars, constraints, body } => {
             let inner: BTreeMap<String, Type> = mapping

crates/ailang-check/src/linearity.rs

@@ -1,13 +1,11 @@
-//! Linearity check for fns whose every parameter mode is
-//! explicit (`Borrow` or `Own`).
+//! Linearity check for fns. Every parameter mode is explicit
+//! (`Borrow` or `Own`) — ownership has no default (spec 0062).
 //!
 //! ## Scope
 //!
 //! - **Active only** on `Def::Fn` whose `Type::Fn.param_modes` is
-//!   non-empty AND contains no [`ParamMode::Implicit`]. Any
-//!   `Implicit`-mode param skips the entire fn — that is the back-compat
-//!   lane that keeps every existing fixture green (only
-//!   `borrow_own_demo` ships an all-explicit signature today).
+//!   non-empty. A nullary fn has no binders to track, so the check
+//!   skips it.
 //! - **Pure diagnostic.** Emits [`Diagnostic`]s with codes
 //!   `use-after-consume` / `consume-while-borrowed`. No IR change, no
 //!   codegen change, no runtime change. The check runs after
@@ -34,8 +32,7 @@
 //!   application.
 //! - `Term::App.args[i]` — Borrow if the callee is a `Var` whose
 //!   resolved type is a `Type::Fn` with `param_modes[i] == Borrow`;
-//!   otherwise Consume (Own / Implicit / unknown all default to
-//!   Consume).
+//!   otherwise Consume (Own / unknown default to Consume).
 //! - `Term::Clone.value` — Borrow (clone reads + bumps RC, doesn't
 //!   move).
 //! - `Term::Match.scrutinee` — Borrow (matching is a read; for an
@@ -364,8 +361,8 @@ fn fn_modes_of(t: &Type) -> Option<Vec<ParamMode>> {
     }
 }
 
-/// Per-fn check. Skips fns whose signature has any `Implicit` param —
-/// see module-level scope rules.
+/// Per-fn check. Skips nullary fns (no binders to track) — see
+/// module-level scope rules.
 fn check_fn(
     f: &FnDef,
     globals: &HashMap<String, Type>,
@@ -380,17 +377,17 @@ fn check_fn(
         _ => return,
     };
 
-    // Activation gate: every param mode must be explicit (Borrow / Own).
-    // No params at all also disables the check — there are no binders
-    // to track in the param-list, so the check has nothing to enforce.
-    if param_modes.is_empty() || param_modes.iter().any(|m| matches!(m, ParamMode::Implicit)) {
+    // Activation gate: no params at all disables the check — there are
+    // no binders to track in the param-list, so the check has nothing
+    // to enforce. Every mode is now explicitly `Own`/`Borrow`
+    // (spec 0062), so there is no unmoded disjunct left.
+    if param_modes.is_empty() {
         return;
     }
 
     // Sanity: param-count has been verified by `check_fn` upstream, but
-    // double-defend in case the type vec is shorter than the binder list
-    // — the linearity walk treats over-long binder lists as `Implicit`
-    // and would silently mis-skip the check otherwise.
+    // double-defend in case the type vec is shorter than the binder
+    // list, which would silently mis-skip the check otherwise.
     if param_modes.len() != f.params.len() || param_tys.len() != f.params.len() {
         return;
     }
@@ -414,7 +411,7 @@ fn check_fn(
             consumed: false,
             borrow_count: match mode {
                 ParamMode::Borrow => 1,
-                ParamMode::Own | ParamMode::Implicit => 0,
+                ParamMode::Own => 0,
             },
             is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
             fn_param_modes: param_tys.get(i).and_then(|t| fn_modes_of(t)),
@@ -436,10 +433,26 @@ fn check_fn(
     // is fine as long as none of the arms moves a sub-binder out.
     // The uniqueness pass already populates `consume_count` for
     // pattern-binders, so the check is a deterministic walk.
+    //
+    // Two guards keep the lint coherent post-cutover:
+    //  - An `(intrinsic)`-bodied fn is skipped wholesale: the walk does
+    //    nothing for `Term::Intrinsic`, so `consume_count == 0` is a
+    //    guaranteed false positive. An intrinsic's param modes are
+    //    hand-authored contracts, not lint-derivable from a body.
+    //  - A value-typed param (`Int`/`Bool`/`Float`/`Unit`) is skipped:
+    //    `(borrow V)` is rejected by `borrow-over-value` (lib.rs), so
+    //    `(own V)` is the only legal mode and a relax-to-borrow
+    //    suggestion would be incoherent.
+    if matches!(f.body, Term::Intrinsic) {
+        return;
+    }
     for (i, mode) in param_modes.iter().enumerate() {
         if !matches!(mode, ParamMode::Own) {
             continue;
         }
+        if param_tys.get(i).map(type_is_value).unwrap_or(false) {
+            continue;
+        }
         let pname = &f.params[i];
         let consume_count = uniq
             .get(&(f.name.clone(), pname.clone()))
@@ -518,7 +531,7 @@ impl<'a> Checker<'a> {
                 for (i, arg) in args.iter().enumerate() {
                     let arg_pos = match arg_modes.get(i) {
                         Some(ParamMode::Borrow) => Position::Borrow,
-                        // Own / Implicit / unknown → Consume.
+                        // Own / unknown → Consume.
                         _ => Position::Consume,
                     };
                     self.walk(arg, arg_pos);
@@ -903,7 +916,7 @@ impl<'a> Checker<'a> {
                 if param_modes.is_empty() {
                     // All-implicit case (legacy): no mode info → all
                     // Consume, by the rule above.
-                    vec![ParamMode::Implicit; n_args]
+                    vec![ParamMode::Own; n_args]
                 } else {
                     param_modes.clone()
                 }
@@ -1444,14 +1457,10 @@ fn relax_param_to_borrow(inner: &Type, i: usize) -> Type {
             ret_mode,
             effects,
         } => {
-            // Materialise param_modes to full length so the relaxed
-            // mode is positioned correctly even when the original
-            // vec was elided to "all-implicit empty" (not the case
-            // here — we only reach this for an `Own` slot — but
-            // defensive).
-            let mut new_modes: Vec<ParamMode> = (0..params.len())
-                .map(|j| param_modes.get(j).copied().unwrap_or(ParamMode::Implicit))
-                .collect();
+            // `param_modes.len() == params.len()` (spec 0062: every
+            // slot is moded), so a direct clone places the relaxed
+            // mode correctly.
+            let mut new_modes: Vec<ParamMode> = param_modes.clone();
             if i < new_modes.len() {
                 new_modes[i] = ParamMode::Borrow;
             }
@@ -1503,7 +1512,7 @@ mod tests {
                     .collect(),
                 param_modes: modes.clone(),
                 ret: Box::new(Type::int()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: (0..modes.len()).map(|i| format!("p{i}")).collect(),
@@ -1529,7 +1538,7 @@ mod tests {
                 }],
                 param_modes: vec![mode],
                 ret: Box::new(Type::int()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["p0".into()],
@@ -1684,7 +1693,7 @@ mod tests {
                 params: vec![Type::Con { name: "Int".into(), args: vec![] }],
                 param_modes: vec![ParamMode::Own],
                 ret: Box::new(Type::int()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["p0".into()],
@@ -1874,17 +1883,18 @@ mod tests {
             imports: vec![],
             defs: vec![fn_with_modes(
                 "f",
-                vec![ParamMode::Implicit],
+                vec![ParamMode::Own],
                 Term::Var { name: "p0".into() },
             )],
         };
         assert!(check_module(&m).is_empty());
     }
 
-    /// Mixed Implicit + Borrow → still skipped (any Implicit disables
-    /// the check entirely, per the activation gate).
+    /// Post-cutover (spec 0062): every param is explicitly `Own`/`Borrow`,
+    /// so a mixed `[Borrow, Own]` fn is checked (no Implicit exemption
+    /// remains). The unused `Own` param trips `over-strict-mode`.
     #[test]
-    fn mixed_implicit_explicit_is_exempt() {
+    fn mixed_borrow_own_unused_own_fires_over_strict() {
         let m = Module {
             schema: ailang_core::SCHEMA.into(),
             name: "t".into(),
@@ -1892,11 +1902,15 @@ mod tests {
             imports: vec![],
             defs: vec![fn_with_modes(
                 "f",
-                vec![ParamMode::Borrow, ParamMode::Implicit],
+                vec![ParamMode::Borrow, ParamMode::Own],
                 Term::Lit { lit: Literal::Int { value: 0 } },
             )],
         };
-        assert!(check_module(&m).is_empty());
+        let diags = check_module(&m);
+        assert!(
+            diags.iter().any(|d| d.code == "over-strict-mode"),
+            "the unused `Own` param must fire over-strict-mode; got: {diags:#?}"
+        );
     }
 
     /// All-explicit fn that NEVER uses its params, annotated `Borrow`:
@@ -2011,7 +2025,7 @@ mod tests {
                 params: vec![Type::Con { name: "List".into(), args: vec![] }],
                 param_modes: vec![ParamMode::Borrow],
                 ret: Box::new(Type::int()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["xs".into()],
@@ -2052,17 +2066,14 @@ mod tests {
             !d.suggested_rewrites.is_empty(),
             "diagnostic should carry a suggested rewrite"
         );
-        // The replacement is a fn-type, so it does not have to round-trip
-        // through `parse_term` (which parses terms). We only assert it's
-        // a non-empty string that mentions the relaxed `(borrow ...)`.
+        // The replacement is a fn-type. Post-cutover every slot is moded,
+        // so the rewrite legitimately carries `(own ...)` on the return
+        // slot; the property under test is that the over-strict *param*
+        // slot is relaxed to `(borrow ...)`.
         let rep = &d.suggested_rewrites[0].replacement;
         assert!(
-            rep.contains("(borrow"),
-            "rewrite should mention `(borrow`; got {rep}"
-        );
-        assert!(
-            !rep.contains("(own"),
-            "rewrite should NOT contain the original `(own`; got {rep}"
+            rep.contains("(params (borrow (con List)))"),
+            "rewrite should relax the param to `(borrow (con List))`; got {rep}"
         );
     }
 
@@ -2183,7 +2194,7 @@ mod tests {
                 params: vec![Type::Con { name: "IntList".into(), args: vec![] }],
                 param_modes: vec![ParamMode::Own],
                 ret: Box::new(Type::int()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["xs".into()],
@@ -2257,7 +2268,7 @@ mod tests {
                 params: vec![Type::Con { name: "State".into(), args: vec![] }],
                 param_modes: vec![ParamMode::Own],
                 ret: Box::new(Type::Con { name: "State".into(), args: vec![] }),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["st".into()],
@@ -2386,6 +2397,92 @@ mod tests {
         );
     }
 
+    /// `over-strict-mode` does NOT fire on a never-consumed `(own V)`
+    /// param whose type is value-typed (`Int`/`Bool`/`Float`/`Unit`).
+    /// Property: for a value-typed param the lint's own suggested
+    /// rewrite — `(borrow V)` — is itself a `borrow-over-value` error
+    /// (lib.rs), so `(own V)` is the only legal mode and a suggestion
+    /// to relax it is incoherent. The fn body is real (a literal), so
+    /// the only reason the param looks "over-strict" is its value type;
+    /// the lint must stay silent regardless.
+    #[test]
+    fn over_strict_mode_silent_when_param_is_value_typed() {
+        // Body: (lit 0) — `p0 : (own (con Int))` is never used at all.
+        let body = Term::Lit { lit: Literal::Int { value: 0 } };
+        let f = Def::Fn(FnDef {
+            name: "f".into(),
+            ty: Type::Fn {
+                params: vec![Type::int()],
+                param_modes: vec![ParamMode::Own],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Own,
+                effects: vec![],
+            },
+            params: vec!["p0".into()],
+            body,
+            suppress: vec![],
+            doc: None,
+            export: None,
+        });
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            kernel: false,
+            imports: vec![],
+            defs: vec![f],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "over-strict-mode"),
+            "no over-strict-mode expected for a value-typed `(own Int)` \
+             param: `(borrow Int)` is a borrow-over-value error, so `own` \
+             is the only legal mode; got {diags:?}"
+        );
+    }
+
+    /// `over-strict-mode` does NOT fire on a fn whose body is
+    /// `Term::Intrinsic`, even when an `(own HeapType)` param looks
+    /// never-consumed. Property: the linearity walk does nothing for an
+    /// intrinsic body (`Term::Intrinsic => {}`), so `consume_count == 0`
+    /// is a guaranteed false positive — the param modes of an intrinsic
+    /// are hand-authored contracts, not lint-derivable from a walkable
+    /// body.
+    #[test]
+    fn over_strict_mode_silent_for_intrinsic_body() {
+        // `(own IntList)` param, body = (intrinsic). IntList is heap-typed,
+        // so the only reason the lint would stay silent post-fix is the
+        // intrinsic-body guard, not the value-type guard.
+        let f = Def::Fn(FnDef {
+            name: "f".into(),
+            ty: Type::Fn {
+                params: vec![Type::Con { name: "IntList".into(), args: vec![] }],
+                param_modes: vec![ParamMode::Own],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Own,
+                effects: vec![],
+            },
+            params: vec!["p0".into()],
+            body: Term::Intrinsic,
+            suppress: vec![],
+            doc: None,
+            export: None,
+        });
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            kernel: false,
+            imports: vec![],
+            defs: vec![intlist_typedef(), f],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "over-strict-mode"),
+            "no over-strict-mode expected for an intrinsic-bodied fn: the \
+             walk cannot observe consumption, so consume_count==0 is a \
+             false positive; got {diags:?}"
+        );
+    }
+
     /// a borrow-mode fn that forwards its borrow
     /// params into a class-method call must not fire
     /// `consume-while-borrowed` false positives. The pre-fix behaviour
@@ -2410,7 +2507,7 @@ mod tests {
                     ],
                     param_modes: vec![ParamMode::Borrow, ParamMode::Borrow],
                     ret: Box::new(Type::bool_()),
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                     effects: vec![],
                 },
                 default: None,
@@ -2427,7 +2524,7 @@ mod tests {
                 ],
                 param_modes: vec![ParamMode::Borrow, ParamMode::Borrow],
                 ret: Box::new(Type::bool_()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["x".into(), "y".into()],

crates/ailang-check/src/lower_to_mir.rs

@@ -260,11 +260,31 @@ fn lower_term(ctx: &mut Ctx, t: &Term) -> Result<MTerm> {
                 .iter()
                 .enumerate()
                 .map(|(i, a)| {
-                    Ok(MArg {
-                        term: lower_term(ctx, a)?,
-                        mode: param_mode_at(&sig, i),
-                        consume_count: 1,
-                    })
+                    let mode = param_mode_at(&sig, i);
+                    let mut term = lower_term(ctx, a)?;
+                    // mir.4 leg D: a `Str` literal passed BY VALUE into an
+                    // owned (`Own`) param the callee drops must be an owned
+                    // heap slab, not a header-less static rodata constant.
+                    // The cutover's now-active Own-param drop path emits
+                    // `ailang_rc_dec` on the argument; dec'ing a
+                    // `StrRep::Static` reads `payload-8` (the length field)
+                    // as a fake refcount and `free()`s a static address ->
+                    // SIGSEGV. Flip the rep to Heap so codegen emits
+                    // `ailang_str_clone` (rc-headered, refcount 1) and the
+                    // callee's single dec is sound. Gated STRICTLY on `Own`:
+                    // a `Borrow` param fires no `rc_dec`, so borrow-arg
+                    // literals MUST stay `StrRep::Static` (no spurious
+                    // clone). This is the fourth Static->Heap promotion,
+                    // siblings to the seed/tail/recur loop-carried ones.
+                    if matches!(mode, Mode::Owned) {
+                        let arg_ty = ctx.synth_pure(a)?;
+                        if is_str_ty(&arg_ty) {
+                            if let MTerm::Str { rep, .. } = &mut term {
+                                *rep = StrRep::Heap;
+                            }
+                        }
+                    }
+                    Ok(MArg { term, mode, consume_count: 1 })
                 })
                 .collect::<Result<Vec<_>>>()?;
             let m_callee = match class {

crates/ailang-check/src/mono.rs

@@ -588,6 +588,15 @@ pub fn scoped_base(scope: &Option<String>, name: &str) -> String {
     }
 }
 
+/// Public view of the per-type-arg mono suffix mangler. Codegen's
+/// per-monomorph drop-fn naming (`drop_<m>_Pair__Int_Int`) reuses this
+/// exact mangling so a drop symbol's suffix matches the fn-symbol
+/// scheme byte-for-byte. Delegates to the same private helper
+/// `mono_symbol_n` uses, so its fn-symbol output is unperturbed.
+pub fn type_mono_suffix(ty: &Type) -> String {
+    type_to_mono_suffix(ty)
+}
+
 fn type_to_mono_suffix(ty: &Type) -> String {
     match primitive_surface_name(ty) {
         Some(p) => p.to_string(),

crates/ailang-check/src/reuse_shape.rs

@@ -29,10 +29,8 @@
 //! ## Activation gate
 //!
 //! Same as `linearity::check_module`: only fns whose `Type::Fn.param_modes`
-//! is non-empty AND contains no [`ParamMode::Implicit`]. Reuse-as is
-//! part of the explicit-mode discipline; firing the check on legacy
-//! all-`Implicit` fns would risk false positives on workloads that
-//! never opted into the explicit-mode lane.
+//! is non-empty (a nullary fn has no binders to track). Every mode is
+//! explicit `Own`/`Borrow` (spec 0062).
 //!
 //! ## Path-ctor resolution
 //!
@@ -96,19 +94,14 @@ pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
     diags
 }
 
-/// Per-fn check. Skips fns whose signature has any `Implicit` param
-/// (legacy back-compat lane) or whose param list is empty (no binders
+/// Per-fn check. Skips fns whose param list is empty (no binders
 /// to track).
 fn check_fn(f: &FnDef, types: &HashMap<String, TypeDef>, diags: &mut Vec<Diagnostic>) {
     let param_modes: &[ParamMode] = match strip_forall(&f.ty) {
         Type::Fn { param_modes, .. } => param_modes.as_slice(),
         _ => return,
     };
-    if param_modes.is_empty()
-        || param_modes
-            .iter()
-            .any(|m| matches!(m, ParamMode::Implicit))
-    {
+    if param_modes.is_empty() {
         return;
     }
 
@@ -607,7 +600,7 @@ mod tests {
                     .collect(),
                 param_modes: modes.clone(),
                 ret: Box::new(Type::Con { name: "List".into(), args: vec![] }),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: (0..modes.len()).map(|i| format!("p{i}")).collect(),

crates/ailang-check/src/suppress_filter.rs

@@ -120,7 +120,7 @@ mod tests {
                     params: vec![],
                     param_modes: vec![],
                     ret: Box::new(Type::int()),
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                     effects: vec![],
                 },
                 params: vec![],

crates/ailang-check/src/uniqueness.rs

@@ -449,7 +449,7 @@ impl<'a> Walker<'a> {
         match inner {
             Type::Fn { param_modes, .. } => {
                 if param_modes.is_empty() {
-                    vec![ParamMode::Implicit; n_args]
+                    vec![ParamMode::Own; n_args]
                 } else {
                     param_modes.clone()
                 }
@@ -510,7 +510,7 @@ mod tests {
                 params: params.iter().map(|_| Type::int()).collect(),
                 param_modes: vec![],
                 ret: Box::new(Type::int()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: params.into_iter().map(|s| s.to_string()).collect(),

crates/ailang-check/tests/workspace.rs

@@ -146,7 +146,7 @@ fn body_errors_accumulate_across_defs() {
             ret: Box::new(Type::int()),
             effects: vec![],
             param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
         },
         params: vec![],
         body: Term::App {
@@ -169,7 +169,7 @@ fn body_errors_accumulate_across_defs() {
             ret: Box::new(Type::int()),
             effects: vec![],
             param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
         },
         params: vec![],
         body: Term::Var {
@@ -229,7 +229,7 @@ fn use_after_consume_on_own_param_is_reported() {
             params: vec![Type::Con { name: "List".into(), args: vec![] }],
             param_modes: vec![ParamMode::Own],
             ret: Box::new(Type::int()),
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
             effects: vec![],
         },
         params: vec!["ys".into()],
@@ -240,7 +240,7 @@ fn use_after_consume_on_own_param_is_reported() {
     });
 
     // The offending fn. Body is `(+ (sum_list xs) (sum_list xs))` — both
-    // arg slots of `+` are Implicit/Consume, so `xs` is consumed twice
+    // arg slots of `+` are Own/Consume, so `xs` is consumed twice
     // without intervening clone. The second occurrence triggers
     // `use-after-consume`. (Using `+` rather than `Seq` keeps the
     // function's return-type Int, which matches its declared signature.)
@@ -250,7 +250,7 @@ fn use_after_consume_on_own_param_is_reported() {
             params: vec![Type::Con { name: "List".into(), args: vec![] }],
             param_modes: vec![ParamMode::Own],
             ret: Box::new(Type::int()),
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
             effects: vec![],
         },
         params: vec!["xs".into()],
@@ -362,7 +362,7 @@ fn consume_while_borrowed_in_sibling_arg_is_reported() {
             ],
             param_modes: vec![ParamMode::Borrow, ParamMode::Own],
             ret: Box::new(Type::int()),
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
             effects: vec![],
         },
         params: vec!["a".into(), "b".into()],
@@ -378,7 +378,7 @@ fn consume_while_borrowed_in_sibling_arg_is_reported() {
             params: vec![Type::Con { name: "List".into(), args: vec![] }],
             param_modes: vec![ParamMode::Own],
             ret: Box::new(Type::int()),
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
             effects: vec![],
         },
         params: vec!["xs".into()],

crates/ailang-codegen/src/drop.rs

@@ -27,7 +27,7 @@
 
 use ailang_core::ast::{ParamMode, Type, TypeDef};
 use ailang_mir::{Callee, MTerm};
-use std::collections::BTreeSet;
+use std::collections::{BTreeMap, BTreeSet};
 
 use super::synth::llvm_type;
 use super::{AllocStrategy, Emitter, FnSig, Result};
@@ -76,10 +76,44 @@ impl<'a> Emitter<'a> {
     /// is known to grow, recursive cascade everywhere else (cheaper
     /// IR, no worklist allocation).
     pub(crate) fn emit_drop_fn_for_type(&mut self, td: &TypeDef) {
+        // Monomorphic / intrinsic ADTs: one drop fn, empty subst, no
+        // suffix — byte-identical to the pre-leg-C emission.
+        let key = (self.module_name.to_string(), td.name.clone());
+        if !self.drop_monos.is_suffixed(&key) {
+            self.emit_drop_fn_for_instantiation(td, &BTreeMap::new(), "");
+            return;
+        }
+        // Polymorphic ADTs: one drop fn per concrete instantiation
+        // collected workspace-wide (leg C). Each fn substitutes the
+        // declared type-vars to the instantiation's concrete args so
+        // the dec-vs-skip decision is made on the *monomorph* field
+        // type (a value-type field is an inline scalar → skipped; a
+        // heap field is dec'd via its own per-monomorph drop symbol).
+        for args in self.drop_monos.instantiations(&key) {
+            let subst: BTreeMap<String, Type> =
+                td.vars.iter().cloned().zip(args.iter().cloned()).collect();
+            let suffix = self
+                .drop_monos
+                .suffix_for(&key, &args)
+                .unwrap_or_default();
+            self.emit_drop_fn_for_instantiation(td, &subst, &suffix);
+        }
+    }
+
+    /// emit one recursive `drop_<m>_<T><suffix>` body. `subst` maps the
+    /// declared type-vars to the concrete instantiation args (empty for
+    /// monomorphic ADTs); `sym_suffix` is the `__<...>` mono suffix
+    /// (empty for monomorphic ADTs).
+    fn emit_drop_fn_for_instantiation(
+        &mut self,
+        td: &TypeDef,
+        subst: &BTreeMap<String, Type>,
+        sym_suffix: &str,
+    ) {
         let m = self.module_name;
         let tname = &td.name;
         let mut out = String::new();
-        out.push_str(&format!("define void @drop_{m}_{tname}(ptr %p) {{\n"));
+        out.push_str(&format!("define void @drop_{m}_{tname}{sym_suffix}(ptr %p) {{\n"));
         out.push_str("entry:\n");
         // Null guard: a null payload is a no-op (matches
         // `runtime/rc.c::ailang_rc_dec`'s null guard).
@@ -101,14 +135,16 @@ impl<'a> Emitter<'a> {
         let mut local = 0u64;
         for (i, ctor) in td.ctors.iter().enumerate() {
             out.push_str(&format!("arm_{i}:\n"));
-            for (j, fty) in ctor.fields.iter().enumerate() {
-                // Decide what to call for this field. If the field
-                // lowers to `ptr` (boxed), we issue a `dec` call.
-                // For known ADT field types we route through that
-                // ADT's own drop fn so the recursion cascades; for
-                // anything else that lowers to `ptr` (Str, fn-typed,
-                // unresolved Var), fall back to plain `ailang_rc_dec`.
-                let lty = llvm_type(fty).unwrap_or_else(|_| "ptr".into());
+            for (j, fty_decl) in ctor.fields.iter().enumerate() {
+                // Substitute the declared field type to its monomorph.
+                // A value-type field (`Int`/`Bool`/`Float`/`Unit`)
+                // lowers to a non-`ptr` scalar → skip the dec (it is
+                // stored inline, NOT a heap pointer — `rc_dec` on it
+                // would SIGSEGV). A heap field lowers to `ptr` → dec via
+                // `field_drop_call` on the *concrete* type, so the
+                // cascade targets the field's own per-monomorph symbol.
+                let fty = super::subst::apply_subst_to_type(fty_decl, subst);
+                let lty = llvm_type(&fty).unwrap_or_else(|_| "ptr".into());
                 if lty != "ptr" {
                     continue;
                 }
@@ -124,7 +160,7 @@ impl<'a> Emitter<'a> {
                 out.push_str(&format!(
                     "  %v{val_id} = load ptr, ptr %a{addr_id}, align 8\n"
                 ));
-                let drop_call = self.field_drop_call(fty);
+                let drop_call = self.field_drop_call(&fty);
                 // Recursive call into the field's drop fn. If the
                 // field's type is itself `(drop-iterative)`, that drop
                 // fn is the worklist variant — recursion stops at one
@@ -227,10 +263,36 @@ impl<'a> Emitter<'a> {
     /// worklist entry shape. The mono-typed version captures the
     /// stack-overflow-on-long-self-chains problem fully.
     pub(crate) fn emit_iterative_drop_fn_for_type(&mut self, td: &TypeDef) {
+        let key = (self.module_name.to_string(), td.name.clone());
+        if !self.drop_monos.is_suffixed(&key) {
+            self.emit_iterative_drop_fn_for_instantiation(td, &BTreeMap::new(), "");
+            return;
+        }
+        for args in self.drop_monos.instantiations(&key) {
+            let subst: BTreeMap<String, Type> =
+                td.vars.iter().cloned().zip(args.iter().cloned()).collect();
+            let suffix = self
+                .drop_monos
+                .suffix_for(&key, &args)
+                .unwrap_or_default();
+            self.emit_iterative_drop_fn_for_instantiation(td, &subst, &suffix);
+        }
+    }
+
+    /// emit one iterative `drop_<m>_<T><suffix>` body (worklist variant).
+    /// `subst` / `sym_suffix` carry the leg-C per-monomorph
+    /// instantiation, identical in role to
+    /// [`Self::emit_drop_fn_for_instantiation`].
+    fn emit_iterative_drop_fn_for_instantiation(
+        &mut self,
+        td: &TypeDef,
+        subst: &BTreeMap<String, Type>,
+        sym_suffix: &str,
+    ) {
         let m = self.module_name;
         let tname = &td.name;
         let mut out = String::new();
-        out.push_str(&format!("define void @drop_{m}_{tname}(ptr %p) {{\n"));
+        out.push_str(&format!("define void @drop_{m}_{tname}{sym_suffix}(ptr %p) {{\n"));
         out.push_str("entry:\n");
         // Null guard — symmetric with the recursive variant. A null
         // payload skips worklist allocation entirely.
@@ -265,8 +327,12 @@ impl<'a> Emitter<'a> {
         let mut local = 0u64;
         for (i, ctor) in td.ctors.iter().enumerate() {
             out.push_str(&format!("arm_{i}:\n"));
-            for (j, fty) in ctor.fields.iter().enumerate() {
-                let lty = llvm_type(fty).unwrap_or_else(|_| "ptr".into());
+            for (j, fty_decl) in ctor.fields.iter().enumerate() {
+                // Substitute to the monomorph (same reasoning as the
+                // recursive variant): a value-type field is inline and
+                // must not be dec'd/pushed.
+                let fty = super::subst::apply_subst_to_type(fty_decl, subst);
+                let lty = llvm_type(&fty).unwrap_or_else(|_| "ptr".into());
                 if lty != "ptr" {
                     continue;
                 }
@@ -281,7 +347,7 @@ impl<'a> Emitter<'a> {
                 out.push_str(&format!(
                     "  %v{val_id} = load ptr, ptr %a{addr_id}, align 8\n"
                 ));
-                if self.field_is_same_type(fty, &td.name) {
+                if self.field_is_same_type(&fty, &td.name) {
                     // Same-type field: push onto the worklist —
                     // continues the iterative cascade. Null-guarding
                     // is handled inside `ailang_drop_worklist_push`
@@ -295,7 +361,7 @@ impl<'a> Emitter<'a> {
                     // iterative). `field_drop_call` resolves the
                     // symbol; its null-guard semantics are the same
                     // as the recursive variant.
-                    let drop_call = self.field_drop_call(fty);
+                    let drop_call = self.field_drop_call(&fty);
                     out.push_str(&format!(
                         "  call void @{drop_call}(ptr %v{val_id})\n"
                     ));
@@ -374,7 +440,7 @@ impl<'a> Emitter<'a> {
     /// those are not user-defined ADTs and have no per-type drop fn.
     pub(crate) fn field_drop_call(&self, fty: &Type) -> String {
         match fty {
-            Type::Con { name, .. } => {
+            Type::Con { name, args } => {
                 // Built-in pointer-typed cons: Str. No drop fn —
                 // shallow `ailang_rc_dec` is the right answer.
                 // Str has two realisations sharing the consumer
@@ -395,19 +461,13 @@ impl<'a> Emitter<'a> {
                 if matches!(name.as_str(), "Str") {
                     return "ailang_rc_dec".to_string();
                 }
-                // Qualified `module.T` → drop fn lives in `module`.
-                if name.matches('.').count() == 1 {
-                    let (prefix, suffix) = name.split_once('.').expect("checked");
-                    if let Some(target) = self.import_map.get(prefix) {
-                        return format!("drop_{target}_{suffix}");
-                    }
-                    // Fallback: treat the prefix itself as the owner
-                    // module (typechecker would have rejected an
-                    // unimported prefix earlier).
-                    return format!("drop_{prefix}_{suffix}");
-                }
-                // Bare name: declared in the current module.
-                format!("drop_{m}_{name}", m = self.module_name)
+                // Resolve owner + per-monomorph suffix in one place
+                // (leg C). A polymorphic non-intrinsic ADT instantiation
+                // (`Box Int`, `Pair Int Int`) gets the same `__<suffix>`
+                // the emission loop minted for that instantiation;
+                // monomorphic / intrinsic ADTs keep the un-suffixed
+                // symbol byte-for-byte.
+                self.adt_drop_symbol(name, args)
             }
             // Type::Fn (closure-typed field) → no per-type drop fn
             // exists for closures (each closure has its own per-pair
@@ -431,6 +491,46 @@ impl<'a> Emitter<'a> {
         }
     }
 
+    /// resolve the `drop_<owner>_<T>` symbol for an ADT `Type::Con`,
+    /// applying the leg-C per-monomorph suffix when the resolved ADT is
+    /// polymorphic + non-intrinsic. The caller has already excluded
+    /// `Str` and non-`Con` shapes. `name` is the (possibly qualified)
+    /// type name; `args` are its concrete instantiation arguments.
+    ///
+    /// The suffix decision lives in [`dropmono::DropAdtMeta`], shared
+    /// with the emission loop, so a call symbol matches its definition
+    /// byte-for-byte (a mismatch is an IR link error).
+    pub(crate) fn adt_drop_symbol(&self, name: &str, args: &[Type]) -> String {
+        let key = super::dropmono::resolve_adt_key(
+            name,
+            self.module_name,
+            &self.import_map,
+        );
+        let base = format!("drop_{owner}_{bare}", owner = key.0, bare = key.1);
+        match self.drop_monos.suffix_for(&key, args) {
+            Some(suffix) => format!("{base}{suffix}"),
+            None => base,
+        }
+    }
+
+    /// resolve the `partial_drop_<owner>_<T>` symbol for an ADT
+    /// `Type::Con`, applying the leg-C per-monomorph suffix. Parallel
+    /// to [`Self::adt_drop_symbol`]. The caller has already excluded
+    /// `Str` / non-`Con` shapes.
+    pub(crate) fn adt_partial_drop_symbol(&self, name: &str, args: &[Type]) -> String {
+        let key = super::dropmono::resolve_adt_key(
+            name,
+            self.module_name,
+            &self.import_map,
+        );
+        let base =
+            format!("partial_drop_{owner}_{bare}", owner = key.0, bare = key.1);
+        match self.drop_monos.suffix_for(&key, args) {
+            Some(suffix) => format!("{base}{suffix}"),
+            None => base,
+        }
+    }
+
     /// predicate the `Term::Let` lowering uses to decide
     /// whether a let-binder owns a fresh RC-heap allocation that
     /// codegen should `dec` at scope close.
@@ -448,8 +548,8 @@ impl<'a> Emitter<'a> {
     /// fn-type carries `ret_mode == Own`. The mode contract states that
     /// the callee hands the returned cell's ownership to the caller's
     /// frame; the let-scope close is the right place for the caller's
-    /// dec. Calls whose callee is `Borrow`/`Implicit`-returning are
-    /// still not trackable — they don't carry that signal.
+    /// dec. Calls whose callee is `Borrow`-returning are still not
+    /// trackable — a borrow-return is a view, not an owned ref.
     ///
     /// Other value shapes (vars, literals, matches, …) return `false`
     /// here. A `Term::Var` returning an RC-allocated box would already
@@ -467,11 +567,10 @@ impl<'a> Emitter<'a> {
             MTerm::App { callee, .. } => {
                 // a call whose callee carries
                 // `ret_mode == Own` hands a fresh heap allocation to
-                // the caller's frame. Trackable. `Borrow` and
-                // `Implicit` ret-modes do not carry that signal —
-                // returning by Borrow is a view into the callee's
-                // owned data (caller does not own it), and Implicit
-                // is the back-compat lane that 18c.3's debt covers.
+                // the caller's frame. Trackable. A `Borrow` ret-mode
+                // does not carry that signal — returning by Borrow is a
+                // view into the callee's owned data (caller does not
+                // own it).
                 self.synth_callee_ret_mode(callee)
                     .map(|m| matches!(m, ParamMode::Own))
                     .unwrap_or(false)
@@ -538,15 +637,16 @@ impl<'a> Emitter<'a> {
     pub(crate) fn drop_symbol_for_binder(&self, value: &MTerm, val_ssa: &str) -> String {
         match value {
             MTerm::Ctor { type_name, .. } => {
-                if type_name.matches('.').count() == 1 {
-                    let (prefix, suffix) =
-                        type_name.split_once('.').expect("checked");
-                    if let Some(target) = self.import_map.get(prefix) {
-                        return format!("drop_{target}_{suffix}");
-                    }
-                    return format!("drop_{prefix}_{suffix}");
-                }
-                format!("drop_{m}_{type_name}", m = self.module_name)
+                // The binder's instantiated result type carries the
+                // concrete args (`Box Int` → args `[Int]`); read them off
+                // `value.ty()` so the leg-C per-monomorph suffix matches
+                // the emitted `drop_<m>_Box__Int`. `type_name` alone
+                // would lose the instantiation.
+                let args = match value.ty() {
+                    Type::Con { args, .. } => args,
+                    _ => Vec::new(),
+                };
+                self.adt_drop_symbol(type_name, &args)
             }
             MTerm::Lam { .. } => self
                 .closure_drops
@@ -563,7 +663,7 @@ impl<'a> Emitter<'a> {
             // var on an as-yet-unmonomorphised polymorphic call —
             // the monomorphised copies will resolve correctly).
             MTerm::App { .. } | MTerm::Loop { .. } => {
-                if let Type::Con { name, .. } = value.ty() {
+                if let Type::Con { name, args } = value.ty() {
                     // Symmetric to `field_drop_call`'s Str arm: Str is a
                     // built-in pointer type with no per-type drop fn. Both
                     // heap-Str (rc_header at payload-8) and static-Str
@@ -572,15 +672,7 @@ impl<'a> Emitter<'a> {
                     if name == "Str" {
                         return "ailang_rc_dec".to_string();
                     }
-                    if name.matches('.').count() == 1 {
-                        let (prefix, suffix) =
-                            name.split_once('.').expect("checked");
-                        if let Some(target) = self.import_map.get(prefix) {
-                            return format!("drop_{target}_{suffix}");
-                        }
-                        return format!("drop_{prefix}_{suffix}");
-                    }
-                    return format!("drop_{m}_{name}", m = self.module_name);
+                    return self.adt_drop_symbol(&name, &args);
                 }
                 "ailang_rc_dec".to_string()
             }
@@ -649,11 +741,36 @@ impl<'a> Emitter<'a> {
     /// cascade points — the unmoved fields go through their own
     /// `drop_<m>_<F>` which itself decides recursive vs iterative).
     pub(crate) fn emit_partial_drop_fn_for_type(&mut self, td: &TypeDef) {
+        let key = (self.module_name.to_string(), td.name.clone());
+        if !self.drop_monos.is_suffixed(&key) {
+            self.emit_partial_drop_fn_for_instantiation(td, &BTreeMap::new(), "");
+            return;
+        }
+        for args in self.drop_monos.instantiations(&key) {
+            let subst: BTreeMap<String, Type> =
+                td.vars.iter().cloned().zip(args.iter().cloned()).collect();
+            let suffix = self
+                .drop_monos
+                .suffix_for(&key, &args)
+                .unwrap_or_default();
+            self.emit_partial_drop_fn_for_instantiation(td, &subst, &suffix);
+        }
+    }
+
+    /// emit one `partial_drop_<m>_<T><suffix>` body. `subst` /
+    /// `sym_suffix` carry the leg-C per-monomorph instantiation,
+    /// identical in role to [`Self::emit_drop_fn_for_instantiation`].
+    fn emit_partial_drop_fn_for_instantiation(
+        &mut self,
+        td: &TypeDef,
+        subst: &BTreeMap<String, Type>,
+        sym_suffix: &str,
+    ) {
         let m = self.module_name;
         let tname = &td.name;
         let mut out = String::new();
         out.push_str(&format!(
-            "define void @partial_drop_{m}_{tname}(ptr %p, i64 %mask) {{\n"
+            "define void @partial_drop_{m}_{tname}{sym_suffix}(ptr %p, i64 %mask) {{\n"
         ));
         out.push_str("entry:\n");
         out.push_str("  %is_null = icmp eq ptr %p, null\n");
@@ -671,8 +788,9 @@ impl<'a> Emitter<'a> {
         let mut local = 0u64;
         for (i, ctor) in td.ctors.iter().enumerate() {
             out.push_str(&format!("arm_{i}:\n"));
-            for (j, fty) in ctor.fields.iter().enumerate() {
-                let lty = llvm_type(fty).unwrap_or_else(|_| "ptr".into());
+            for (j, fty_decl) in ctor.fields.iter().enumerate() {
+                let fty = super::subst::apply_subst_to_type(fty_decl, subst);
+                let lty = llvm_type(&fty).unwrap_or_else(|_| "ptr".into());
                 if lty != "ptr" {
                     continue;
                 }
@@ -702,7 +820,7 @@ impl<'a> Emitter<'a> {
                 out.push_str(&format!(
                     "  %v{val_id} = load ptr, ptr %a{addr_id}, align 8\n"
                 ));
-                let drop_call = self.field_drop_call(fty);
+                let drop_call = self.field_drop_call(&fty);
                 out.push_str(&format!(
                     "  call void @{drop_call}(ptr %v{val_id})\n"
                 ));
@@ -788,21 +906,11 @@ impl<'a> Emitter<'a> {
     /// populated for those shapes anyway).
     pub(crate) fn partial_drop_symbol_for_type(&self, ty: &Type) -> Option<String> {
         match ty {
-            Type::Con { name, .. } => {
+            Type::Con { name, args } => {
                 if name == "Str" {
                     return None;
                 }
-                if name.matches('.').count() == 1 {
-                    let (prefix, suffix) = name.split_once('.').expect("checked");
-                    if let Some(target) = self.import_map.get(prefix) {
-                        return Some(format!("partial_drop_{target}_{suffix}"));
-                    }
-                    return Some(format!("partial_drop_{prefix}_{suffix}"));
-                }
-                Some(format!(
-                    "partial_drop_{m}_{name}",
-                    m = self.module_name
-                ))
+                Some(self.adt_partial_drop_symbol(name, args))
             }
             _ => None,
         }
@@ -879,12 +987,28 @@ impl<'a> Emitter<'a> {
             }
         };
         let cref = self.lookup_ctor_by_type(type_name, ctor_name)?;
+        // leg C: substitute the declared field types to the binder's
+        // concrete instantiation (read off `value.ty()`'s args against
+        // the ADT's declared type-vars), so a value-type field is
+        // recognised as inline (non-`ptr`, skipped) and a heap field
+        // routes through its own per-monomorph drop symbol. For a
+        // monomorphic ADT the subst is empty and this is a no-op.
+        let inst_subst: BTreeMap<String, Type> =
+            match (&cref.type_vars, value.ty()) {
+                (vars, Type::Con { args, .. })
+                    if !vars.is_empty() && vars.len() == args.len() =>
+                {
+                    vars.iter().cloned().zip(args.into_iter()).collect()
+                }
+                _ => BTreeMap::new(),
+            };
         // Per-field dec for non-moved pointer-typed slots. ail_fields
         // are the AILang-level field types; field_drop_call resolves
         // them to either `drop_<owner>_<T>` (ADTs cascade) or
         // `ailang_rc_dec` (Str / closures / vars).
-        for (idx, fty_ail) in cref.ail_fields.iter().enumerate() {
-            let lty = llvm_type(fty_ail).unwrap_or_else(|_| "ptr".into());
+        for (idx, fty_decl) in cref.ail_fields.iter().enumerate() {
+            let fty_ail = super::subst::apply_subst_to_type(fty_decl, &inst_subst);
+            let lty = llvm_type(&fty_ail).unwrap_or_else(|_| "ptr".into());
             if lty != "ptr" {
                 continue;
             }
@@ -900,7 +1024,7 @@ impl<'a> Emitter<'a> {
             self.body.push_str(&format!(
                 "  {v} = load ptr, ptr {addr}, align 8\n"
             ));
-            let drop_call = self.field_drop_call(fty_ail);
+            let drop_call = self.field_drop_call(&fty_ail);
             self.body.push_str(&format!(
                 "  call void @{drop_call}(ptr {v})\n"
             ));

crates/ailang-codegen/src/dropmono.rs

@@ -0,0 +1,437 @@
+//! Per-monomorph drop-fn collection for polymorphic ADTs (leg C of
+//! the #55-cutover drop-soundness family).
+//!
+//! Background. Pre-cutover, the per-ADT drop fn was emitted exactly
+//! once per `Def::Type`, keyed by the *declared* field types. For a
+//! polymorphic ADT (`Box a`, `Pair a b`) a ctor field typed at a
+//! type-var `a` failed `synth::llvm_type` and fell back to `ptr`,
+//! emitting an `ailang_rc_dec` on it. At a value-type monomorph
+//! (`Box Int`) that field is an inline `i64`, so `rc_dec(7)`
+//! dereferences the scalar and SIGSEGVs.
+//!
+//! Fix. Emit one drop fn per (polymorphic-ADT, concrete instantiation)
+//! and decide dec-vs-skip on the *substituted* field type. A
+//! value-type field (`Int`/`Bool`/`Float`/`Unit`) is skipped (inline
+//! scalar, no RC); a heap field is dec'd through its own per-monomorph
+//! drop symbol so the cascade composes.
+//!
+//! Symbol naming. A concrete-monomorphic ADT (`vars` empty: IntList,
+//! Ordering) keeps its un-suffixed `drop_<m>_<T>` symbol byte-for-byte
+//! (the `ir_snapshot` goldens pin these). A polymorphic ADT
+//! instantiation gets a mono suffix mangled the same way
+//! `ailang_check::mono::mono_symbol_n` mangles fn symbols
+//! (`drop_<m>_Pair__Int_Int`; compound args hash-route to stay
+//! bounded). Intrinsic-storage types (RawBuf) are polymorphic but use
+//! the flat intrinsic drop path — they are NOT suffixed (their drop is
+//! element-type independent and the golden pins `drop_<m>_RawBuf`).
+//!
+//! This module owns the workspace-global collection
+//! ([`collect_drop_monos`]) and the shared suffix decision
+//! ([`DropAdtMeta`]); the emission and call-site manglers in `drop.rs`
+//! / `match_lower.rs` consult the same [`DropAdtMeta`] so a definition
+//! and its callers always agree on the symbol (a mismatch is a link
+//! error).
+
+use ailang_core::ast::{Def, Module, Term, Type, TypeDef};
+use ailang_mir::{Callee, MArg, MNewArg, MTerm, MirWorkspace};
+use std::collections::{BTreeMap, BTreeSet};
+
+use super::subst::{apply_subst_to_type, qualify_local_types_codegen};
+
+/// A canonical key for an ADT: `(owner_module, bare_type_name)`.
+pub(crate) type AdtKey = (String, String);
+
+/// Workspace-global drop-monomorphisation metadata, built once before
+/// the per-module codegen loop and shared (by reference) with every
+/// `Emitter`.
+#[derive(Debug, Default)]
+pub(crate) struct DropAdtMeta {
+    /// ADTs that take a per-monomorph drop-symbol suffix: declared
+    /// `vars` non-empty AND not intrinsic-storage. A `Type::Con` whose
+    /// resolved key is in this set, and whose `args` are non-empty,
+    /// gets a `__<suffix>` appended to its `drop_`/`partial_drop_`
+    /// symbol.
+    suffixed: BTreeSet<AdtKey>,
+    /// For each suffixed ADT, the concrete arg-tuples it is
+    /// instantiated at across the whole workspace, keyed by a canonical
+    /// hash of the arg-tuple (`Type` is not `Ord`, so the tuple itself
+    /// cannot key a `BTreeSet`; the hash gives a deterministic,
+    /// dedup-stable key). The emission loop reads the values to emit one
+    /// drop fn per instantiation in the owning module.
+    monos: BTreeMap<AdtKey, BTreeMap<String, Vec<Type>>>,
+}
+
+/// Canonical, deterministic key for an arg-tuple (used to dedup
+/// instantiations that `Type`'s non-`Ord`-ness blocks from a set key).
+fn args_key(args: &[Type]) -> String {
+    args.iter()
+        .map(ailang_core::canonical::type_hash)
+        .collect::<Vec<_>>()
+        .join("|")
+}
+
+impl DropAdtMeta {
+    /// Is this ADT (resolved to `key`) suffixed (poly + non-intrinsic)?
+    pub(crate) fn is_suffixed(&self, key: &AdtKey) -> bool {
+        self.suffixed.contains(key)
+    }
+
+    /// The concrete instantiations of `key` to emit in its owner
+    /// module. Empty for monomorphic / intrinsic / never-instantiated
+    /// ADTs.
+    pub(crate) fn instantiations(&self, key: &AdtKey) -> Vec<Vec<Type>> {
+        self.monos
+            .get(key)
+            .map(|s| s.values().cloned().collect())
+            .unwrap_or_default()
+    }
+
+    /// The mono symbol suffix for an instantiation `args`, mangled the
+    /// same way `mono_symbol_n` mangles fn type-args. `None` when the
+    /// type is not suffixed (monomorphic / intrinsic) or has no args —
+    /// caller keeps the un-suffixed base symbol. The leading `__`
+    /// joiner is included so callers concatenate directly.
+    pub(crate) fn suffix_for(&self, key: &AdtKey, args: &[Type]) -> Option<String> {
+        if args.is_empty() || !self.is_suffixed(key) {
+            return None;
+        }
+        // Reuse the fn-symbol mangler: `mono_symbol_n("", &args)` would
+        // prepend an empty base + joiner. We want only the per-arg
+        // suffix joined by `__`, prefixed with the `__` that separates
+        // it from the drop base. Mirror `mono_symbol_n`'s join exactly.
+        let parts: Vec<String> = args
+            .iter()
+            .map(ailang_check::mono::type_mono_suffix)
+            .collect();
+        Some(format!("__{}", parts.join("__")))
+    }
+}
+
+/// Resolve a (possibly qualified) `Type::Con` name to its canonical
+/// `(owner_module, bare_name)` key, using `import_map` for the
+/// qualified case and `current_module` for the bare case.
+pub(crate) fn resolve_adt_key(
+    name: &str,
+    current_module: &str,
+    import_map: &BTreeMap<String, String>,
+) -> AdtKey {
+    if name.matches('.').count() == 1 {
+        let (prefix, suffix) = name.split_once('.').expect("checked");
+        let owner = import_map
+            .get(prefix)
+            .map(|s| s.as_str())
+            .unwrap_or(prefix);
+        (owner.to_string(), suffix.to_string())
+    } else {
+        (current_module.to_string(), name.to_string())
+    }
+}
+
+/// Does this `Def::Type` use the flat intrinsic-storage drop path
+/// (its `new` op is an `(intrinsic)`, not a real term-ctor body)?
+/// Mirror of the gate in `lib.rs`'s drop-fn emission loop.
+fn is_intrinsic_storage(module: &Module, td: &TypeDef) -> bool {
+    module.defs.iter().any(|d| {
+        matches!(d, Def::Fn(f)
+            if f.name == "new"
+                && matches!(f.body, Term::Intrinsic)
+                && fn_returns_type_name(f, &td.name))
+    })
+}
+
+/// Does fn `f` return a `Type::Con` named `tname` (outermost)? Mirror
+/// of `lib.rs::fn_returns_type` (kept local to avoid widening that
+/// fn's visibility).
+fn fn_returns_type_name(f: &ailang_core::ast::FnDef, tname: &str) -> bool {
+    fn outer(t: &Type, tname: &str) -> bool {
+        match t {
+            Type::Con { name, .. } => name == tname,
+            Type::Forall { body, .. } => outer(body, tname),
+            _ => false,
+        }
+    }
+    if let Type::Fn { ret, .. } = &f.ty {
+        outer(ret, tname)
+    } else if let Type::Forall { body, .. } = &f.ty {
+        if let Type::Fn { ret, .. } = body.as_ref() {
+            outer(ret, tname)
+        } else {
+            false
+        }
+    } else {
+        false
+    }
+}
+
+/// Build the workspace-global drop-monomorphisation table: which ADTs
+/// are suffixed, and which concrete instantiations each is used at.
+pub(crate) fn collect_drop_monos(mir: &MirWorkspace) -> DropAdtMeta {
+    let mut meta = DropAdtMeta::default();
+
+    // Per-module set of locally-declared ADT names. Used to qualify a
+    // bare type-con reference (`List` in `std_list`'s body) to its
+    // canonical `module.Type` form *at the module where it appears*, so
+    // a stored arg / field resolves to the same owner regardless of
+    // which module later emits a drop fn referencing it. Without this,
+    // a `Maybe (List Int)` collected in `std_list` would store a bare
+    // `List`, and the drop fn emitted in `std_maybe` (Maybe's owner)
+    // would resolve that bare `List` to `drop_std_maybe_List` (wrong
+    // owner) — an undefined-symbol link error.
+    let mut local_types: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
+
+    // 1. Determine the suffixed set + record each ADT's declared
+    //    type-vars and ctor field types (under their owner module),
+    //    so the fixpoint below can expand nested field instantiations.
+    //    `adt_decl[(m, T)] = (vars, ctor_field_types_flattened)`.
+    let mut adt_decl: BTreeMap<AdtKey, (Vec<String>, Vec<Type>)> = BTreeMap::new();
+    for (mname, mir_module) in &mir.modules {
+        let m = &mir_module.ast;
+        for def in &m.defs {
+            if let Def::Type(td) = def {
+                let key = (mname.clone(), td.name.clone());
+                let fields: Vec<Type> =
+                    td.ctors.iter().flat_map(|c| c.fields.clone()).collect();
+                adt_decl.insert(key.clone(), (td.vars.clone(), fields));
+                local_types
+                    .entry(mname.clone())
+                    .or_default()
+                    .insert(td.name.clone());
+                if !td.vars.is_empty() && !is_intrinsic_storage(m, td) {
+                    meta.suffixed.insert(key);
+                }
+            }
+        }
+    }
+
+    // 2. Seed the instantiation set by walking every MIR body / const
+    //    and collecting every `Type` that appears. Each walked type is
+    //    qualified against its module's local types before collection,
+    //    so stored args carry canonical `module.Type` names.
+    let mut seeds: Vec<(AdtKey, Vec<Type>)> = Vec::new();
+    for (mname, mir_module) in &mir.modules {
+        let m = &mir_module.ast;
+        let import_map = build_import_map(m);
+        let owner_local = local_types.get(mname).cloned().unwrap_or_default();
+        let mut sink = |t: &Type| {
+            let q = qualify_local_types_codegen(t, mname, &owner_local);
+            collect_instantiations(&q, mname, &import_map, &meta.suffixed, &mut seeds);
+        };
+        for d in &mir_module.defs {
+            walk_term_types(&d.body, &mut sink);
+        }
+        for c in &mir_module.consts {
+            walk_term_types(&c.body, &mut sink);
+        }
+        // Also walk every fn signature type appearing in the AST defs —
+        // an Own-returned polymorphic ADT whose ctor is built in a
+        // callee still needs its drop emitted in the caller's module
+        // when the let-close decs it. The body walk catches the ctor
+        // site; the signature walk is belt-and-braces for ret types
+        // that surface only through a call.
+        for def in &m.defs {
+            if let Def::Fn(f) = def {
+                walk_type(&f.ty, &mut sink);
+            }
+        }
+    }
+
+    // 3. Fixpoint: an instantiation `T<args>` needs each of its ctor
+    //    fields, substituted by {var -> arg}, to also be emitted (a
+    //    `Pair (Box Int) Int` field-drops `Box Int`). Expand until no
+    //    new (key, args) pairs appear. Dedup on `(AdtKey, args-hash)`
+    //    since `Type` is not `Ord`.
+    let mut worklist: Vec<(AdtKey, Vec<Type>)> = seeds;
+    let mut seen: BTreeSet<(AdtKey, String)> = BTreeSet::new();
+    while let Some((key, args)) = worklist.pop() {
+        let ak = args_key(&args);
+        if !seen.insert((key.clone(), ak.clone())) {
+            continue;
+        }
+        meta.monos
+            .entry(key.clone())
+            .or_default()
+            .insert(ak, args.clone());
+        let Some((vars, fields)) = adt_decl.get(&key) else {
+            continue;
+        };
+        if vars.len() != args.len() {
+            // Defensive: arity mismatch means our resolution missed;
+            // skip rather than mis-substitute.
+            continue;
+        }
+        let subst: BTreeMap<String, Type> =
+            vars.iter().cloned().zip(args.iter().cloned()).collect();
+        // Field types are written in the owner module's local
+        // namespace; resolve against the owner's import map and qualify
+        // the owner's own bare type-cons (e.g. a `List a` self-field, or
+        // a sibling ADT) so the nested instantiation keys on the
+        // canonical owner. The substituted-in args are already
+        // qualified from the seed pass.
+        let owner = key.0.clone();
+        let import_map = mir
+            .modules
+            .get(&owner)
+            .map(|mm| build_import_map(&mm.ast))
+            .unwrap_or_default();
+        let owner_local = local_types.get(&owner).cloned().unwrap_or_default();
+        for f in fields {
+            let concrete = apply_subst_to_type(f, &subst);
+            let concrete = qualify_local_types_codegen(&concrete, &owner, &owner_local);
+            collect_instantiations(
+                &concrete,
+                &owner,
+                &import_map,
+                &meta.suffixed,
+                &mut worklist,
+            );
+        }
+    }
+
+    meta
+}
+
+/// Build a module's import map (alias|name -> actual module), mirroring
+/// the per-module loop in `lower_workspace_inner`.
+fn build_import_map(m: &Module) -> BTreeMap<String, String> {
+    let mut import_map: BTreeMap<String, String> = BTreeMap::new();
+    for imp in &m.imports {
+        let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
+        import_map.insert(key, imp.module.clone());
+    }
+    if m.name != "prelude" {
+        import_map
+            .entry("prelude".to_string())
+            .or_insert_with(|| "prelude".to_string());
+    }
+    import_map
+}
+
+/// Collect, from a single `Type`, every suffixed-ADT instantiation
+/// (recursing into args).
+fn collect_instantiations(
+    t: &Type,
+    current_module: &str,
+    import_map: &BTreeMap<String, String>,
+    suffixed: &BTreeSet<AdtKey>,
+    out: &mut Vec<(AdtKey, Vec<Type>)>,
+) {
+    match t {
+        Type::Con { name, args } => {
+            if !args.is_empty() {
+                let key = resolve_adt_key(name, current_module, import_map);
+                if suffixed.contains(&key) {
+                    out.push((key, args.clone()));
+                }
+            }
+            for a in args {
+                collect_instantiations(a, current_module, import_map, suffixed, out);
+            }
+        }
+        Type::Fn { params, ret, .. } => {
+            for p in params {
+                collect_instantiations(p, current_module, import_map, suffixed, out);
+            }
+            collect_instantiations(ret, current_module, import_map, suffixed, out);
+        }
+        Type::Forall { body, .. } => {
+            collect_instantiations(body, current_module, import_map, suffixed, out)
+        }
+        Type::Var { .. } => {}
+    }
+}
+
+/// Apply `sink` to every `Type` reachable from a `Type`.
+fn walk_type<F: FnMut(&Type)>(t: &Type, sink: &mut F) {
+    sink(t);
+}
+
+/// Apply `sink` to every `Type` carried by `term` and its sub-terms.
+/// `sink` itself recurses into the type structure
+/// ([`collect_instantiations`]), so this walker only has to surface
+/// every type-bearing node once.
+fn walk_term_types<F: FnMut(&Type)>(term: &MTerm, sink: &mut F) {
+    // The node's own static type.
+    let ty = term.ty();
+    sink(&ty);
+    match term {
+        MTerm::Lit { .. }
+        | MTerm::Var { .. }
+        | MTerm::Str { .. }
+        | MTerm::Intrinsic { .. }
+        | MTerm::Recur { .. } => {}
+        MTerm::App { callee, args, .. } => {
+            walk_callee_types(callee, sink);
+            walk_args(args, sink);
+        }
+        MTerm::Do { args, .. } => walk_args(args, sink),
+        MTerm::Ctor { args, .. } => walk_args(args, sink),
+        MTerm::New { elem, args, .. } => {
+            if let Some(e) = elem {
+                sink(e);
+            }
+            for a in args {
+                if let MNewArg::Value(v) = a {
+                    walk_term_types(v, sink);
+                } else if let MNewArg::Type(t) = a {
+                    sink(t);
+                }
+            }
+        }
+        MTerm::Let { init, body, .. } => {
+            walk_term_types(init, sink);
+            walk_term_types(body, sink);
+        }
+        MTerm::LetRec { sig, body, in_term, .. } => {
+            sink(sig);
+            walk_term_types(body, sink);
+            walk_term_types(in_term, sink);
+        }
+        MTerm::If { cond, then, else_, .. } => {
+            walk_term_types(cond, sink);
+            walk_term_types(then, sink);
+            walk_term_types(else_, sink);
+        }
+        MTerm::Match { scrutinee, arms, .. } => {
+            walk_term_types(scrutinee, sink);
+            for arm in arms {
+                walk_term_types(&arm.body, sink);
+            }
+        }
+        MTerm::Lam { param_tys, ret_ty, body, .. } => {
+            for p in param_tys {
+                sink(p);
+            }
+            sink(ret_ty);
+            walk_term_types(body, sink);
+        }
+        MTerm::Seq { lhs, rhs, .. } => {
+            walk_term_types(lhs, sink);
+            walk_term_types(rhs, sink);
+        }
+        MTerm::Clone { value, .. } => walk_term_types(value, sink),
+        MTerm::ReuseAs { source, body, .. } => {
+            walk_term_types(source, sink);
+            walk_term_types(body, sink);
+        }
+        MTerm::Loop { binders, body, .. } => {
+            for b in binders {
+                sink(&b.ty);
+                walk_term_types(&b.init, sink);
+            }
+            walk_term_types(body, sink);
+        }
+    }
+}
+
+fn walk_args<F: FnMut(&Type)>(args: &[MArg], sink: &mut F) {
+    for a in args {
+        walk_term_types(&a.term, sink);
+    }
+}
+
+fn walk_callee_types<F: FnMut(&Type)>(callee: &Callee, sink: &mut F) {
+    match callee {
+        Callee::Static { sig, .. } | Callee::Builtin { sig, .. } => sink(sig),
+        Callee::Indirect(inner) => walk_term_types(inner, sink),
+    }
+}

crates/ailang-codegen/src/lambda.rs

@@ -153,15 +153,13 @@ impl<'a> Emitter<'a> {
         let saved_entry_marker = self.entry_block_end_marker.take();
         // A lambda thunk is its own fn frame for
         // param-mode lookup. The outer fn's params are not in scope
-        // inside the thunk; the thunk's own params are pushed below
-        // and (currently) carry no mode annotation, so they default
-        // to `Implicit` — `lower_match`'s Iter A gate will skip arm-
-        // close pattern-binder dec for matches on lambda params,
-        // mirroring the fn-level Implicit-param treatment.
+        // inside the thunk; the thunk's own params carry no surface
+        // annotation, so they are synthesised `Own` — the consume-side
+        // default that owns its argument for the thunk body.
         let saved_param_modes = std::mem::take(&mut self.current_param_modes);
         for pname in lam_params.iter() {
             self.current_param_modes
-                .insert(pname.clone(), ParamMode::Implicit);
+                .insert(pname.clone(), ParamMode::Own);
         }
         // Lambdas inside lambdas are fine: they get their own counter
         // namespace within the enclosing thunk. They share the

crates/ailang-codegen/src/lib.rs

@@ -40,6 +40,7 @@ use ailang_mir::{Callee, MArg, MTerm, MirDef, MirWorkspace, Mode, StrRep};
 use std::collections::{BTreeMap, BTreeSet};
 
 mod drop;
+mod dropmono;
 mod escape;
 mod intercepts;
 mod lambda;
@@ -396,6 +397,14 @@ fn lower_workspace_inner(mir: &MirWorkspace, alloc: AllocStrategy, target: Targe
         module_consts.insert(mname.clone(), consts);
     }
 
+    // Leg C: workspace-global per-monomorph drop metadata. Built once
+    // here (after the symbol-table pass, before lowering) and shared by
+    // reference with every `Emitter`. Computes which polymorphic ADTs
+    // take a per-instantiation drop fn and the concrete arg-tuples each
+    // is used at, so the emission loop and the call-site manglers agree
+    // on every `drop_<m>_<T>__<suffix>` symbol.
+    let drop_monos = dropmono::collect_drop_monos(mir);
+
     // Pass 2: lower per module. Globals/strings are accumulated per module,
     // because they are mangled per module.
     for (mname, mir_module) in &mir.modules {
@@ -432,6 +441,7 @@ fn lower_workspace_inner(mir: &MirWorkspace, alloc: AllocStrategy, target: Targe
             &module_ctor_index,
             &module_consts,
             import_map,
+            &drop_monos,
             alloc,
         );
         emitter
@@ -770,6 +780,13 @@ struct Emitter<'a> {
     module_user_fns: &'a BTreeMap<String, BTreeMap<String, FnSig>>,
     /// Import map of the current module (alias/module name → actual module name).
     import_map: BTreeMap<String, String>,
+    /// workspace-global per-monomorph drop metadata (leg C). Tells the
+    /// drop-fn emission loop which polymorphic ADTs to emit one drop fn
+    /// per instantiation for, and tells the call-site manglers whether
+    /// a `Type::Con` takes a per-monomorph `__<suffix>` on its
+    /// `drop_`/`partial_drop_` symbol. Shared by reference with every
+    /// `Emitter`.
+    drop_monos: &'a dropmono::DropAdtMeta,
     /// ADT table: type_name -> list of ctors in definition order.
     /// Tag of a ctor = index in this list.
     /// Kept around for future tools (pretty-printer for ADT values,
@@ -874,15 +891,15 @@ struct Emitter<'a> {
     /// entry) from the fn type's `param_modes`. Consulted by
     /// `lower_match`'s arm-close pattern-binder dec emission (Iter A) to
     /// decide whether the scrutinee was statically owned: if the
-    /// scrutinee resolves to a fn-param whose mode is `Borrow` or
-    /// `Implicit`, the pattern-binder dec must NOT fire — the caller
-    /// still holds a reference and dec'ing the pattern-binder would
-    /// fragment the caller's structure.
+    /// scrutinee resolves to a fn-param whose mode is `Borrow`, the
+    /// pattern-binder dec must NOT fire — the caller still holds a
+    /// reference and dec'ing the pattern-binder would fragment the
+    /// caller's structure.
     ///
     /// Symmetric with the Iter B gate at fn return (`emit_fn`'s Own-
-    /// param dec): both sites must check the param-mode signal before
-    /// dec'ing, because Implicit and Borrow do not carry the "caller
-    /// handed off ownership" signal that makes the dec safe.
+    /// param dec): both sites check the param-mode signal before
+    /// dec'ing, because `Borrow` does not carry the "caller handed off
+    /// ownership" signal that makes the dec safe.
     current_param_modes: BTreeMap<String, ParamMode>,
     /// Per-fn map of name → (alloca SSA name, AIL element type) for
     /// alloca-resident loop binders. Populated on entry to a
@@ -973,6 +990,7 @@ impl<'a> Emitter<'a> {
         module_ctor_index: &'a BTreeMap<String, BTreeMap<String, CtorRef>>,
         module_consts: &'a BTreeMap<String, BTreeMap<String, ConstDef>>,
         import_map: BTreeMap<String, String>,
+        drop_monos: &'a dropmono::DropAdtMeta,
         alloc: AllocStrategy,
     ) -> Self {
         let mut types: BTreeMap<String, Vec<CtorInfo>> = BTreeMap::new();
@@ -1030,6 +1048,7 @@ impl<'a> Emitter<'a> {
             str_counter: 0,
             module_user_fns,
             import_map,
+            drop_monos,
             types,
             module_ctor_index,
             module_consts,
@@ -1293,10 +1312,9 @@ impl<'a> Emitter<'a> {
     fn emit_fn(&mut self, f: &FnDef, body: Option<&MTerm>) -> Result<()> {
         // also lift `param_modes` out of the fn type. The
         // fn-return Own-param dec emission below consults it to decide
-        // which params get a drop call before `ret`. `Implicit`
-        // entries (legacy / unannotated) and `Borrow` entries are
-        // skipped — only `Own` carries the static "caller handed off
-        // ownership" signal.
+        // which params get a drop call before `ret`. `Borrow` entries
+        // are skipped — only `Own` carries the static "caller handed
+        // off ownership" signal.
         let (param_tys, ret_ty, param_modes) = match &f.ty {
             Type::Fn {
                 params,
@@ -1339,7 +1357,10 @@ impl<'a> Emitter<'a> {
         self.pending_entry_allocas.clear();
         self.entry_block_end_marker = None;
         for (i, pname) in f.params.iter().enumerate() {
-            let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
+            // Codegen-synthesised fn-defs (lambda thunks, local-rec
+            // lifts) may carry an empty `param_modes`; fall back to
+            // `Own` (the synthesis default) rather than index-panic.
+            let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Own);
             self.current_param_modes.insert(pname.clone(), mode);
         }
         // run escape analysis over the fn body. The result
@@ -1469,11 +1490,10 @@ impl<'a> Emitter<'a> {
             //     the caller's frame; caller dec's, not us),
             //   - the current block is still open.
             //
-            // `Implicit`-mode params do NOT get this dec: they have
-            // no static "caller handed off ownership" signal —
-            // emitting a dec here might double-dec a value the caller
-            // also dec's. `Borrow`-mode params definitely don't get
-            // dec'd (the caller still owns them).
+            // `Borrow`-mode params do NOT get dec'd: the caller still
+            // owns them, so there is no caller-handed-off-ownership
+            // signal and a dec here would fragment the caller's
+            // structure.
             //
             // Closes the 18c.3/18c.4 carve-out: "fn parameters still
             // don't get dec'd at fn return — the caller-handed-off-
@@ -1490,7 +1510,7 @@ impl<'a> Emitter<'a> {
                     if plty != "ptr" {
                         continue;
                     }
-                    let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
+                    let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Own);
                     if !matches!(mode, ParamMode::Own) {
                         continue;
                     }
@@ -1812,8 +1832,8 @@ impl<'a> Emitter<'a> {
                 // If `value` is a `Term::Var` referencing a name in
                 // `current_param_modes`, the let-binder inherits that
                 // mode for the duration of the body. Without this,
-                // `(let a t (match a ...))` where `t` is an Implicit
-                // / Borrow-mode param defeats the
+                // `(let a t (match a ...))` where `t` is a
+                // `Borrow`-mode param defeats the
                 // `scrutinee_is_owned` gate in `lower_match` (the
                 // gate looks up `a` in `current_param_modes`, misses,
                 // and defaults to "owned" — Iter A then dec's
@@ -2690,8 +2710,7 @@ impl<'a> Emitter<'a> {
         //     alias whose owner is some other binder and is dropped
         //     there, never here;
         //   - the matching callee param mode is `Borrow` — `Own` slots
-        //     consume the arg (the callee dec's it), `Implicit` is the
-        //     back-compat lane that carries no transfer signal;
+        //     consume the arg (the callee dec's it);
         //   - the dropped SSA is never the call result `dst` (an input
         //     argument SSA is always distinct from the freshly-minted
         //     result SSA), so this can never dec a value that flows out
@@ -2702,7 +2721,7 @@ impl<'a> Emitter<'a> {
             // `param_modes`), so the borrow-slot test reads it directly
             // — no re-lookup of the callee's signature from a codegen
             // sig table. `Borrow` slots borrow the arg, so an Own-ret
-            // heap temp landing in one is dropped here; `Own`/`Implicit`
+            // heap temp landing in one is dropped here; `Own`
             // slots consume the arg (the callee dec's it).
             for (arg, (arg_ssa, arg_ty)) in args.iter().zip(compiled_args.iter()) {
                 let is_borrow_slot = matches!(arg.mode, Mode::Borrow);
@@ -3168,7 +3187,7 @@ mod tests {
                         ret: Box::new(Type::int()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec!["a".into(), "b".into()],
                     body: Term::App {
@@ -3192,7 +3211,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec![],
                     body: Term::Lit { lit: Literal::Unit },
@@ -3238,7 +3257,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Lit {
@@ -3313,7 +3332,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec![],
                     body: Term::Lit { lit: Literal::Unit },
@@ -3386,7 +3405,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec![],
                     body: Term::Lit { lit: Literal::Unit },
@@ -3418,7 +3437,7 @@ mod tests {
                     ret: Box::new(ret_ty),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body,
@@ -3491,7 +3510,7 @@ mod tests {
                 name: name.into(),
                 ty: Type::Fn {
                     params: vec![], ret: Box::new(ret_ty), effects: vec![],
-                    param_modes: vec![], ret_mode: ParamMode::Implicit,
+                    param_modes: vec![], ret_mode: ParamMode::Own,
                 },
                 params: vec![], body, suppress: vec![], doc: None,
             export: None,
@@ -3543,7 +3562,7 @@ mod tests {
                 name: name.into(),
                 ty: Type::Fn {
                     params: vec![], ret: Box::new(Type::float()), effects: vec![],
-                    param_modes: vec![], ret_mode: ParamMode::Implicit,
+                    param_modes: vec![], ret_mode: ParamMode::Own,
                 },
                 params: vec![], body, suppress: vec![], doc: None,
             export: None,
@@ -3553,7 +3572,7 @@ mod tests {
             name: "main".into(),
             ty: Type::Fn {
                 params: vec![], ret: Box::new(Type::unit()), effects: vec![],
-                param_modes: vec![], ret_mode: ParamMode::Implicit,
+                param_modes: vec![], ret_mode: ParamMode::Own,
             },
             params: vec![], body: Term::Lit { lit: Literal::Unit },
             suppress: vec![], doc: None,
@@ -3598,7 +3617,7 @@ mod tests {
                         ret: Box::new(Type::bool_()),
                         effects: vec![],
                         param_modes: vec![ParamMode::Borrow, ParamMode::Borrow],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec!["x".into(), "y".into()],
                     // Body is a placeholder — the intercept must
@@ -3616,7 +3635,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec![],
                     body: Term::Lit { lit: Literal::Unit },
@@ -3661,7 +3680,7 @@ mod tests {
                         ret: Box::new(Type::bool_()),
                         effects: vec![],
                         param_modes: vec![ParamMode::Borrow, ParamMode::Borrow],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec!["x".into(), "y".into()],
                     body: Term::Lit { lit: Literal::Bool { value: false } },
@@ -3676,7 +3695,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec![],
                     body: Term::Lit { lit: Literal::Unit },
@@ -3725,7 +3744,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Lit { lit: Literal::Unit },
@@ -3824,8 +3843,11 @@ mod tests {
                 params: vec![param_ail_ty.clone(), param_ail_ty.clone()],
                 ret: Box::new(Type::Con { name: "Ordering".into(), args: vec![] }),
                 effects: vec![],
-                param_modes: vec![ParamMode::Borrow, ParamMode::Borrow],
-                ret_mode: ParamMode::Implicit,
+                // value-typed params (Int/Bool) cannot be `(borrow V)` —
+                // the cutover's `borrow-over-value` reject forbids it; a
+                // value type is copied, so `own` is the only legal mode.
+                param_modes: vec![ParamMode::Own, ParamMode::Own],
+                ret_mode: ParamMode::Own,
             },
             params: vec!["x".into(), "y".into()],
             // placeholder body; the `compare__<T>` intercept overrides
@@ -3849,7 +3871,7 @@ mod tests {
                 ret: Box::new(Type::unit()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec![],
             body: Term::Lit { lit: Literal::Unit },
@@ -3894,7 +3916,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec![],
                     body: Term::Lit { lit: Literal::Unit },
@@ -3930,7 +3952,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec!["IO".into()],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Do {
@@ -3972,7 +3994,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec!["IO".into()],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Do {
@@ -4033,7 +4055,7 @@ mod tests {
                         ret: Box::new(Type::bool_()),
                         effects: vec![],
                         param_modes: vec![ParamMode::Borrow, ParamMode::Borrow],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec!["x".into(), "y".into()],
                     body: Term::Lit { lit: Literal::Bool { value: false } },
@@ -4048,7 +4070,7 @@ mod tests {
                         ret: Box::new(Type::unit()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec![],
                     body: Term::Lit { lit: Literal::Unit },
@@ -4129,7 +4151,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec!["IO".into()],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Do {
@@ -4170,7 +4192,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec!["IO".into()],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Do {
@@ -4212,7 +4234,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec!["IO".into()],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Do {
@@ -4254,7 +4276,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec!["IO".into()],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Do {
@@ -4296,7 +4318,7 @@ mod tests {
                     ret: Box::new(Type::unit()),
                     effects: vec!["IO".into()],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Do {

crates/ailang-codegen/src/match_lower.rs

@@ -256,8 +256,16 @@ impl<'a> Emitter<'a> {
         } else {
             cref.ail_fields.clone()
         };
-        let expected_llvm_tys: Vec<String> = if cref.type_vars.is_empty() {
-            cref.fields.clone()
+        // leg C: the body-ctor field substitution (var -> concrete
+        // arg). Empty for monomorphic ADTs; for a polymorphic body ctor
+        // it pins each declared field var to the instantiation arg
+        // derived from the body args' types. Used both for the expected
+        // LLVM field types AND (further down) for the reuse-arm per-field
+        // dec, so a value-type field is recognised as inline (skipped)
+        // and a heap field routes through its own per-monomorph drop
+        // symbol.
+        let field_subst: BTreeMap<String, Type> = if cref.type_vars.is_empty() {
+            BTreeMap::new()
         } else {
             let arg_ail_tys: Vec<Type> = body_args
                 .iter()
@@ -269,9 +277,14 @@ impl<'a> Emitter<'a> {
             for (exp, actual) in qualified_ail_fields.iter().zip(arg_ail_tys.iter()) {
                 unify_for_subst(exp, actual, &var_set, &mut subst)?;
             }
+            subst
+        };
+        let expected_llvm_tys: Vec<String> = if cref.type_vars.is_empty() {
+            cref.fields.clone()
+        } else {
             qualified_ail_fields
                 .iter()
-                .map(|f| llvm_type(&apply_subst_to_type(f, &subst)))
+                .map(|f| llvm_type(&apply_subst_to_type(f, &field_subst)))
                 .collect::<Result<_>>()?
         };
         // (18d.2 currently does not dec old fields in the reuse
@@ -353,8 +366,12 @@ impl<'a> Emitter<'a> {
             .as_ref()
             .and_then(|sb| self.moved_slots.get(sb).cloned())
             .unwrap_or_default();
-        for (idx, fty_ail) in qualified_ail_fields.iter().enumerate() {
-            let lty = llvm_type(fty_ail).unwrap_or_else(|_| "ptr".into());
+        for (idx, fty_decl) in qualified_ail_fields.iter().enumerate() {
+            // leg C: substitute to the body-ctor's monomorph so a
+            // value-type slot is skipped (inline scalar) and a heap slot
+            // dec's through its own per-monomorph drop symbol.
+            let fty_ail = apply_subst_to_type(fty_decl, &field_subst);
+            let lty = llvm_type(&fty_ail).unwrap_or_else(|_| "ptr".into());
             if lty != "ptr" {
                 continue;
             }
@@ -370,7 +387,7 @@ impl<'a> Emitter<'a> {
             self.body.push_str(&format!(
                 "  {v} = load ptr, ptr {addr}, align 8\n"
             ));
-            let drop_call = self.field_drop_call(fty_ail);
+            let drop_call = self.field_drop_call(&fty_ail);
             self.body.push_str(&format!(
                 "  call void @{drop_call}(ptr {v})\n"
             ));

crates/ailang-codegen/src/subst.rs

@@ -170,13 +170,37 @@ pub(crate) fn apply_subst_to_type(t: &Type, subst: &BTreeMap<String, Type>) -> T
             name: name.clone(),
             args: args.iter().map(|a| apply_subst_to_type(a, subst)).collect(),
         },
-        Type::Fn { params, ret, effects, param_modes, ret_mode } => Type::Fn {
-            params: params.iter().map(|p| apply_subst_to_type(p, subst)).collect(),
-            ret: Box::new(apply_subst_to_type(ret, subst)),
+        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: param_modes.clone(),
-            ret_mode: *ret_mode,
-        },
+                param_modes: new_param_modes,
+                ret_mode: new_ret_mode,
+            }
+        }
         Type::Forall { vars, constraints, body } => {
             // Inner forall shadows: don't substitute re-bound names.
             let inner: BTreeMap<String, Type> = subst

crates/ailang-core/src/ast.rs

@@ -770,17 +770,14 @@ pub enum Type {
     /// `(own T)` wrappers from the surface form. They are metadata
     /// on `Type::Fn`, not new `Type` variants — so unification,
     /// occurs, apply, and every other `Type` match-arm keeps working
-    /// unchanged. `param_modes` is omitted from canonical JSON when
-    /// every entry is `Implicit`; `ret_mode` is omitted when it is
-    /// `Implicit`, so pre-mode-annotation fixtures hash
-    /// bit-identically. Full contract in
+    /// unchanged. Both are always present (one mode per slot,
+    /// `param_modes.len() == params.len()`); ownership has no default
+    /// (spec 0062). Full contract in
     /// `design/contracts/0008-memory-model.md`.
     Fn {
         params: Vec<Type>,
-        #[serde(default, skip_serializing_if = "all_implicit")]
         param_modes: Vec<ParamMode>,
         ret: Box<Type>,
-        #[serde(default, skip_serializing_if = "ParamMode::is_implicit")]
         ret_mode: ParamMode,
         #[serde(default)]
         effects: Vec<String>,
@@ -829,123 +826,37 @@ impl Type {
         Type::Con { name: "Float".into(), args: vec![] }
     }
 
-    /// Build a `Type::Fn` with all parameter modes set to
-    /// `ParamMode::Implicit` and `ret_mode` set to `Implicit`. This
-    /// is the form every typechecker / desugar / codegen site that
-    /// synthesises a fn-type should use, so that newly inferred
-    /// fn-types retain pre-mode-annotation canonical-JSON bytes.
-    pub fn fn_implicit(params: Vec<Type>, ret: Type, effects: Vec<String>) -> Type {
+    /// 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::Implicit; n],
+            param_modes: vec![ParamMode::Own; n],
             ret: Box::new(ret),
-            ret_mode: ParamMode::Implicit,
+            ret_mode: ParamMode::Own,
             effects,
         }
     }
 }
 
-/// 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);
-        }
-    }
-}
-
 /// Per-parameter / return mode marker on a [`Type::Fn`]. Full
 /// contract lives in `design/contracts/0008-memory-model.md`.
-///
-/// `Implicit` is the legacy state for fn-types that were constructed
-/// before the borrow/own surface annotations existed. Semantically,
-/// `Implicit ≡ Own`; the distinction exists only so pre-annotation
-/// JSON fixtures continue to serialize without a `"mode"` wrapper
-/// and therefore keep their canonical-JSON hash.
-///
-/// `Own` and `Borrow` are author-asserted: the surface form
-/// `(own T)` / `(borrow T)` round-trips through this enum.
-#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
+/// 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 {
-    /// Unannotated / back-compat. Treated as `Own` by the typechecker.
-    #[default]
-    Implicit,
     /// `(own T)` — caller transfers ownership; callee consumes.
     Own,
     /// `(borrow T)` — caller retains ownership; callee may not consume.
     Borrow,
 }
 
-impl ParamMode {
-    /// Used by the `skip_serializing_if` predicate on
-    /// [`Type::Fn::ret_mode`].
-    pub fn is_implicit(&self) -> bool {
-        matches!(self, ParamMode::Implicit)
-    }
-}
-
-/// Serde helper for [`Type::Fn::param_modes`]. Returns `true` when
-/// every entry is [`ParamMode::Implicit`] (or when the list is
-/// empty), so canonical JSON omits the field for any fn-type without
-/// explicit `(borrow)` / `(own)` annotations and pre-annotation
-/// fixtures keep bit-identical hashes.
-fn all_implicit(modes: &[ParamMode]) -> bool {
-    modes.iter().all(|m| m.is_implicit())
-}
-
-/// Equality of [`ParamMode`] for the purposes of `Type` equality.
-/// `Implicit` and `Own` are treated as the same mode; `Borrow` is
-/// distinct. This keeps pre-annotation fixtures (whose fn-types
-/// serialize `Implicit`) compatible with newly-written fixtures
-/// that mark the same fn-type explicitly with `(own T)`.
-fn mode_eq(a: &ParamMode, b: &ParamMode) -> bool {
-    match (a, b) {
-        (ParamMode::Borrow, ParamMode::Borrow) => true,
-        (ParamMode::Borrow, _) | (_, ParamMode::Borrow) => false,
-        // Implicit and Own are interchangeable.
-        _ => true,
-    }
-}
-
-/// Equality of two `param_modes` slices, robust to the
-/// "elided when all-implicit" representation used by typechecker /
-/// desugar / codegen sites that construct fn-types with
-/// `param_modes: vec![]`. Both slices are normalised to "implicit
-/// padding to match the longer one"; equality then proceeds
-/// element-wise via [`mode_eq`].
-fn mode_slices_eq(a: &[ParamMode], b: &[ParamMode]) -> bool {
-    let n = a.len().max(b.len());
-    for i in 0..n {
-        let x = a.get(i).copied().unwrap_or(ParamMode::Implicit);
-        let y = b.get(i).copied().unwrap_or(ParamMode::Implicit);
-        if !mode_eq(&x, &y) {
-            return false;
-        }
-    }
-    true
-}
-
 impl PartialEq for Type {
     fn eq(&self, other: &Self) -> bool {
         match (self, other) {
@@ -971,8 +882,8 @@ impl PartialEq for Type {
             ) => {
                 ap == bp
                     && ar == br
-                    && mode_slices_eq(apm, bpm)
-                    && mode_eq(arm, brm)
+                    && apm == bpm
+                    && arm == brm
                     && {
                         let mut a = ae.clone();
                         let mut b = be.clone();

crates/ailang-core/src/desugar.rs

@@ -933,7 +933,7 @@ impl Desugarer {
                             ret: ret.clone(),
                             effects: effects.clone(),
                             param_modes: vec![],
-                            ret_mode: ParamMode::Implicit,
+                            ret_mode: ParamMode::Own,
                         }
                     }
                     Type::Forall { .. } => panic!(
@@ -1115,8 +1115,6 @@ impl Desugarer {
                 arms,
             };
         }
-        let s = self.fresh();
-        let s_var = Term::Var { name: s.clone() };
         // `default` is unreachable for valid programs (the
         // typechecker requires either a catch-all arm or exhaustive
         // ctor coverage). Use the polymorphic bottom builtin
@@ -1125,6 +1123,28 @@ impl Desugarer {
         // `Unit`-typed `_` arm to dominate it. Codegen lowers the
         // var to LLVM `unreachable`.
         let default = Term::Var { name: "__unreachable__".into() };
+        // When the scrutinee is ALREADY a bare `Term::Var` (a function
+        // param or an existing let-binder), do NOT introduce a fresh
+        // `Let $mp = <scrutinee>` rebind: reuse the binder directly as
+        // the chain scrutinee. The rebind is spurious here and, post-#55,
+        // harmful — walking the `Let` value in `Position::Consume` bumps
+        // the param's `consume_count` to 1, which trips the fn-return
+        // husk-free gate (`consume_count != 0` ⇒ skip) and relocates the
+        // outer-cell ownership onto the internal `$mp` binder the gate
+        // never inspects, leaking the moved-from outer cell. Reusing the
+        // binder keeps `consume_count == 0` and populates `moved_slots`
+        // exactly as the single-match case, so the existing gate fires
+        // unchanged (refs #55, examples/lit_pat_ctor_tail_drop.ail,
+        // examples/lit_pat_nil_scrutinee_drop.ail).
+        //
+        // A COMPOUND-expression scrutinee (not a bare Var) still needs
+        // the `$mp` rebind so it is evaluated once and shared across all
+        // chain arms rather than re-evaluated per arm.
+        if matches!(scrutinee, Term::Var { .. }) {
+            return self.build_chain(&scrutinee, &arms, &default);
+        }
+        let s = self.fresh();
+        let s_var = Term::Var { name: s.clone() };
         let chain = self.build_chain(&s_var, &arms, &default);
         Term::Let {
             name: s,
@@ -1136,16 +1156,109 @@ impl Desugarer {
     /// Recursively builds a chain of single-arm matches with a shared
     /// fall-through. Empty arms ⇒ `default`; otherwise the first arm
     /// is desugared with the rest of the chain as its fall-through.
+    ///
+    /// Consecutive arms whose head pattern is the *same* outer ctor
+    /// (same name + arity) are grouped into ONE [`Term::Match`] arm
+    /// that binds the ctor fields exactly once, then branches the
+    /// per-arm sub-patterns over those bound field vars. This is the
+    /// single-ownership-scope invariant the arm-close drop accounting
+    /// in `match_lower` relies on: a ctor's owned children are bound
+    /// (and therefore dropped) under one match scope per ctor, never
+    /// re-matched on the same scrutinee. Re-matching the same owned
+    /// scrutinee under a second ctor scope (the pre-fix lowering of a
+    /// lit sub-pattern's `else` branch) bound — and the post-#55
+    /// `Own`-param arm-close dropped — the same heap child twice
+    /// (double-free; refs #55, examples/lit_pat_ctor_tail_drop.ail).
     fn build_chain(&mut self, s_var: &Term, arms: &[Arm], default: &Term) -> Term {
         if arms.is_empty() {
             return default.clone();
         }
         let head = &arms[0];
+        // Detect a maximal run of consecutive arms sharing the head
+        // arm's outer ctor + arity. A run of length ≥ 1 of ctor arms
+        // is lowered as a single bind-once ctor-match; everything else
+        // (Wild / Var / Lit head) falls through to the per-arm path.
+        if let Pattern::Ctor { ctor, fields } = &head.pat {
+            let arity = fields.len();
+            let group_len = arms
+                .iter()
+                .take_while(|a| match &a.pat {
+                    Pattern::Ctor {
+                        ctor: c,
+                        fields: f,
+                    } => c == ctor && f.len() == arity,
+                    _ => false,
+                })
+                .count();
+            let group = &arms[..group_len];
+            let rest = &arms[group_len..];
+            let rest_chain = self.build_chain(s_var, rest, default);
+            return self.build_ctor_group(s_var, ctor, arity, group, rest_chain);
+        }
         let rest = &arms[1..];
         let fall_k = self.build_chain(s_var, rest, default);
         self.desugar_one_arm(s_var, head, fall_k)
     }
 
+    /// Lowers a run of consecutive arms that all match the same outer
+    /// ctor `ctor`/`arity` into a single [`Term::Match`] that binds the
+    /// ctor fields once. The bound field vars are threaded through each
+    /// arm's sub-patterns (via [`wrap_sub`](Self::wrap_sub)); the arms'
+    /// internal fall-throughs chain left-to-right, ending in
+    /// `rest_chain` (the arms after the group, which by construction
+    /// match a *different* ctor or are catch-alls). The single match's
+    /// wildcard arm also routes to `rest_chain`. No arm in the group
+    /// re-matches `s_var`, so the ctor's owned children live under
+    /// exactly one match scope.
+    fn build_ctor_group(
+        &mut self,
+        s_var: &Term,
+        ctor: &str,
+        arity: usize,
+        group: &[Arm],
+        rest_chain: Term,
+    ) -> Term {
+        let fresh_vars: Vec<String> = (0..arity).map(|_| self.fresh()).collect();
+        let flat_fields: Vec<Pattern> = fresh_vars
+            .iter()
+            .map(|n| Pattern::Var { name: n.clone() })
+            .collect();
+        // Build the group body inside-out: the last arm falls to
+        // `rest_chain`; each earlier arm falls to the next arm's body.
+        // Within an arm, fold the field sub-patterns right-to-left so
+        // the deepest field is matched first (matches the single-arm
+        // `desugar_one_arm` ordering).
+        let mut inner = rest_chain.clone();
+        for arm in group.iter().rev() {
+            let sub_fields = match &arm.pat {
+                Pattern::Ctor { fields, .. } => fields,
+                // `build_chain` only calls this with ctor arms.
+                _ => unreachable!("build_ctor_group requires ctor arms"),
+            };
+            let mut arm_body = arm.body.clone();
+            for (sub, fv) in sub_fields.iter().zip(fresh_vars.iter()).rev() {
+                arm_body = self.wrap_sub(fv, sub, arm_body, &inner);
+            }
+            inner = arm_body;
+        }
+        Term::Match {
+            scrutinee: Box::new(s_var.clone()),
+            arms: vec![
+                Arm {
+                    pat: Pattern::Ctor {
+                        ctor: ctor.to_string(),
+                        fields: flat_fields,
+                    },
+                    body: inner,
+                },
+                Arm {
+                    pat: Pattern::Wild,
+                    body: rest_chain,
+                },
+            ],
+        }
+    }
+
     /// Lowers one arm into a term. Wild/Var arms drop the chain (the
     /// arm matches everything); Lit and Ctor arms emit a `Term::Match`
     /// with the desugared head pattern as the first arm and a
@@ -1988,7 +2101,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec!["xs".into()],
                 body: body_match,
@@ -2046,7 +2159,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec!["xs".into()],
                 body: original.clone(),
@@ -2138,7 +2251,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["n".into()],
             body: Box::new(Term::Var { name: "n".into() }),
@@ -2164,7 +2277,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: fact_letrec_term(),
@@ -2228,7 +2341,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec!["n".into()],
                 // (let-rec helper (params x) (type Int -> Int)
@@ -2241,7 +2354,7 @@ mod tests {
                         ret: Box::new(Type::int()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec!["x".into()],
                     body: Box::new(Term::App {
@@ -2278,7 +2391,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             "lifted fn type should have capture appended; got {:?}",
             lifted.ty
@@ -2348,7 +2461,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["x".into()],
             body: Box::new(Term::App {
@@ -2377,7 +2490,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Let {
@@ -2451,7 +2564,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["z".into()],
             body: Box::new(Term::App {
@@ -2498,7 +2611,7 @@ mod tests {
                         ret: Box::new(Type::int()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec!["p".into()],
                     body: outer_body,
@@ -2548,7 +2661,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["x".into()],
             body: Box::new(Term::Let {
@@ -2578,7 +2691,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: letrec,
@@ -2611,7 +2724,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["x".into()],
             body: Box::new(Term::App {
@@ -2641,7 +2754,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: letrec,
@@ -2733,7 +2846,7 @@ mod tests {
                 ret: Box::new(Type::Var { name: "a".into() }),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["k".into()],
             // 2026-05-21 operator-routing-eq-ord: keep `==` here (vs
@@ -2786,7 +2899,7 @@ mod tests {
                         ret: Box::new(Type::Var { name: "a".into() }),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     }),
                 },
                 params: vec!["x".into()],
@@ -2862,7 +2975,7 @@ mod tests {
                 ret: Box::new(Type::Var { name: "a".into() }),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["k".into()],
             body: Box::new(Term::Var { name: "x".into() }),
@@ -2891,7 +3004,7 @@ mod tests {
                         ret: Box::new(Type::Var { name: "a".into() }),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     }),
                 },
                 params: vec!["x".into()],
@@ -2932,7 +3045,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["j".into()],
             body: Box::new(Term::App {
@@ -2953,7 +3066,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["i".into()],
             body: Box::new(inner),
@@ -2975,7 +3088,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: outer,
@@ -3011,7 +3124,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["j".into()],
             body: Box::new(Term::App {
@@ -3035,7 +3148,7 @@ mod tests {
                 ret: Box::new(Type::int()),
                 effects: vec![],
                 param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
             },
             params: vec!["i".into()],
             body: Box::new(inner),
@@ -3057,7 +3170,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: outer,
@@ -3189,7 +3302,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec!["n".into()],
                 body: body_match,
@@ -3207,15 +3320,15 @@ mod tests {
             !any_lit_pattern(body),
             "desugarer must remove every Pattern::Lit from the term tree; got: {body:#?}"
         );
-        // The desugar wraps the match in `let $mp_N = scrutinee in <chain>`,
-        // and the chain head must be a `Term::If` (the lit arm).
-        let chain = match body {
-            Term::Let { body, .. } => body.as_ref(),
-            other => panic!("expected outer Let from chain machinery, got {other:?}"),
-        };
+        // The scrutinee is a bare `Term::Var` (the param `n`), so the
+        // chain machinery reuses the binder directly without a spurious
+        // `let $mp_N = n` rebind (the rebind would bump the param's
+        // `consume_count` and break the fn-return husk-free gate; refs
+        // #55). The chain head is therefore the `Term::If` (the lit arm)
+        // sitting directly at the function body.
         assert!(
-            matches!(chain, Term::If { .. }),
-            "expected Term::If at the chain head, got {chain:?}"
+            matches!(body, Term::If { .. }),
+            "expected Term::If at the chain head, got {body:?}"
         );
     }
 
@@ -3264,7 +3377,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec!["xs".into()],
                 body: body_match,
@@ -3347,7 +3460,7 @@ mod tests {
                     ret: Box::new(Type::int()),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec!["n".into()],
                 body: body_match,
@@ -3361,13 +3474,11 @@ mod tests {
             Def::Fn(f) => &f.body,
             _ => unreachable!(),
         };
-        // Outer is `let $mp_N = scrutinee in <chain>`. The chain is
-        // `if (== sv 0) then 100 else if (== sv 1) then 200 else __unreachable__`.
-        let chain = match body {
-            Term::Let { body, .. } => body.as_ref(),
-            other => panic!("expected outer Let from chain machinery, got {other:?}"),
-        };
-        let inner_else = match chain {
+        // The scrutinee is a bare `Term::Var` (the param `n`), so there
+        // is no `let $mp_N = n` rebind (it would break the fn-return
+        // husk-free gate; refs #55). The body IS the chain directly:
+        // `if (== n 0) then 100 else if (== n 1) then 200 else __unreachable__`.
+        let inner_else = match body {
             Term::If { else_, .. } => else_.as_ref(),
             other => panic!("expected outer If, got {other:?}"),
         };

crates/ailang-core/src/pretty.rs

@@ -179,7 +179,7 @@ mod tests {
                         ret: Box::new(Type::int()),
                         effects: vec![],
                         param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                     },
                     params: vec!["a".into(), "b".into()],
                     body: Term::App {

crates/ailang-core/src/workspace.rs

@@ -1811,7 +1811,7 @@ mod tests {
             "defs": [{
                 "kind": "fn",
                 "name": "f",
-                "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_con }, "effects": [] },
+                "type": { "k": "fn", "params": [], "param_modes": [], "ret": { "k": "con", "name": type_con }, "ret_mode": "own", "effects": [] },
                 "params": [],
                 "body": { "t": "lit", "lit": { "kind": "unit" } }
             }],
@@ -1829,7 +1829,7 @@ mod tests {
             "defs": [
                 { "kind": "type", "name": type_name, "ctors": [] },
                 { "kind": "fn", "name": "f",
-                  "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_name }, "effects": [] },
+                  "type": { "k": "fn", "params": [], "param_modes": [], "ret": { "k": "con", "name": type_name }, "ret_mode": "own", "effects": [] },
                   "params": [],
                   "body": { "t": "lit", "lit": { "kind": "unit" } } }
             ],
@@ -1847,7 +1847,7 @@ mod tests {
             "defs": [{
                 "kind": "fn",
                 "name": "f",
-                "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_con }, "effects": [] },
+                "type": { "k": "fn", "params": [], "param_modes": [], "ret": { "k": "con", "name": type_con }, "ret_mode": "own", "effects": [] },
                 "params": [],
                 "body": { "t": "lit", "lit": { "kind": "unit" } }
             }],
@@ -1982,7 +1982,7 @@ mod tests {
             "defs": [{
                 "kind": "fn",
                 "name": "f",
-                "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] },
+                "type": { "k": "fn", "params": [], "param_modes": [], "ret": { "k": "con", "name": "Unit" }, "ret_mode": "own", "effects": [] },
                 "params": [],
                 "body": {
                     "t": "lam",
@@ -2026,7 +2026,7 @@ mod tests {
             "defs": [{
                 "kind": "fn",
                 "name": "f",
-                "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] },
+                "type": { "k": "fn", "params": [], "param_modes": [], "ret": { "k": "con", "name": "Unit" }, "ret_mode": "own", "effects": [] },
                 "params": [],
                 "body": {
                     "t": "ctor",
@@ -2173,8 +2173,8 @@ mod tests {
                         { "class": "other.MyEq", "type": { "k": "var", "name": "a" } }
                     ],
                     "body": {
-                        "k": "fn", "params": [{ "k": "var", "name": "a" }],
-                        "ret": { "k": "con", "name": "Unit" }, "effects": []
+                        "k": "fn", "params": [{ "k": "var", "name": "a" }], "param_modes": ["own"],
+                        "ret": { "k": "con", "name": "Unit" }, "ret_mode": "own", "effects": []
                     }
                 },
                 "params": ["x"],
@@ -2226,8 +2226,8 @@ mod tests {
                     "methods": [
                         { "name": "tshow",
                           "type": { "k": "fn",
-                                    "params": [{ "k": "var", "name": "a" }],
-                                    "ret": { "k": "con", "name": "Str" },
+                                    "params": [{ "k": "var", "name": "a" }], "param_modes": ["own"],
+                                    "ret": { "k": "con", "name": "Str" }, "ret_mode": "own",
                                     "effects": [] } }
                     ]
                 },
@@ -2326,9 +2326,9 @@ mod tests {
             }],
             body: Box::new(Type::Fn {
                 params: vec![Type::Var { name: "a".to_string() }],
-                param_modes: vec![],
+                param_modes: vec![crate::ast::ParamMode::Own],
                 ret: Box::new(Type::Var { name: "a".to_string() }),
-                ret_mode: Default::default(),
+                ret_mode: crate::ast::ParamMode::Own,
                 effects: vec![],
             }),
         };
@@ -2392,8 +2392,8 @@ mod tests {
                         ],
                         "body": {
                             "k": "fn",
-                            "params": [{ "k": "var", "name": "b" }],
-                            "ret": { "k": "con", "name": "Unit" },
+                            "params": [{ "k": "var", "name": "b" }], "param_modes": ["own"],
+                            "ret": { "k": "con", "name": "Unit" }, "ret_mode": "own",
                             "effects": []
                         }
                     }
@@ -2597,8 +2597,8 @@ mod tests {
                     ],
                     "body": {
                         "k": "fn",
-                        "params": [{ "k": "var", "name": "a" }],
-                        "ret": { "k": "con", "name": "Unit" },
+                        "params": [{ "k": "var", "name": "a" }], "param_modes": ["own"],
+                        "ret": { "k": "con", "name": "Unit" }, "ret_mode": "own",
                         "effects": []
                     }
                 },

crates/ailang-core/tests/design_index_pin.rs

@@ -119,14 +119,42 @@ fn every_contract_names_a_resolvable_ratifying_test() {
     for row in &contracts {
         // columns: id | consumer/lifetime | ratifying-test | link
         let rt = &row[2];
-        // take the path token (before any " (" note)
-        let path = rt.split(" (").next().unwrap_or(rt).trim();
+        // strip a trailing " (...)" note, then resolve every
+        // " + "-separated path segment. A dual ratifier such as
+        // "uniqueness.rs + linearity.rs (in-source mod tests)" names
+        // two real files — both must resolve, mirroring the
+        // dual-link handling in `link_target_exists` (clause-1).
+        // The second segment is a bare leafname relative to the
+        // first segment's directory.
+        let body = rt.split(" (").next().unwrap_or(rt).trim();
+        let segments: Vec<&str> = body.split(" + ").map(str::trim).collect();
+        let first = segments[0];
         assert!(
-            root().join(path).exists(),
+            root().join(first).exists(),
             "ratifying-test does not resolve to a real file: {:?} (contract {:?})",
-            path,
+            first,
             row[0]
         );
+        let base_dir = std::path::Path::new(first)
+            .parent()
+            .map(|p| p.to_path_buf())
+            .unwrap_or_default();
+        for seg in &segments[1..] {
+            // a later segment may be a full repo-relative path or a
+            // bare leafname rooted at the first segment's directory.
+            let resolved = if root().join(seg).exists() {
+                root().join(seg)
+            } else {
+                root().join(base_dir.join(seg))
+            };
+            assert!(
+                resolved.exists(),
+                "ratifying-test dual segment does not resolve to a real \
+                 file: {:?} (contract {:?})",
+                seg,
+                row[0]
+            );
+        }
     }
 }
 

crates/ailang-core/tests/design_schema_drift.rs

@@ -82,7 +82,7 @@ fn design_md_anchors_every_term_variant() {
             r#""t": "letrec""#,
             Term::LetRec {
                 name: "f".into(),
-                ty: Type::fn_implicit(vec![], Type::int(), vec![]),
+                ty: Type::fn_owned(vec![], Type::int(), vec![]),
                 params: vec![],
                 body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
                 in_term: Box::new(Term::Var { name: "f".into() }),
@@ -248,7 +248,7 @@ fn design_md_anchors_every_pattern_variant() {
 fn design_md_anchors_every_type_variant() {
     let exemplars: Vec<(&str, Type)> = vec![
         (r#""k": "con""#, Type::int()),
-        (r#""k": "fn""#, Type::fn_implicit(vec![], Type::unit(), vec![])),
+        (r#""k": "fn""#, Type::fn_owned(vec![], Type::unit(), vec![])),
         (r#""k": "var""#, Type::Var { name: "a".into() }),
         (
             r#""k": "forall""#,
@@ -313,7 +313,7 @@ fn design_md_anchors_every_def_kind() {
         name: "f".into(),
         doc: None,
         suppress: vec![],
-        ty: Type::fn_implicit(vec![], Type::int(), vec![]),
+        ty: Type::fn_owned(vec![], Type::int(), vec![]),
         params: vec![],
         body: Term::Lit { lit: Literal::Int { value: 0 } },
     export: None,
@@ -338,7 +338,7 @@ fn design_md_anchors_every_def_kind() {
         superclass: None,
         methods: vec![ClassMethod {
             name: "show".into(),
-            ty: Type::fn_implicit(vec![Type::Var { name: "a".into() }], Type::str_(), vec![]),
+            ty: Type::fn_owned(vec![Type::Var { name: "a".into() }], Type::str_(), vec![]),
             default: None,
         }],
         doc: None,
@@ -378,18 +378,16 @@ fn design_md_anchors_every_def_kind() {
 
 /// Every `ParamMode` variant must have its serialized string form present
 /// in design/contracts/0002-data-model.md. The mode annotations are load-bearing for
-/// ownership checking; an LLM author must know all three forms.
+/// ownership checking; an LLM author must know both forms.
 #[test]
 fn design_md_anchors_every_parammode_variant() {
     let exemplars: Vec<(&str, ParamMode)> = vec![
-        (r#""implicit""#, ParamMode::Implicit),
         (r#""own""#, ParamMode::Own),
         (r#""borrow""#, ParamMode::Borrow),
     ];
 
     for (anchor, mode) in exemplars {
         let _: &'static str = match mode {
-            ParamMode::Implicit => "implicit",
             ParamMode::Own => "own",
             ParamMode::Borrow => "borrow",
         };
@@ -525,7 +523,7 @@ fn design_md_anchors_nested_struct_keys() {
     let _ = Suppress { code: "x".into(), because: "y".into() };
     let _ = ClassMethod {
         name: "m".into(),
-        ty: Type::fn_implicit(vec![], Type::int(), vec![]),
+        ty: Type::fn_owned(vec![], Type::int(), vec![]),
         default: None,
     };
     let _ = InstanceMethod {

crates/ailang-core/tests/embed_export_hash_stable.rs

@@ -21,7 +21,7 @@ fn fn_without_export_hash_is_unchanged() {
     // equal the value captured before the field existed.
     let def = Def::Fn(FnDef {
         name: "f".into(),
-        ty: Type::fn_implicit(vec![Type::int()], Type::int(), vec![]),
+        ty: Type::fn_owned(vec![Type::int()], Type::int(), vec![]),
         params: vec!["x".into()],
         body: Term::Var { name: "x".into() },
         doc: None,
@@ -29,7 +29,7 @@ fn fn_without_export_hash_is_unchanged() {
         export: None,
     });
     // GOLDEN: captured pre-field (Step 2) from `def_hash` on this shape.
-    let golden = "b4662aa70839f60b";
+    let golden = "8ce080ee897b3f80";
     assert_eq!(def_hash(&def), golden,
         "pre-M1 fn hash drifted — additive-field invariant violated");
 }

crates/ailang-core/tests/hash_pin.rs

@@ -31,8 +31,8 @@ fn sample_fn() -> Def {
             params: vec![Type::int(), Type::int()],
             ret: Box::new(Type::int()),
             effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
+            param_modes: vec![ParamMode::Own, ParamMode::Own],
+            ret_mode: ParamMode::Own,
         },
         params: vec!["a".into(), "b".into()],
         body: Term::App {
@@ -86,7 +86,7 @@ fn iter13a_schema_extension_preserves_pre_13a_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
+    assert_eq!(def_hash(sum_def), "19920ec4123d35d6");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
         .expect("examples/list.ail loads");
@@ -108,7 +108,7 @@ fn loop_recur_schema_extension_preserves_pre_loop_recur_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
+    assert_eq!(def_hash(sum_def), "19920ec4123d35d6");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
         .expect("examples/list.ail loads");
@@ -162,7 +162,7 @@ fn iter19b_schema_extension_preserves_pre_19b_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
+    assert_eq!(def_hash(sum_def), "19920ec4123d35d6");
 }
 
 /// adding `Def::Class` and `Def::Instance` must
@@ -177,7 +177,7 @@ fn iter22b1_schema_extension_preserves_pre_22b_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
+    assert_eq!(def_hash(sum_def), "19920ec4123d35d6");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
         .expect("examples/list.ail loads");
@@ -220,7 +220,7 @@ fn forall_without_constraints_hashes_bit_identical_to_pre_22b2() {
     let t = Type::Forall {
         vars: vec!["a".into()],
         constraints: vec![],
-        body: Box::new(Type::fn_implicit(
+        body: Box::new(Type::fn_owned(
             vec![Type::Var { name: "a".into() }],
             Type::Var { name: "a".into() },
             vec![],
@@ -254,7 +254,7 @@ fn ct4_migrated_fixtures_have_canonical_form_hashes() {
     // io/print_str no longer adds a trailing newline.
     assert_eq!(
         def_hash(main_def),
-        "8ed47b4062ce00f5",
+        "602d7a6d6ba72bc4",
         "ordering_match::main canonical hash must match captured post-fputs-swap value"
     );
 
@@ -272,7 +272,7 @@ fn ct4_migrated_fixtures_have_canonical_form_hashes() {
     assert_eq!(dup_classmod_mod.defs.len(), 1, "test_22b1_dup_classmod expected to have exactly 1 def (class TShow)");
     assert_eq!(
         def_hash(&dup_classmod_mod.defs[0]),
-        "b8bca96c2d09ed93",
+        "4ca71c7d8212c96a",
         "test_22b1_dup_classmod class TShow canonical hash; post-24.2 captured value"
     );
 }
@@ -286,7 +286,7 @@ fn ct4_unmigrated_fixtures_remain_bit_identical() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "25343a2e5927a257",
+    assert_eq!(def_hash(sum_def), "19920ec4123d35d6",
         "sum.sum hash drifted across canonical-form tightening — unexpected");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))

crates/ailang-core/tests/schema_coverage.rs

@@ -67,7 +67,6 @@ enum VariantTag {
     TypeVar,
     TypeForall,
     // ParamMode
-    ParamModeImplicit,
     ParamModeOwn,
     ParamModeBorrow,
 }
@@ -111,7 +110,6 @@ const EXPECTED_VARIANTS: &[VariantTag] = &[
     VariantTag::TypeFn,
     VariantTag::TypeVar,
     VariantTag::TypeForall,
-    VariantTag::ParamModeImplicit,
     VariantTag::ParamModeOwn,
     VariantTag::ParamModeBorrow,
 ];
@@ -341,9 +339,6 @@ fn visit_type(t: &Type, observed: &mut HashSet<VariantTag>) {
 
 fn visit_param_mode(m: &ParamMode, observed: &mut HashSet<VariantTag>) {
     match m {
-        ParamMode::Implicit => {
-            observed.insert(VariantTag::ParamModeImplicit);
-        }
         ParamMode::Own => {
             observed.insert(VariantTag::ParamModeOwn);
         }
@@ -364,6 +359,17 @@ fn examples_dir() -> PathBuf {
     crate_dir.parent().unwrap().parent().unwrap().join("examples")
 }
 
+/// Fixtures that intentionally do NOT parse — the `#55` cutover
+/// reject corpus. Negative fixtures whose whole point is that the
+/// parser rejects them, so they have no AST to scan for variant
+/// coverage and the scan must skip them. Mirrors the same list in
+/// `crates/ail/tests/roundtrip_cli.rs`.
+///
+/// - `bare_slot_reject.ail`: a bare fn-type slot with no mode. The
+///   binary-ParamMode parser rejects it ("fn-type slot requires a
+///   mode: write (own T) or (borrow T)").
+const NON_PARSEABLE_FIXTURES: &[&str] = &["bare_slot_reject.ail"];
+
 fn list_ail_fixtures() -> Vec<PathBuf> {
     let dir = examples_dir();
     let mut paths: Vec<PathBuf> = std::fs::read_dir(&dir)
@@ -373,7 +379,7 @@ fn list_ail_fixtures() -> Vec<PathBuf> {
         .filter(|p| {
             p.file_name()
                 .and_then(|n| n.to_str())
-                .map(|n| n.ends_with(".ail"))
+                .map(|n| n.ends_with(".ail") && !NON_PARSEABLE_FIXTURES.contains(&n))
                 .unwrap_or(false)
         })
         .collect();

crates/ailang-core/tests/spec_drift.rs

@@ -49,7 +49,7 @@ fn spec_mentions_every_term_variant() {
             "(let-rec",
             Term::LetRec {
                 name: "f".into(),
-                ty: Type::fn_implicit(vec![], Type::int(), vec![]),
+                ty: Type::fn_owned(vec![], Type::int(), vec![]),
                 params: vec![],
                 body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
                 in_term: Box::new(Term::Var { name: "f".into() }),
@@ -207,7 +207,7 @@ fn spec_mentions_every_type_variant() {
         ("(con ", Type::int()),
         (
             "(fn-type",
-            Type::fn_implicit(vec![], Type::unit(), vec![]),
+            Type::fn_owned(vec![], Type::unit(), vec![]),
         ),
         (
             "TYVAR-NAME",
@@ -271,7 +271,7 @@ fn spec_mentions_every_def_kind() {
         name: "f".into(),
         doc: None,
         suppress: vec![],
-        ty: Type::fn_implicit(vec![], Type::int(), vec![]),
+        ty: Type::fn_owned(vec![], Type::int(), vec![]),
         params: vec![],
         body: Term::Lit { lit: Literal::Int { value: 0 } },
     export: None,

crates/ailang-core/tests/workspace_kernel.rs

@@ -48,7 +48,7 @@ fn kernel_tier_module_auto_imports_without_explicit_import() {
             "(module bridge\n",
             "  (import k_mod)\n",
             "  (fn anchor\n",
-            "    (type (forall (vars a) (fn-type (params (con KT a)) (ret (con Unit)))))\n",
+            "    (type (forall (vars a) (fn-type (params (own (con KT a))) (ret (own (con Unit))))))\n",
             "    (params k) (body unit)))\n",
         ),
     );
@@ -61,7 +61,7 @@ fn kernel_tier_module_auto_imports_without_explicit_import() {
             "(module consumer\n",
             "  (import bridge)\n",
             "  (fn use_kt\n",
-            "    (type (forall (vars a) (fn-type (params (con KT a)) (ret (con Unit)))))\n",
+            "    (type (forall (vars a) (fn-type (params (own (con KT a))) (ret (own (con Unit))))))\n",
             "    (params k) (body unit)))\n",
         ),
     );
@@ -106,7 +106,7 @@ fn two_kernel_tier_modules_coload() {
             "  (import k_a)\n",
             "  (import k_b)\n",
             "  (fn anchor\n",
-            "    (type (fn-type (params (con A) (con B)) (ret (con Unit))))\n",
+            "    (type (fn-type (params (own (con A)) (own (con B))) (ret (own (con Unit)))))\n",
             "    (params a b) (body unit)))\n",
         ),
     );
@@ -117,7 +117,7 @@ fn two_kernel_tier_modules_coload() {
             "(module consumer\n",
             "  (import bridge)\n",
             "  (fn use_ab\n",
-            "    (type (fn-type (params (con A) (con B)) (ret (con Unit))))\n",
+            "    (type (fn-type (params (own (con A)) (own (con B))) (ret (own (con Unit)))))\n",
             "    (params a b) (body unit)))\n",
         ),
     );
@@ -151,7 +151,7 @@ fn explicit_import_takes_precedence_over_auto_import() {
             "(module consumer\n",
             "  (import k_mod)\n",
             "  (fn use_kt\n",
-            "    (type (fn-type (params (con KT)) (ret (con Unit))))\n",
+            "    (type (fn-type (params (own (con KT))) (ret (own (con Unit)))))\n",
             "    (params k) (body unit)))\n",
         ),
     );

crates/ailang-kernel/src/raw_buf/source.ail

@@ -6,21 +6,21 @@
     (param-in (a Int Float Bool)))
   (fn new
     (doc "Allocate an uninitialised RawBuf of capacity n. Compiler-supplied (intrinsic) body; codegen intercept RawBuf_new__<T> emits @ailang_rc_alloc plus the i64 size header. Element bytes are uninitialised; caller must set before get.")
-    (type (forall (vars a) (fn-type (params (con Int)) (ret (own (con RawBuf a))))))
+    (type (forall (vars a) (fn-type (params (own (con Int))) (ret (own (con RawBuf a))))))
     (params n)
     (intrinsic))
   (fn get
     (doc "Indexed read. UB if i >= (size b); caller checks bounds via size. Compiler-supplied (intrinsic) body; codegen intercept RawBuf_get__<T> emits getelementptr plus load.")
-    (type (forall (vars a) (fn-type (params (borrow (con RawBuf a)) (con Int)) (ret a))))
+    (type (forall (vars a) (fn-type (params (borrow (con RawBuf a)) (own (con Int))) (ret (own a)))))
     (params b i)
     (intrinsic))
   (fn set
     (doc "Indexed write. Linear: own in, own out. Under uniqueness in-place; under shared copy-on-write (Issue #22). Compiler-supplied (intrinsic) body; codegen intercept RawBuf_set__<T> emits getelementptr plus store.")
-    (type (forall (vars a) (fn-type (params (own (con RawBuf a)) (con Int) a) (ret (own (con RawBuf a))))))
+    (type (forall (vars a) (fn-type (params (own (con RawBuf a)) (own (con Int)) (own a)) (ret (own (con RawBuf a))))))
     (params b i v)
     (intrinsic))
   (fn size
     (doc "Element count. Compiler-supplied (intrinsic) body; codegen intercept RawBuf_size__<T> emits a single i64 load from the slab header.")
-    (type (forall (vars a) (fn-type (params (borrow (con RawBuf a))) (ret (con Int)))))
+    (type (forall (vars a) (fn-type (params (borrow (con RawBuf a))) (ret (own (con Int))))))
     (params b)
     (intrinsic)))

crates/ailang-prose/src/lib.rs

@@ -298,7 +298,7 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize, owning_module: &str)
             let mode = param_modes
                 .get(i)
                 .copied()
-                .unwrap_or(ParamMode::Implicit);
+                .unwrap_or(ParamMode::Own);
             write_mode_type(out, ty, mode, owning_module);
         }
         out.push_str(") -> ");
@@ -384,7 +384,7 @@ fn write_class_method(out: &mut String, m: &ClassMethod, level: usize, owning_mo
                 out.push_str(&format!("x{i}"));
             }
             out.push_str(": ");
-            let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
+            let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Own);
             write_mode_type(out, p, mode, owning_module);
         }
         out.push_str(") -> ");
@@ -453,7 +453,6 @@ fn write_instance_method(out: &mut String, m: &InstanceMethod, level: usize, own
 
 fn write_mode_type(out: &mut String, t: &Type, mode: ParamMode, owning_module: &str) {
     match mode {
-        ParamMode::Implicit => write_type(out, t, owning_module),
         ParamMode::Own => {
             out.push_str("own ");
             write_type(out, t, owning_module);
@@ -505,7 +504,7 @@ fn write_type(out: &mut String, t: &Type, owning_module: &str) {
                 let mode = param_modes
                     .get(i)
                     .copied()
-                    .unwrap_or(ParamMode::Implicit);
+                    .unwrap_or(ParamMode::Own);
                 // In a bare `Type::Fn` outside a fn signature we have no
                 // parameter names, so render `mode T` only (no `name:`).
                 write_mode_type(out, p, mode, owning_module);
@@ -738,7 +737,7 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow
                     let mode = param_modes
                         .get(i)
                         .copied()
-                        .unwrap_or(ParamMode::Implicit);
+                        .unwrap_or(ParamMode::Own);
                     write_mode_type(out, pty, mode, owning_module);
                 }
                 out.push_str(") -> ");
@@ -1749,14 +1748,14 @@ mod tests {
 
     #[test]
     fn type_fn_no_modes_no_effects() {
-        let t = Type::fn_implicit(vec![Type::int()], Type::int(), vec![]);
-        assert_eq!(render_type(&t), "(Int) -> Int");
+        let t = Type::fn_owned(vec![Type::int()], Type::int(), vec![]);
+        assert_eq!(render_type(&t), "(own Int) -> own Int");
     }
 
     #[test]
     fn type_fn_with_effects() {
-        let t = Type::fn_implicit(vec![], Type::unit(), vec!["IO".into()]);
-        assert_eq!(render_type(&t), "() -> Unit with IO");
+        let t = Type::fn_owned(vec![], Type::unit(), vec!["IO".into()]);
+        assert_eq!(render_type(&t), "() -> own Unit with IO");
     }
 
     #[test]
@@ -1794,7 +1793,7 @@ mod tests {
                 }],
                 param_modes: vec![ParamMode::Own],
                 ret: Box::new(Type::int()),
-                ret_mode: ParamMode::Implicit,
+                ret_mode: ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["xs".into()],
@@ -1806,14 +1805,14 @@ mod tests {
         let mut out = String::new();
         write_fn_def(&mut out, &fd, 0, "");
         assert!(out.contains("xs: own IntList"), "got:\n{out}");
-        assert!(out.contains(") -> Int "), "got:\n{out}");
+        assert!(out.contains(") -> own Int "), "got:\n{out}");
     }
 
     #[test]
     fn fn_def_with_effects_appends_with_clause() {
         let fd = FnDef {
             name: "main".into(),
-            ty: Type::fn_implicit(vec![], Type::unit(), vec!["IO".into()]),
+            ty: Type::fn_owned(vec![], Type::unit(), vec!["IO".into()]),
             params: vec![],
             body: Term::Lit { lit: Literal::Unit },
             suppress: vec![],
@@ -1822,7 +1821,7 @@ mod tests {
         };
         let mut out = String::new();
         write_fn_def(&mut out, &fd, 0, "");
-        assert!(out.contains("() -> Unit with IO {"), "got:\n{out}");
+        assert!(out.contains("() -> own Unit with IO {"), "got:\n{out}");
     }
 
     /// a FnDef with a single `Suppress` entry renders the
@@ -1841,7 +1840,7 @@ mod tests {
                 }],
                 param_modes: vec![ailang_core::ast::ParamMode::Own],
                 ret: Box::new(Type::int()),
-                ret_mode: ailang_core::ast::ParamMode::Implicit,
+                ret_mode: ailang_core::ast::ParamMode::Own,
                 effects: vec![],
             },
             params: vec!["xs".into()],
@@ -1866,7 +1865,7 @@ mod tests {
         assert_eq!(lines[1], "/// Take ownership.", "doc line should follow; got:\n{out}");
         // Fn signature follows the doc.
         assert!(
-            out.contains("fn head_or_zero(xs: own IntList) -> Int"),
+            out.contains("fn head_or_zero(xs: own IntList) -> own Int"),
             "fn signature should follow; got:\n{out}"
         );
     }
@@ -1878,7 +1877,7 @@ mod tests {
     fn fn_def_renders_multiple_suppress_in_order() {
         let fd = FnDef {
             name: "f".into(),
-            ty: Type::fn_implicit(vec![], Type::int(), vec![]),
+            ty: Type::fn_owned(vec![], Type::int(), vec![]),
             params: vec![],
             body: Term::Lit { lit: Literal::Int { value: 0 } },
             suppress: vec![
@@ -1910,7 +1909,7 @@ mod tests {
     fn fn_def_with_empty_suppress_emits_no_suppress_lines() {
         let fd = FnDef {
             name: "f".into(),
-            ty: Type::fn_implicit(vec![], Type::int(), vec![]),
+            ty: Type::fn_owned(vec![], Type::int(), vec![]),
             params: vec![],
             body: Term::Lit { lit: Literal::Int { value: 0 } },
             suppress: vec![],
@@ -2345,7 +2344,7 @@ mod tests {
                     }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Ctor {
@@ -2361,7 +2360,7 @@ mod tests {
 
         let prose = module_to_prose(&m);
         assert!(
-            prose.contains("-> Ordering"),
+            prose.contains("-> own Ordering"),
             "expected bare `Ordering` in fn return type (owner == file's \
              module); got prose:\n{}",
             prose
@@ -2394,7 +2393,7 @@ mod tests {
                     }),
                     effects: vec![],
                     param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
+                    ret_mode: ParamMode::Own,
                 },
                 params: vec![],
                 body: Term::Ctor {

crates/ailang-surface/src/parse.rs

@@ -1177,26 +1177,18 @@ impl<'a> Parser<'a> {
             effects = self.parse_effects_clause()?;
         }
         self.expect_rparen("fn-type")?;
-        // If every entry is Implicit, store as `vec![]` so canonical
-        // JSON serialisation omits the field — preserves pre-18a
-        // hashes for any fixture that still uses bare types.
-        let stored_modes = if param_modes.iter().all(|m| matches!(m, ParamMode::Implicit)) {
-            Vec::new()
-        } else {
-            param_modes
-        };
         Ok(Type::Fn {
             params,
             ret: Box::new(ret),
             effects,
-            param_modes: stored_modes,
+            param_modes,
             ret_mode,
         })
     }
 
-    /// parse one fn-type slot — a type, optionally wrapped
-    /// in `(borrow T)` or `(own T)`. The mode is `Implicit` for a
-    /// bare type, `Borrow` for `(borrow T)`, `Own` for `(own T)`.
+    /// parse one fn-type slot — a type wrapped in `(borrow T)` or
+    /// `(own T)`. A bare type carries no mode and is rejected
+    /// (spec 0062): every slot must declare its ownership.
     fn parse_param_with_mode(&mut self) -> Result<(Type, ParamMode), ParseError> {
         if let Some(head) = self.peek_head_ident() {
             match head {
@@ -1217,8 +1209,12 @@ impl<'a> Parser<'a> {
                 _ => {}
             }
         }
-        let t = self.parse_type()?;
-        Ok((t, ParamMode::Implicit))
+        let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
+        Err(ParseError::Production {
+            production: "fn-type-slot",
+            message: "fn-type slot requires a mode: write (own T) or (borrow T)".into(),
+            pos,
+        })
     }
 
     fn parse_effects_clause(&mut self) -> Result<Vec<String>, ParseError> {
@@ -1942,7 +1938,7 @@ mod tests {
             r#"
             (module hello
               (fn main
-                (type (fn-type (params) (ret (con Unit)) (effects IO)))
+                (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
                 (params)
                 (body (do io/print_str "Hello, AILang."))))
             "#,
@@ -1958,7 +1954,7 @@ mod tests {
             r#"
             (module m
               (fn id
-                (type (fn-type (params (con Int)) (ret (con Int))))
+                (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
                 (params x)
                 (body x)))
             "#,
@@ -1969,9 +1965,8 @@ mod tests {
 
     /// `(borrow T)` and `(own T)` wrappers in fn-type
     /// param/ret slots round-trip into [`ParamMode::Borrow`] /
-    /// [`ParamMode::Own`] on `Type::Fn`. A bare type stays
-    /// [`ParamMode::Implicit`] (and its mode is elided from the
-    /// canonical form).
+    /// [`ParamMode::Own`] on `Type::Fn`. A bare slot is a parse
+    /// error (spec 0062): every slot carries an explicit mode.
     #[test]
     fn parses_borrow_and_own_modes_on_fn_type_slots() {
         let m = parse(
@@ -1979,7 +1974,7 @@ mod tests {
             (module m
               (fn f
                 (type (fn-type
-                        (params (borrow (con Int)) (con Bool))
+                        (params (borrow (con Int)) (own (con Bool)))
                         (ret (own (con Int)))))
                 (params x y)
                 (body x)))
@@ -1994,8 +1989,8 @@ mod tests {
             Type::Fn { param_modes, ret_mode, .. } => {
                 assert_eq!(
                     param_modes,
-                    &vec![ParamMode::Borrow, ParamMode::Implicit],
-                    "first param parsed as `(borrow ...)`, second as bare"
+                    &vec![ParamMode::Borrow, ParamMode::Own],
+                    "first param parsed as `(borrow ...)`, second as `(own ...)`"
                 );
                 assert_eq!(*ret_mode, ParamMode::Own, "ret parsed as `(own ...)`");
             }
@@ -2032,7 +2027,7 @@ mod tests {
             r#"
             (module m
               (fn id
-                (type (fn-type (params (con Int)) (ret (con Int))))
+                (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
                 (params x)
                 (body (clone x))))
             "#,
@@ -2059,7 +2054,7 @@ mod tests {
             r#"
             (module m
               (fn id
-                (type (fn-type (params (con Int)) (ret (con Int))))
+                (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
                 (params x)
                 (body (clone))))
             "#,
@@ -2116,7 +2111,7 @@ mod tests {
             r#"
             (module m
               (fn f
-                (type (fn-type (params (con Int)) (ret (con Int))))
+                (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
                 (params x)
                 (body (reuse-as))))
             "#,
@@ -2136,7 +2131,7 @@ mod tests {
             r#"
             (module m
               (fn f
-                (type (fn-type (params (con Int)) (ret (con Int))))
+                (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
                 (params x)
                 (body (reuse-as x))))
             "#,
@@ -2258,12 +2253,12 @@ mod tests {
             r#"
             (module m
               (fn main
-                (type (fn-type (params) (ret (con Int))))
+                (type (fn-type (params) (ret (own (con Int)))))
                 (params)
                 (body
                   (let-rec f
                     (params x)
-                    (type (fn-type (params (con Int)) (ret (con Int))))
+                    (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
                     (body x)
                     (in (app f 1))))))
             "#,
@@ -2300,7 +2295,7 @@ mod tests {
             (module t
               (fn f
                 (suppress (code "over-strict-mode") (because "test reason"))
-                (type (fn-type (params) (ret (con Int))))
+                (type (fn-type (params) (ret (own (con Int)))))
                 (params)
                 (body 0)))
             "#,
@@ -2327,7 +2322,7 @@ mod tests {
               (fn f
                 (suppress (code "over-strict-mode") (because "first"))
                 (suppress (code "other-code") (because "second"))
-                (type (fn-type (params) (ret (con Int))))
+                (type (fn-type (params) (ret (own (con Int)))))
                 (params)
                 (body 0)))
             "#,
@@ -2354,7 +2349,7 @@ mod tests {
             r#"
             (module t
               (fn f
-                (type (fn-type (params) (ret (con Int))))
+                (type (fn-type (params) (ret (own (con Int)))))
                 (params)
                 (body 0)))
             "#,
@@ -2381,7 +2376,7 @@ mod tests {
             (module t
               (fn f
                 (suppress (code "over-strict-mode") (because ""))
-                (type (fn-type (params) (ret (con Int))))
+                (type (fn-type (params) (ret (own (con Int)))))
                 (params)
                 (body 0)))
             "#,
@@ -2406,7 +2401,7 @@ mod tests {
             (module t
               (fn f
                 (suppress (code "over-strict-mode") (because "ok") (oops "x"))
-                (type (fn-type (params) (ret (con Int))))
+                (type (fn-type (params) (ret (own (con Int)))))
                 (params)
                 (body 0)))
             "#,
@@ -2425,7 +2420,7 @@ mod tests {
   (class Foo
     (param a)
     (method m
-      (type (fn-type (params (con a)) (ret (con Int)))))))"#;
+      (type (fn-type (params (own (con a))) (ret (own (con Int))))))))"#;
         let m = parse(src).expect("parse ok");
         assert_eq!(m.defs.len(), 1, "one def");
         match &m.defs[0] {
@@ -2451,7 +2446,7 @@ mod tests {
     (superclass (class Foo) (type a))
     (doc "bar extends foo")
     (method m
-      (type (fn-type (params (con a)) (ret (con Int))))
+      (type (fn-type (params (own (con a))) (ret (own (con Int)))))
       (default 0))))"#;
         let m = parse(src).expect("parse ok");
         let c = match &m.defs[0] {
@@ -2517,7 +2512,7 @@ mod tests {
               (fn f
                 (doc "first")
                 (doc "second")
-                (type (fn-type (params) (ret (con Unit))))
+                (type (fn-type (params) (ret (own (con Unit)))))
                 (params)
                 (body (do io/print_str "x"))))
             "#,
@@ -2536,8 +2531,8 @@ mod tests {
             r#"
             (module m
               (fn f
-                (type (fn-type (params) (ret (con Unit))))
-                (type (fn-type (params) (ret (con Unit))))
+                (type (fn-type (params) (ret (own (con Unit)))))
+                (type (fn-type (params) (ret (own (con Unit)))))
                 (params)
                 (body (do io/print_str "x"))))
             "#,
@@ -2556,7 +2551,7 @@ mod tests {
             r#"
             (module m
               (fn f
-                (type (fn-type (params) (ret (con Unit))))
+                (type (fn-type (params) (ret (own (con Unit)))))
                 (params)
                 (params)
                 (body (do io/print_str "x"))))
@@ -2576,7 +2571,7 @@ mod tests {
             r#"
             (module m
               (fn f
-                (type (fn-type (params) (ret (con Unit))))
+                (type (fn-type (params) (ret (own (con Unit)))))
                 (params)
                 (body (do io/print_str "x"))
                 (body (do io/print_str "y"))))

crates/ailang-surface/src/print.rs

@@ -351,13 +351,11 @@ fn write_instance_method(out: &mut String, m: &InstanceMethod, level: usize) {
 
 // ---- types ----------------------------------------------------------------
 
-/// print one fn-type param/ret slot, wrapping with
-/// `(borrow ...)` or `(own ...)` when the slot has an explicit
-/// mode. `Implicit` is printed bare so pre-18a fixtures round-trip
-/// unchanged.
+/// print one fn-type param/ret slot, always wrapping with
+/// `(own ...)` or `(borrow ...)` — every slot carries an explicit
+/// mode (spec 0062).
 fn write_fn_type_slot(out: &mut String, t: &Type, mode: ParamMode) {
     match mode {
-        ParamMode::Implicit => write_type(out, t),
         ParamMode::Own => {
             out.push_str("(own ");
             write_type(out, t);
@@ -405,7 +403,7 @@ fn write_type(out: &mut String, t: &Type) {
             out.push_str("(fn-type (params");
             for (i, p) in params.iter().enumerate() {
                 out.push(' ');
-                let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
+                let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Own);
                 write_fn_type_slot(out, p, mode);
             }
             out.push_str(") (ret ");
@@ -771,9 +769,9 @@ mod tests {
                     name: "m".into(),
                     ty: Type::Fn {
                         params: vec![Type::Var { name: "a".into() }],
-                        param_modes: vec![ParamMode::Implicit],
+                        param_modes: vec![ParamMode::Own],
                         ret: Box::new(Type::int()),
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                         effects: vec![],
                     },
                     default: None,
@@ -802,9 +800,9 @@ mod tests {
                     name: "m".into(),
                     ty: Type::Fn {
                         params: vec![Type::Var { name: "a".into() }],
-                        param_modes: vec![ParamMode::Implicit],
+                        param_modes: vec![ParamMode::Own],
                         ret: Box::new(Type::int()),
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                         effects: vec![],
                     },
                     default: Some(Term::Lit { lit: Literal::Int { value: 0 } }),
@@ -832,12 +830,12 @@ mod tests {
                     }],
                     body: Box::new(Type::Fn {
                         params: vec![Type::Var { name: "a".into() }],
-                        param_modes: vec![ParamMode::Implicit],
+                        param_modes: vec![ParamMode::Own],
                         ret: Box::new(Type::Con {
                             name: "Str".into(),
                             args: vec![],
                         }),
-                        ret_mode: ParamMode::Implicit,
+                        ret_mode: ParamMode::Own,
                         effects: vec![],
                     }),
                 },

crates/ailang-surface/tests/mut_removed_pin.rs

@@ -5,14 +5,14 @@ use ailang_surface::parse;
 
 #[test]
 fn mut_keyword_is_rejected_by_form_a_parse() {
-    let src = "(module m (fn f (type (fn-type (params) (ret (con Int)))) (params) (body (mut (var x (con Int) 0) (assign x (app + x 1)) x))))";
+    let src = "(module m (fn f (type (fn-type (params) (ret (own (con Int))))) (params) (body (mut (var x (con Int) 0) (assign x (app + x 1)) x))))";
     let r = parse(src);
     assert!(r.is_err(), "mut keyword must no longer parse, got Ok");
 }
 
 #[test]
 fn assign_keyword_is_rejected_by_form_a_parse() {
-    let src = "(module m (fn f (type (fn-type (params) (ret (con Int)))) (params) (body (assign x 1))))";
+    let src = "(module m (fn f (type (fn-type (params) (ret (own (con Int))))) (params) (body (assign x 1))))";
     assert!(parse(src).is_err(), "assign keyword must no longer parse, got Ok");
 }
 

crates/ailang-surface/tests/prelude_module_hash_pin.rs

@@ -47,7 +47,7 @@ fn prelude_parse_yields_canonical_hash() {
     // the synthesised mono def-hashes do NOT (synthesise_mono_fn
     // sets doc: None).
     assert_eq!(
-        h, "b1373a2c69e70a3f",
+        h, "62764e07c1bc9bbb",
         "prelude module hash drifted; if intentional, capture the new \
          hex below + record the why in the commit body."
     );

crates/ailang-surface/tests/reserved_dollar_pin.rs

@@ -12,8 +12,8 @@ use ailang_surface::{parse, ParseError};
 
 #[test]
 fn dollar_binder_in_module_is_rejected_at_parse() {
-    // (module bad (fn main (type (fn-type (params) (ret (con Int)))) (params) (body (let x$1 7 x$1))))
-    let src = "(module bad\n  (fn main\n    (type (fn-type (params) (ret (con Int))))\n    (params)\n    (body\n      (let x$1 7 x$1))))\n";
+    // (module bad (fn main (type (fn-type (params) (ret (own (con Int))))) (params) (body (let x$1 7 x$1))))
+    let src = "(module bad\n  (fn main\n    (type (fn-type (params) (ret (own (con Int)))))\n    (params)\n    (body\n      (let x$1 7 x$1))))\n";
     let err = parse(src).expect_err("authored `$` binder must be rejected at parse");
     assert!(
         matches!(err, ParseError::Lex(LexError::ReservedDollar { ref token, .. }) if token == "x$1"),
@@ -25,6 +25,6 @@ fn dollar_binder_in_module_is_rejected_at_parse() {
 fn dollar_in_string_in_module_parses_clean() {
     // The exemption survives at the `parse` level too: `$` inside a
     // string literal in a real module is fine.
-    let src = "(module dollar_ok\n  (fn main\n    (type (fn-type (params) (ret (con Str))))\n    (params)\n    (body \"price: $5\")))\n";
+    let src = "(module dollar_ok\n  (fn main\n    (type (fn-type (params) (ret (own (con Str)))))\n    (params)\n    (body \"price: $5\")))\n";
     parse(src).expect("string-internal `$` must parse clean");
 }

crates/ailang-surface/tests/round_trip.rs

@@ -51,6 +51,17 @@ fn examples_dir() -> PathBuf {
 //   only one form is hand-authored post-iter; counterparts are derived in-process
 //   via `ail parse`.
 
+/// Fixtures that intentionally do NOT parse — the `#55` cutover
+/// reject corpus. Negative fixtures whose whole point is that the
+/// parser rejects them, so the parse/round-trip properties below are
+/// not meaningful for them and the corpus scan must skip them.
+/// Mirrors the same list in `crates/ail/tests/roundtrip_cli.rs`.
+///
+/// - `bare_slot_reject.ail`: a bare fn-type slot with no mode. The
+///   binary-ParamMode parser rejects it ("fn-type slot requires a
+///   mode: write (own T) or (borrow T)").
+const NON_PARSEABLE_FIXTURES: &[&str] = &["bare_slot_reject.ail"];
+
 fn list_ail_fixtures() -> Vec<PathBuf> {
     let dir = examples_dir();
     let mut paths: Vec<PathBuf> = std::fs::read_dir(&dir)
@@ -60,7 +71,7 @@ fn list_ail_fixtures() -> Vec<PathBuf> {
         .filter(|p| {
             p.file_name()
                 .and_then(|n| n.to_str())
-                .map(|n| n.ends_with(".ail"))
+                .map(|n| n.ends_with(".ail") && !NON_PARSEABLE_FIXTURES.contains(&n))
                 .unwrap_or(false)
         })
         .collect();
@@ -155,7 +166,7 @@ fn round_trip_term_new_mixed_args() {
     // (new Series (con Float) 3) — a Type-positional arg followed by
     // a Value-positional arg. The body lives inside an otherwise
     // minimal module shell that the printer emits in canonical form.
-    let form_a = "(module new_demo\n  (data Series\n    (ctor MkSeries (con Int)))\n  (fn new\n    (type (fn-type (params (con Int)) (ret (con Series))))\n    (params n)\n    (body (term-ctor Series MkSeries n)))\n  (fn main\n    (type (fn-type (params) (ret (con Series))))\n    (params)\n    (body (new Series (con Float) 3))))";
+    let form_a = "(module new_demo\n  (data Series\n    (ctor MkSeries (con Int)))\n  (fn new\n    (type (fn-type (params (own (con Int))) (ret (own (con Series)))))\n    (params n)\n    (body (term-ctor Series MkSeries n)))\n  (fn main\n    (type (fn-type (params) (ret (own (con Series)))))\n    (params)\n    (body (new Series (con Float) 3))))";
     let parsed_once = ailang_surface::parse(form_a)
         .expect("Form-A round-trip fixture must parse");
     let printed = ailang_surface::print(&parsed_once);

design/contracts/0002-data-model.md

@@ -269,9 +269,8 @@ metadata is defined and gated there as well.
 // Function type. paramModes/retMode are metadata on Type::Fn —
 // they are NOT separate Type variants, so every existing match-arm
 // in the typechecker (unify, occurs, apply) keeps working.
-// `paramModes` omitted when every entry is "implicit"; `retMode`
-// omitted when "implicit" (hash-stable when omitted). Full mode
-// contract lives in contracts/0008-memory-model.md.
+// `paramModes` and `retMode` are always present (one mode per slot).
+// Full mode contract lives in contracts/0008-memory-model.md.
 { "k": "fn",
   "params":     [Type...],
   "paramModes": [ParamMode...],
@@ -294,17 +293,15 @@ metadata is defined and gated there as well.
 [memory model](0008-memory-model.md)):
 
 ```
-"implicit"   — unannotated / back-compat. Treated as `own` by the typechecker.
 "own"        — (own T) — caller transfers ownership; callee consumes.
 "borrow"     — (borrow T) — caller retains ownership; callee may not consume.
 ```
 
-`implicit ≡ own` semantically; the distinction exists so existing
-unannotated fixtures continue to serialize without the mode wrapper and keep their
-canonical-JSON hash. 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
+Every fn-type slot carries `own` or `borrow`; ownership has no
+default — there is no bare/unannotated mode. 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).
 
 Ratified by: `crates/ailang-core/tests/design_schema_drift.rs`.

design/contracts/0008-memory-model.md

@@ -54,14 +54,13 @@ schema). The substantive reasons for per-position metadata over a
   ordering that don't exist when modes live in a flat metadata
   vector.
 
-`Implicit` is the legacy / back-compat state — semantically
-equivalent to `Own` but printed bare (`(con T)`, no wrapper).
-`Own` and `Borrow` are explicitly annotated.
+`Own` and `Borrow` are the two modes; every fn-type slot carries
+one explicitly. Ownership has no default — there is no
+bare/unannotated mode.
 
-JSON canonical hash for every existing fixture stays bit-
-identical: `param_modes` is skipped when every entry is
-`Implicit`, `ret_mode` is skipped when `Implicit`. Existing
-modules emit the same bytes as before.
+JSON canonical form: `param_modes` and `ret_mode` are always
+present, one mode per slot, with no elision — the mode vectors
+are never omitted from the canonical bytes.
 
 **Type::Con name scoping (canonical form).** Within a
 `.ail.json`, a `Type::Con.name` is interpreted relative to the
@@ -189,6 +188,9 @@ fn-param `p` annotated `(own T)` when:
      never consumes `p` as a whole).
   2. For every match arm whose scrutinee is `p`, no
      **heap-typed** pattern-binder has `consume_count > 0`.
+  3. `p`'s type `T` is **not** a value type
+     (`Int`/`Bool`/`Float`/`Unit`).
+  4. The enclosing fn's body is **not** `(intrinsic)`.
 
 The heap-type filter is load-bearing for soundness:
 `match xs { Cons(h, t) => h }` records `consume_count(h) == 1`,
@@ -198,6 +200,22 @@ binders is what lets the lint correctly identify `head_or_zero`
 as over-strict (could be `borrow`) while staying silent on
 `sum_list` where `t: List` *is* moved out.
 
+Conditions 3 and 4 keep the lint coherent under universal mode
+activation:
+
+- **Value-typed params never fire.** `(borrow V)` for a value
+  type `V` is itself rejected by the `borrow-over-value` check,
+  so `(own V)` is the only legal mode for a value-typed param.
+  A suggestion to relax `(own Int)` to `(borrow Int)` would point
+  at an illegal rewrite, so the lint stays silent on value-typed
+  params regardless of whether they are consumed.
+- **`(intrinsic)`-bodied fns never fire.** The linearity walk
+  does nothing for a `Term::Intrinsic` body, so every param of an
+  intrinsic has `consume_count == 0` — a guaranteed false positive.
+  An intrinsic's param modes are hand-authored contracts
+  (`new`/`get`/`set`/`float_*`), not lint-derivable from a walkable
+  body, so the whole fn is skipped.
+
 Severity: `Warning`. `ail check`, `ail build`, `ail emit-ir` exit 1
 only on at least one `Error`; warnings print but do not abort.
 
@@ -246,10 +264,9 @@ metadata's role is explicit:
   fall-throughs to a `ret` (no tail-call), every parameter with
   `param_modes[i] == Own` is dec'd before the `ret` iff its
   uniqueness `consume_count == 0` and the ret value is not the
-  param itself. `Borrow` and `Implicit` parameters are skipped:
-  `Borrow` retains the caller's ownership by contract;
-  `Implicit` carries no static caller-handed-off-ownership
-  signal (it's the back-compat lane).
+  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`.)
 
 - **Iter A: arm-close pattern-binder dec.** When a match-arm's
   body terminates without a tail-call, every ptr-typed
@@ -257,8 +274,8 @@ metadata's role is explicit:
   iff its `consume_count == 0` and it is not the arm's tail
   value, **gated on the scrutinee's static ownership**. If the
   scrutinee is a fn-param, only `Own`-mode scrutinees enable
-  the dec — `Borrow` and `Implicit` scrutinees would let the
-  arm dec memory the caller still references.
+  the dec — a `Borrow` scrutinee would let the arm dec memory
+  the caller still references.
 
 - **Pre-tail-call shallow-dec.** When a match-arm's
   body IS a tail call, both Iter A and Iter B are skipped (the
@@ -292,10 +309,12 @@ suppressing or doubling a drop. Ratified by
   trackable for scope-close drop iff the callee's
   `ret_mode == Own`. The signal is the callee's static
   contract that ownership of the freshly heap-allocated cell
-  flows to the caller. `Borrow`-returning calls remain
-  non-trackable (the callee retains ownership; the caller
-  holds a view, not an own ref). `Implicit`-returning calls
-  remain non-trackable (back-compat lane).
+  flows to the caller. 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 (the callee retains ownership; the caller holds a view,
+  not an own ref — and a borrow-return is in any case rejected
+  at the signature, spec 0062).
 
 The drop fn's symbol resolution for an Own-returning App:
 synthesise the call's return type, resolve `Type::Con { name }`

examples/bare_slot_reject.ail

@@ -0,0 +1,10 @@
+(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)))

examples/bench_closure_chain.ail

@@ -28,9 +28,9 @@
     (doc "Higher-order: apply f three times to seed.")
     (type
       (fn-type
-        (params (fn-type (params (con Int)) (ret (con Int)))
-                (con Int))
-        (ret (con Int))))
+        (params (own (fn-type (params (own (con Int))) (ret (own (con Int)))))
+                (own (con Int)))
+        (ret (own (con Int)))))
     (params f seed)
     (body
       (app f (app f (app f seed)))))
@@ -39,15 +39,15 @@
     (doc "For each i in [n-1, n-2, ..., 0], build a closure capturing i, pass to apply_thrice, accumulate. Tail-recursive on i and acc.")
     (type
       (fn-type
-        (params (con Int) (con Int))
-        (ret (con Int))))
+        (params (own (con Int)) (own (con Int)))
+        (ret (own (con Int)))))
     (params i acc)
     (body
       (if (app lt i 0)
         acc
         (let-rec helper
           (params x)
-          (type (fn-type (params (con Int)) (ret (con Int))))
+          (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
           (body i)
           (in
             (let r (app apply_thrice helper i)
@@ -55,12 +55,12 @@
 
   (fn run
     (doc "Drive run_loop from i=n-1 down to 0.")
-    (type (fn-type (params (con Int)) (ret (con Int))))
+    (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
     (params n)
     (body (app run_loop (app - n 1) 0)))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (app print (app run 10000))

examples/bench_compute_collatz.ail

@@ -27,8 +27,8 @@
     (doc "Tail-recursive: count Collatz steps from n to 1, accumulating in acc.")
     (type
       (fn-type
-        (params (con Int) (con Int))
-        (ret (con Int))))
+        (params (own (con Int)) (own (con Int)))
+        (ret (own (con Int)))))
     (params n acc)
     (body
       (if (app eq n 1)
@@ -41,8 +41,8 @@
     (doc "Tail-recursive: sum collatz_steps(i) for i in [n, n-1, ..., 1].")
     (type
       (fn-type
-        (params (con Int) (con Int))
-        (ret (con Int))))
+        (params (own (con Int)) (own (con Int)))
+        (ret (own (con Int)))))
     (params i total)
     (body
       (if (app eq i 0)
@@ -52,12 +52,12 @@
           (app + total (app collatz_steps i 0))))))
 
   (fn run_one
-    (type (fn-type (params (con Int)) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params (own (con Int))) (ret (own (con Unit))) (effects IO)))
     (params n)
     (body (app print (app sum_steps_loop n 0))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (app run_one 10000)

examples/bench_compute_intsum.ail

@@ -24,8 +24,8 @@
     (doc "Tail-recursive: acc += i*7 for i in [n, n-1, ..., 1]. Returns final acc.")
     (type
       (fn-type
-        (params (con Int) (con Int))
-        (ret (con Int))))
+        (params (own (con Int)) (own (con Int)))
+        (ret (own (con Int)))))
     (params i acc)
     (body
       (if (app eq i 0)
@@ -35,12 +35,12 @@
           (app + acc (app * i 7))))))
 
   (fn run_one
-    (type (fn-type (params (con Int)) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params (own (con Int))) (ret (own (con Unit))) (effects IO)))
     (params n)
     (body (app print (app intsum_loop n 0))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (app run_one 1000000)

examples/bench_hof_pipeline.ail

@@ -8,7 +8,7 @@
 ;      layout is the same width as bench_list_sum's IntList ICons,
 ;      but the type-arg substitution is the additional code path.
 ;   2. The traversal is via `fold_with_fn` — an HOF taking
-;      `(fn-type (params a) (ret (con Int)))` as its first param.
+;      `(fn-type (params (own a)) (ret (own (con Int))))` as its first param.
 ;      Each step calls `(app f h)` — an indirect call through the
 ;      fn-arg. This is the only fixture that exercises tight-loop
 ;      indirect dispatch.
@@ -36,8 +36,8 @@
     (doc "Build [0, 1, ..., n-1] :: List Int. Tail-recursive accumulator form.")
     (type
       (fn-type
-        (params (con Int) (con List (con Int)))
-        (ret (con List (con Int)))))
+        (params (own (con Int)) (own (con List (con Int))))
+        (ret (own (con List (con Int))))))
     (params n acc)
     (body
       (if (app eq n 0)
@@ -48,7 +48,7 @@
 
   (fn inc
     (doc "Add 1 to an Int. Used as the HOF argument to fold_with_fn.")
-    (type (fn-type (params (con Int)) (ret (con Int))))
+    (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
     (params x)
     (body (app + x 1)))
 
@@ -57,10 +57,10 @@
     (type
       (forall (vars a)
         (fn-type
-          (params (fn-type (params a) (ret (con Int)))
-                  (con List a)
-                  (con Int))
-          (ret (con Int)))))
+          (params (borrow (fn-type (params (own a)) (ret (own (con Int)))))
+                  (own (con List a))
+                  (own (con Int)))
+          (ret (own (con Int))))))
     (params f xs acc)
     (body
       (match xs
@@ -70,7 +70,7 @@
 
   (fn run_one
     (doc "Build [0..n-1], fold with inc, print sum of (inc x).")
-    (type (fn-type (params (con Int)) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params (own (con Int))) (ret (own (con Unit))) (effects IO)))
     (params n)
     (body
       (app print
@@ -79,7 +79,7 @@
           0))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (app run_one 100000)

examples/bench_latency_explicit.ail

@@ -45,7 +45,7 @@
     (doc "Build a balanced tree of given depth, every value = 1. Returns owned Tree; main holds it across the loop and the final drop fires at main's scope close.")
     (type
       (fn-type
-        (params (con Int))
+        (params (own (con Int)))
         (ret (own (con Tree)))))
     (params depth)
     (body
@@ -61,7 +61,7 @@
     (type
       (fn-type
         (params (borrow (con Tree)))
-        (ret (con Int))))
+        (ret (own (con Int)))))
     (params t)
     (body
       (match t
@@ -74,7 +74,7 @@
     (doc "Tail-recursive list builder. Returns owned chain; caller is sum_list which owns and drops it.")
     (type
       (fn-type
-        (params (con Int) (own (con IntList)))
+        (params (own (con Int)) (own (con IntList)))
         (ret (own (con IntList)))))
     (params n acc)
     (body
@@ -88,7 +88,7 @@
     (doc "Build [0,1,...,n-1] :: IntList. Returns owned chain.")
     (type
       (fn-type
-        (params (con Int))
+        (params (own (con Int)))
         (ret (own (con IntList)))))
     (params n)
     (body
@@ -98,8 +98,8 @@
     (doc "Tail-recursive sum. Owns xs; consumes it via the LCons arm's t binder (move-into-tail-call).")
     (type
       (fn-type
-        (params (own (con IntList)) (con Int))
-        (ret (con Int))))
+        (params (own (con IntList)) (own (con Int)))
+        (ret (own (con Int)))))
     (params xs acc)
     (body
       (match xs
@@ -112,7 +112,7 @@
     (type
       (fn-type
         (params (own (con IntList)))
-        (ret (con Int))))
+        (ret (own (con Int)))))
     (params xs)
     (body
       (app sum_list_acc xs 0)))
@@ -121,8 +121,8 @@
     (doc "One bench operation: build+sum a fresh CHUNK_LEN-cell list, pin the tree's root, return their sum so the value chain stays observable. Tree is borrowed; no inc/dec on the hot path against the persistent cache.")
     (type
       (fn-type
-        (params (con Int) (borrow (con Tree)))
-        (ret (con Int))))
+        (params (own (con Int)) (borrow (con Tree)))
+        (ret (own (con Int)))))
     (params chunk_len t)
     (body
       (app + (app sum_list (app cons_n chunk_len)) (app pin_root t))))
@@ -133,8 +133,8 @@
     (doc "Tail-recursive bench loop. Tree is borrowed across all iterations.")
     (type
       (fn-type
-        (params (con Int) (con Int) (con Int) (con Int) (borrow (con Tree)))
-        (ret (con Unit))
+        (params (own (con Int)) (own (con Int)) (own (con Int)) (own (con Int)) (borrow (con Tree)))
+        (ret (own (con Unit)))
         (effects IO)))
     (params remaining print_countdown chunk_len print_k t)
     (body
@@ -159,7 +159,7 @@
 
   (fn main
     (doc "Top-level: build tree, signal READY (8888), run loop, signal DONE (9999 emitted by loop).")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (let t (app build_tree 19)

examples/bench_latency_implicit.ail

@@ -69,8 +69,8 @@
     (doc "Build a balanced tree of given depth, every value = 1. Constructor-blocked — recursion depth = `depth`, fits 8MB stack at depth 19.")
     (type
       (fn-type
-        (params (con Int))
-        (ret (con Tree))))
+        (params (own (con Int)))
+        (ret (own (con Tree)))))
     (params depth)
     (body
       (if (app eq depth 0)
@@ -84,8 +84,8 @@
     (doc "Touch every node of the tree (ensures liveness across the loop).")
     (type
       (fn-type
-        (params (con Tree))
-        (ret (con Int))))
+        (params (own (con Tree)))
+        (ret (own (con Int)))))
     (params t)
     (body
       (match t
@@ -99,8 +99,8 @@
     (doc "Tail-recursive list builder. Result = [n-1, n-2, ..., 0] :: IntList.")
     (type
       (fn-type
-        (params (con Int) (con IntList))
-        (ret (con IntList))))
+        (params (own (con Int)) (own (con IntList)))
+        (ret (own (con IntList)))))
     (params n acc)
     (body
       (if (app eq n 0)
@@ -113,8 +113,8 @@
     (doc "Build [0,1,...,n-1] :: IntList.")
     (type
       (fn-type
-        (params (con Int))
-        (ret (con IntList))))
+        (params (own (con Int)))
+        (ret (own (con IntList)))))
     (params n)
     (body
       (app cons_n_acc n (term-ctor IntList LNil))))
@@ -123,8 +123,8 @@
     (doc "Tail-recursive sum.")
     (type
       (fn-type
-        (params (con IntList) (con Int))
-        (ret (con Int))))
+        (params (own (con IntList)) (own (con Int)))
+        (ret (own (con Int)))))
     (params xs acc)
     (body
       (match xs
@@ -136,8 +136,8 @@
     (doc "Sum every element. Calls sum_list_acc with seed 0.")
     (type
       (fn-type
-        (params (con IntList))
-        (ret (con Int))))
+        (params (own (con IntList)))
+        (ret (own (con Int)))))
     (params xs)
     (body
       (app sum_list_acc xs 0)))
@@ -158,8 +158,8 @@
     (doc "Constant-time tree liveness pin — read root tag, return 1 (TNode) or 0 (TLeaf).")
     (type
       (fn-type
-        (params (con Tree))
-        (ret (con Int))))
+        (params (borrow (con Tree)))
+        (ret (own (con Int)))))
     (params t)
     (body
       (match t
@@ -170,8 +170,8 @@
     (doc "One bench operation: build+sum a fresh CHUNK_LEN-cell list, pin the tree's root, return their sum so the value chain stays observable.")
     (type
       (fn-type
-        (params (con Int) (con Tree))
-        (ret (con Int))))
+        (params (own (con Int)) (borrow (con Tree)))
+        (ret (own (con Int)))))
     (params chunk_len t)
     (body
       (app + (app sum_list (app cons_n chunk_len)) (app pin_root t))))
@@ -192,8 +192,8 @@
     (doc "Tail-recursive bench loop. Ops countdown in `remaining`; print marker every time `print_countdown` hits 0.")
     (type
       (fn-type
-        (params (con Int) (con Int) (con Int) (con Int) (con Tree))
-        (ret (con Unit))
+        (params (own (con Int)) (own (con Int)) (own (con Int)) (own (con Int)) (borrow (con Tree)))
+        (ret (own (con Unit)))
         (effects IO)))
     (params remaining print_countdown chunk_len print_k t)
     (body
@@ -218,7 +218,7 @@
 
   (fn main
     (doc "Top-level: build tree, signal READY (8888), run loop, signal DONE (9999 emitted by loop).")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (let t (app build_tree 19)

examples/bench_list_sum.ail

@@ -40,8 +40,8 @@
     (doc "Tail-recursive list builder. Result = accumulator-prepended list.")
     (type
       (fn-type
-        (params (con Int) (con IntList))
-        (ret (con IntList))))
+        (params (own (con Int)) (own (con IntList)))
+        (ret (own (con IntList)))))
     (params n acc)
     (body
       (if (app eq n 0)
@@ -54,8 +54,8 @@
     (doc "Build [0, 1, ..., n-1] :: IntList. Order doesn't matter for sum.")
     (type
       (fn-type
-        (params (con Int))
-        (ret (con IntList))))
+        (params (own (con Int)))
+        (ret (own (con IntList)))))
     (params n)
     (body
       (app cons_n_acc n (term-ctor IntList INil))))
@@ -64,8 +64,8 @@
     (doc "Tail-recursive sum.")
     (type
       (fn-type
-        (params (con IntList) (con Int))
-        (ret (con Int))))
+        (params (own (con IntList)) (own (con Int)))
+        (ret (own (con Int)))))
     (params xs acc)
     (body
       (match xs
@@ -77,21 +77,21 @@
     (doc "Sum every element. Calls sum_acc with seed 0.")
     (type
       (fn-type
-        (params (con IntList))
-        (ret (con Int))))
+        (params (own (con IntList)))
+        (ret (own (con Int)))))
     (params xs)
     (body
       (app sum_acc xs 0)))
 
   (fn run_one
     (doc "Build a list of length n, sum it, print the sum.")
-    (type (fn-type (params (con Int)) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params (own (con Int))) (ret (own (con Unit))) (effects IO)))
     (params n)
     (body
       (app print (app sum_list (app cons_n n)))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (app run_one 100000)

examples/bench_list_sum.prose.txt

@@ -3,7 +3,7 @@
 data IntList = INil | ICons(Int, IntList)
 
 /// Tail-recursive list builder. Result = accumulator-prepended list.
-fn cons_n_acc(n: Int, acc: IntList) -> IntList {
+fn cons_n_acc(n: own Int, acc: own IntList) -> own IntList {
   if eq(n, 0) {
     acc
   } else {
@@ -12,12 +12,12 @@ fn cons_n_acc(n: Int, acc: IntList) -> IntList {
 }
 
 /// Build [0, 1, ..., n-1] :: IntList. Order doesn't matter for sum.
-fn cons_n(n: Int) -> IntList {
+fn cons_n(n: own Int) -> own IntList {
   cons_n_acc(n, INil)
 }
 
 /// Tail-recursive sum.
-fn sum_acc(xs: IntList, acc: Int) -> Int {
+fn sum_acc(xs: own IntList, acc: own Int) -> own Int {
   match xs {
     INil => acc,
     ICons(h, t) => tail sum_acc(t, acc + h)
@@ -25,16 +25,16 @@ fn sum_acc(xs: IntList, acc: Int) -> Int {
 }
 
 /// Sum every element. Calls sum_acc with seed 0.
-fn sum_list(xs: IntList) -> Int {
+fn sum_list(xs: own IntList) -> own Int {
   sum_acc(xs, 0)
 }
 
 /// Build a list of length n, sum it, print the sum.
-fn run_one(n: Int) -> Unit with IO {
+fn run_one(n: own Int) -> own Unit with IO {
   print(sum_list(cons_n(n)))
 }
 
-fn main() -> Unit with IO {
+fn main() -> own Unit with IO {
   run_one(100000);
   run_one(1000000);
   run_one(3000000)

examples/bench_list_sum_explicit.ail

@@ -37,7 +37,7 @@
     (doc "Tail-recursive: prepend (n-1, n-2, ..., 0) onto acc. Returns owned chain.")
     (type
       (fn-type
-        (params (con Int) (own (con IntList)))
+        (params (own (con Int)) (own (con IntList)))
         (ret (own (con IntList)))))
     (params n acc)
     (body
@@ -51,7 +51,7 @@
     (doc "Build [0..n-1] :: IntList. Returns owned chain; caller owns and consumes.")
     (type
       (fn-type
-        (params (con Int))
+        (params (own (con Int)))
         (ret (own (con IntList)))))
     (params n)
     (body (app cons_n_acc n (term-ctor IntList INil))))
@@ -60,8 +60,8 @@
     (doc "Tail-recursive sum. Owns xs; consumes via LCons-arm move-into-tail-call.")
     (type
       (fn-type
-        (params (own (con IntList)) (con Int))
-        (ret (con Int))))
+        (params (own (con IntList)) (own (con Int)))
+        (ret (own (con Int)))))
     (params xs acc)
     (body
       (match xs
@@ -74,19 +74,19 @@
     (type
       (fn-type
         (params (own (con IntList)))
-        (ret (con Int))))
+        (ret (own (con Int)))))
     (params xs)
     (body (app sum_acc xs 0)))
 
   (fn run_one
     (doc "Build, sum, print. The owned list flows from cons_n into sum_list and is fully consumed.")
-    (type (fn-type (params (con Int)) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params (own (con Int))) (ret (own (con Unit))) (effects IO)))
     (params n)
     (body
       (app print (app sum_list (app cons_n n)))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (app run_one 100000)

examples/bench_mono_dispatch.ail

@@ -2,7 +2,7 @@
   (class Foo
     (param a)
     (method foo
-      (type (fn-type (params a) (ret (con Int))))))
+      (type (fn-type (params (own a)) (ret (own (con Int)))))))
   (instance
     (class Foo)
     (type (con Int))
@@ -11,13 +11,13 @@
   (class Looper
     (param a)
     (method loop_call
-      (type (fn-type (params a (con Int)) (ret (con Int))))))
+      (type (fn-type (params (own a) (own (con Int))) (ret (own (con Int)))))))
   (instance
     (class Looper)
     (type (con Int))
     (method loop_call
       (body (lam (params (typed i a) (typed acc (con Int))) (ret (con Int)) (body (if (app eq i 0) acc (tail-app loop_call (app - i 1) (app + acc (app foo (app + acc i))))))))))
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (app print (app loop_call 100000000 0)))))

examples/bench_tree_walk.ail

@@ -38,8 +38,8 @@
     (doc "Balanced binary tree of given depth, every value = 1.")
     (type
       (fn-type
-        (params (con Int))
-        (ret (con Tree))))
+        (params (own (con Int)))
+        (ret (own (con Tree)))))
     (params depth)
     (body
       (if (app eq depth 0)
@@ -53,8 +53,8 @@
     (doc "Sum every Node value via match recursion. Constructor-blocked: not tail-recursive, but recursion depth = tree depth so fits.")
     (type
       (fn-type
-        (params (con Tree))
-        (ret (con Int))))
+        (params (own (con Tree)))
+        (ret (own (con Int)))))
     (params t)
     (body
       (match t
@@ -64,13 +64,13 @@
 
   (fn run_one
     (doc "Build a tree of given depth, sum it, print the sum.")
-    (type (fn-type (params (con Int)) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params (own (con Int))) (ret (own (con Unit))) (effects IO)))
     (params depth)
     (body
       (app print (app sum_tree (app build_tree depth)))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (app run_one 16)

examples/bool_to_str_drop_rc.ail

@@ -1,6 +1,6 @@
 (module bool_to_str_drop_rc
   (fn main
     (doc "Iter 24.1: pin that `bool_to_str` participates in RC discipline. Bind the heap-Str result to `s`, consume `s` once in `io/print_str`, let the binder drop at scope close. Under --alloc=rc with AILANG_RC_STATS=1 the atexit summary must report allocs == 1 && frees == 1 && live == 0 — the heap-Str slab allocated by str_alloc inside ailang_bool_to_str rides the same rc_header + ailang_rc_dec path as int_to_str.")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (let s (app bool_to_str true) (seq (do io/print_str s) (do io/print_str "\n"))))))

examples/bool_to_str_smoke_false.ail

@@ -1,6 +1,6 @@
 (module bool_to_str_smoke_false
   (fn main
     (doc "Iter 24.1: stdout-smoke for the false branch of bool_to_str. Stdout must be `false\\n` (puts adds the newline). Companion of bool_to_str_drop_rc.ail.json (which covers the true branch and the RC-stats invariant).")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (let s (app bool_to_str false) (seq (do io/print_str s) (do io/print_str "\n"))))))

examples/borrow_own_demo.ail

@@ -28,7 +28,7 @@
     (type
       (fn-type
         (params (borrow (con List)))
-        (ret (con Int))))
+        (ret (own (con Int)))))
     (params xs)
     (body
       (match xs
@@ -41,7 +41,7 @@
     (type
       (fn-type
         (params (own (con List)))
-        (ret (con Int))))
+        (ret (own (con Int)))))
     (params xs)
     (body
       (match xs
@@ -51,7 +51,7 @@
 
   (fn main
     (doc "Build [1,2,3]; print list_length (3) then sum_list (6).")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (let xs

examples/borrow_value_reject.ail

@@ -0,0 +1,10 @@
+(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)))

examples/box.ail

@@ -14,8 +14,8 @@
     (type
       (forall (vars a)
         (fn-type
-          (params (con Box a))
-          (ret a))))
+          (params (own (con Box a)))
+          (ret (own a)))))
     (params b)
     (body
       (match b
@@ -27,7 +27,7 @@
     (type
       (fn-type
         (params)
-        (ret (con Unit))
+        (ret (own (con Unit)))
         (effects IO)))
     (params)
     (body

examples/broken_unbound.ail.json

@@ -9,12 +9,20 @@
       "type": {
         "k": "fn",
         "params": [],
-        "ret": { "k": "con", "name": "Int" },
+        "param_modes": [],
+        "ret": {
+          "k": "con",
+          "name": "Int"
+        },
+        "ret_mode": "own",
         "effects": []
       },
       "params": [],
       "doc": "Referenziert eine nicht-existente Variable -> unbound-var.",
-      "body": { "t": "var", "name": "does_not_exist" }
+      "body": {
+        "t": "var",
+        "name": "does_not_exist"
+      }
     }
   ]
 }

examples/bug_unbound_in_instance_method.ail

@@ -2,7 +2,7 @@
   (class Describe
     (param a)
     (method describe
-      (type (fn-type (params (borrow a)) (ret (con Str))))))
+      (type (fn-type (params (borrow a)) (ret (own (con Str)))))))
   (instance
     (class Describe)
     (type (con Int))
@@ -13,6 +13,6 @@
           (ret (con Str))
           (body (app format_label "n=" (app int_to_str n)))))))
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (do io/print_str (app describe 5)))))

examples/classify_pin.ail

@@ -1,5 +1,5 @@
 (module classify_pin
-  (fn bump (type (fn-type (params (con Int)) (ret (con Int)))) (params n)
+  (fn bump (type (fn-type (params (own (con Int))) (ret (own (con Int))))) (params n)
     (body (app + n 1)))
-  (fn main (type (fn-type (params) (ret (con Int)))) (params)
+  (fn main (type (fn-type (params) (ret (own (con Int))))) (params)
     (body (app bump 41))))

examples/clone_demo.ail

@@ -19,7 +19,7 @@
 
   (fn main
     (doc "Use `(clone x)` on a let-bound Int; print it.")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (let x 42

examples/closure.ail

@@ -1,11 +1,11 @@
 (module closure
   (fn apply
     (doc "apply a fn-of-Int to an Int")
-    (type (fn-type (params (fn-type (params (con Int)) (ret (con Int))) (con Int)) (ret (con Int))))
+    (type (fn-type (params (own (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con Int))) (ret (own (con Int)))))
     (params f x)
     (body (app f x)))
   (fn main
     (doc "captures `n` from the enclosing let, returns 42")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (let n 3 (app print (app apply (lam (params (typed x (con Int))) (ret (con Int)) (body (app + x n))) 39))))))

examples/cmp_max_smoke.ail

@@ -1,11 +1,11 @@
 (module cmp_max_smoke
   (fn cmp_max
-    (type (forall (vars a) (constraints (constraint prelude.Ord a)) (fn-type (params a a) (ret a))))
+    (type (forall (vars a) (constraints (constraint prelude.Ord a)) (fn-type (params (own a) (own a)) (ret (own a)))))
     (params x y)
     (body (match (app compare x y)
       (case (pat-ctor LT) y)
       (case _ x))))
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (app print (app cmp_max 3 7)))))

examples/compare_float_noinstance.ail

@@ -1,5 +1,5 @@
 (module compare_float_noinstance
   (fn cmp
-    (type (fn-type (params) (ret (con Ordering))))
+    (type (fn-type (params) (ret (own (con Ordering)))))
     (params)
     (body (app compare 1.0 2.0))))

examples/compare_primitives_smoke.ail

@@ -1,6 +1,6 @@
 (module compare_primitives_smoke
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (seq (seq (app print (match (app compare 1 2)
       (case (pat-ctor LT) 1)

examples/ct_1_ordering_signum.ail

@@ -23,7 +23,7 @@
 
   (fn signum
     (doc "Map an Int to -1/0/+1 via prelude.compare. Returns the sign as an Int.")
-    (type (fn-type (params (con Int)) (ret (con Int))))
+    (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
     (params n)
     (body
       (match (app compare n 0)
@@ -33,7 +33,7 @@
 
   (fn drain
     (doc "Print signum of every element of xs, in list order.")
-    (type (fn-type (params (con IntList)) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params (own (con IntList))) (ret (own (con Unit))) (effects IO)))
     (params xs)
     (body
       (match xs
@@ -43,7 +43,7 @@
                (tail-app drain t))))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (app drain

examples/ct_2_bare_cross_module.ail

@@ -22,13 +22,13 @@
     (doc "Identity over Maybe<Int>; signature uses bare `Maybe` with no import.")
     (type
       (fn-type
-        (params (con Maybe (con Int)))
-        (ret (con Maybe (con Int)))))
+        (params (own (con Maybe (con Int))))
+        (ret (own (con Maybe (con Int))))))
     (params m)
     (body m))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (app classify (term-ctor Maybe Just 7)))))

examples/ct_3_bad_qualified.ail

@@ -11,12 +11,12 @@
     (doc "Identity at mystery.Widget — but `mystery` is not a workspace module.")
     (type
       (fn-type
-        (params (con mystery.Widget))
-        (ret (con mystery.Widget))))
+        (params (own (con mystery.Widget)))
+        (ret (own (con mystery.Widget)))))
     (params w)
     (body w))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (do io/print_str "unreachable"))))

examples/ct_3b_bad_qualified_known_module.ail

@@ -15,12 +15,12 @@
     (doc "Identity at std_maybe.Widget — `std_maybe` is real, but `Widget` is not in it.")
     (type
       (fn-type
-        (params (con std_maybe.Widget))
-        (ret (con std_maybe.Widget))))
+        (params (own (con std_maybe.Widget)))
+        (ret (own (con std_maybe.Widget)))))
     (params w)
     (body w))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body (do io/print_str "unreachable"))))

examples/ctt2_collision_cls.ail

@@ -2,4 +2,4 @@
   (class MyC
     (param a)
     (method op
-      (type (fn-type (params a) (ret (con Int)))))))
+      (type (fn-type (params (own a)) (ret (own (con Int))))))))

examples/drop_value_field_no_segfault_pin.ail

@@ -0,0 +1,44 @@
+; RED-pin fixture for leg (C) of the drop-soundness bug family the
+; Implicit-cutover (#55) surfaced: a polymorphic ctor's drop fn
+; rc_dec's a type-parameter field even when that field is
+; monomorphised at a value type (Int).
+;
+; `Box a` is the minimal single-field box. `unbox` takes the box by
+; `own` and matches it, extracting the inner value `x` and returning
+; it. The match consumes the box husk, so codegen emits the
+; scope-close drop `drop_drop_value_field_no_segfault_pin_Box(box)`.
+; That drop fn is emitted ONCE from the polymorphic declaration; the
+; field type is the type-var `a`, which `llvm_type` cannot lower, so
+; drop.rs's `.unwrap_or_else(|_| "ptr")` treats it as a boxed pointer
+; and emits `ailang_rc_dec` on it.
+;
+; At the `Box Int` monomorph the field holds the raw i64 `7` stored
+; inline (offset 8), NOT a heap pointer. `ailang_rc_dec(7)`
+; dereferences address 7 -> SIGSEGV. Expected post-fix: prints `7`,
+; exits 0, AILANG_RC_STATS reports `allocs == frees && live == 0`
+; (the one Box slab is freed exactly once; no spurious dec of the
+; inline value field).
+
+(module drop_value_field_no_segfault_pin
+
+  (data Box (vars a)
+    (doc "Single-field polymorphic box.")
+    (ctor MkBox a))
+
+  (fn unbox
+    (doc "Consume the box by own, return its inner value. The match drops the box husk.")
+    (type
+      (forall (vars a)
+        (fn-type
+          (params (own (con Box a)))
+          (ret (own a)))))
+    (params b)
+    (body
+      (match b
+        (case (pat-ctor MkBox x) x))))
+
+  (fn main
+    (doc "Build MkBox 7 at Int, unbox it (drops the Box husk), print the result.")
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
+    (params)
+    (body (app print (app unbox (term-ctor Box MkBox 7))))))

examples/embed_backtest_step.ail

@@ -4,8 +4,8 @@
     (export "backtest_step")
     (type
       (fn-type
-        (params (con Int) (con Int))
-        (ret (con Int))))
+        (params (own (con Int)) (own (con Int)))
+        (ret (own (con Int)))))
     (params state sample)
     (body
       (app + state (app * sample sample))))
@@ -13,8 +13,8 @@
   (fn helper
     (type
       (fn-type
-        (params (con Int))
-        (ret (con Int))))
+        (params (own (con Int)))
+        (ret (own (con Int)))))
     (params x)
     (body
       (app * x x))))

examples/embed_backtest_step_record.ail

@@ -7,8 +7,8 @@
     (export "backtest_step")
     (type
       (fn-type
-        (params (own (con State)) (con Float))
-        (ret (con State))))
+        (params (own (con State)) (own (con Float)))
+        (ret (own (con State)))))
     (params st sample)
     (body
       (match st

examples/embed_backtest_step_record_borrow.ail

@@ -7,8 +7,8 @@
     (export "backtest_step")
     (type
       (fn-type
-        (params (borrow (con State)) (con Float))
-        (ret (con State))))
+        (params (borrow (con State)) (own (con Float)))
+        (ret (own (con State)))))
     (params st sample)
     (body
       (match st

examples/embed_backtest_step_tick.ail

@@ -11,7 +11,7 @@
     (type
       (fn-type
         (params (own (con State)) (own (con Tick)))
-        (ret (con State))))
+        (ret (own (con State)))))
     (params st tick)
     (body
       (match st

examples/embed_backtest_step_tick_borrow.ail

@@ -11,7 +11,7 @@
     (type
       (fn-type
         (params (own (con State)) (borrow (con Tick)))
-        (ret (con State))))
+        (ret (own (con State)))))
     (params st tick)
     (body
       (match st

examples/embed_export_adt_ret_rejected.ail

@@ -6,7 +6,7 @@
     (export "f")
     (type
       (fn-type
-        (params (con Int))
-        (ret (con Reading))))
+        (params (own (con Int)))
+        (ret (own (con Reading)))))
     (params n)
     (body (term-ctor Reading Sample n "tick"))))

examples/embed_export_effectful_rejected.ail

@@ -3,8 +3,8 @@
     (export "log_step")
     (type
       (fn-type
-        (params (con Int) (con Str))
-        (ret (con Int))
+        (params (own (con Int)) (own (con Str)))
+        (ret (own (con Int)))
         (effects IO)))
     (params state label)
     (body

examples/embed_export_float_ok.ail

@@ -3,8 +3,8 @@
     (export "embed_scale")
     (type
       (fn-type
-        (params (con Float) (con Float))
-        (ret (con Float))))
+        (params (own (con Float)) (own (con Float)))
+        (ret (own (con Float)))))
     (params a b)
     (body
       (app * a b))))

examples/embed_export_io_rejected.ail

@@ -3,8 +3,8 @@
     (export "f")
     (type
       (fn-type
-        (params (con Int))
-        (ret (con Int))
+        (params (own (con Int)))
+        (ret (own (con Int)))
         (effects IO)))
     (params n)
     (body

examples/embed_export_list_field_record_rejected.ail

@@ -6,6 +6,6 @@
     (ctor Boxed (con Int) (con List)))
   (fn f
     (export "f")
-    (type (fn-type (params (con Int)) (ret (con Boxed))))
+    (type (fn-type (params (own (con Int))) (ret (own (con Boxed)))))
     (params n)
     (body (term-ctor Boxed Boxed n (term-ctor List Nil)))))

examples/embed_export_multictor_rejected.ail

@@ -4,6 +4,6 @@
     (ctor R (con Float)))
   (fn f
     (export "f")
-    (type (fn-type (params (con Int)) (ret (con Either2))))
+    (type (fn-type (params (own (con Int))) (ret (own (con Either2)))))
     (params n)
     (body (term-ctor Either2 L n))))

examples/embed_export_record_ok.ail

@@ -5,8 +5,8 @@
     (export "step")
     (type
       (fn-type
-        (params (own (con State)) (con Float))
-        (ret (con State))))
+        (params (own (con State)) (own (con Float)))
+        (ret (own (con State)))))
     (params st sample)
     (body
       (match st

examples/embed_export_str_field_record_rejected.ail

@@ -3,6 +3,6 @@
     (ctor Tagged (con Int) (con Str)))
   (fn f
     (export "f")
-    (type (fn-type (params (con Int)) (ret (con Tagged))))
+    (type (fn-type (params (own (con Int))) (ret (own (con Tagged)))))
     (params n)
     (body (term-ctor Tagged Tagged n "x"))))

examples/embed_export_str_param_rejected.ail

@@ -3,7 +3,7 @@
     (export "f")
     (type
       (fn-type
-        (params (con Int) (con Str))
-        (ret (con Int))))
+        (params (own (con Int)) (own (con Str)))
+        (ret (own (con Int)))))
     (params n label)
     (body n)))

examples/embed_noentry_baseline.ail

@@ -2,8 +2,8 @@
   (fn helper
     (type
       (fn-type
-        (params (con Int))
-        (ret (con Int))))
+        (params (own (con Int)))
+        (ret (own (con Int)))))
     (params x)
     (body
       (app * x x))))

examples/embed_record_layout_carrier.ail

@@ -6,16 +6,16 @@
   (fn mk
     (type
       (fn-type
-        (params (con Int) (con Int))
-        (ret (con Pt))))
+        (params (own (con Int)) (own (con Int)))
+        (ret (own (con Pt)))))
     (params a b)
     (body (term-ctor Pt Pt a b)))
 
   (fn sum_pt
     (type
       (fn-type
-        (params (own (con Pt)))
-        (ret (con Int))))
+        (params (borrow (con Pt)))
+        (ret (own (con Int)))))
     (params p)
     (body
       (match p
@@ -23,7 +23,7 @@
           (app + x y)))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (let s (app int_to_str (app sum_pt (app mk 3 4)))

examples/eq_demo.ail

@@ -34,7 +34,7 @@
 
   (fn classify_str
     (doc "Lit-pattern over Str; exercises build_eq's class-dispatch lowering for non-Int.")
-    (type (fn-type (params (con Str)) (ret (con Int))))
+    (type (fn-type (params (own (con Str))) (ret (own (con Int)))))
     (params s)
     (body
       (match s
@@ -44,7 +44,7 @@
 
   (fn main
     (doc "Drive eq at Int/Bool/Str/Unit; then drive classify_str.")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (seq (seq (app print (app eq 5 5)) (do io/print_str "\n"))