diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index 0897878..34989c4 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -77,33 +77,78 @@ //! mode is explicit, we re-inspect each param annotated `(own T)`: //! //! - The uniqueness pass ([`crate::uniqueness::infer_module`]) gives -//! us the param's `consume_count`. -//! - If `consume_count == 0` AND the body never destructures the -//! param via `(match p ...)` (the latter is a *conservative cut* — -//! see below), the fn could have been written with `(borrow T)` -//! instead and would be cheaper to call (no inc/dec pair, no -//! rec-cascade at fn return). Emit `over-strict-mode` as a -//! `Severity::Warning` with a suggested fn-type rewrite. +//! us the param's `consume_count` and, importantly, the +//! `consume_count` of every pattern-binder introduced when the +//! param is matched on. +//! - If `consume_count(p) == 0` AND, for every `match p ...` in the +//! body, every pattern-binder bound by an arm of that match has +//! `consume_count == 0`, then the fn could have been written with +//! `(borrow T)` instead and would be cheaper to call (no inc/dec +//! pair, no rec-cascade at fn return). Emit `over-strict-mode` as +//! a `Severity::Warning` with a suggested fn-type rewrite. //! -//! ### Why the match-scrutinee carve-out is conservative +//! ### Iter 19a.1: precise sub-binder analysis //! -//! The precise rule would be "no consume of any sub-binder of `p`". -//! Implementing that requires an extra side-table tracking which -//! pattern-binders trace back to which scrutinee param — non-trivial -//! and out of scope for 19a. The conservative cut "no `match` with `p` -//! as scrutinee" is sound (it never warns when the precise rule -//! wouldn't) but incomplete (it misses some real over-strict fns -//! whose body matches on `p` but never moves a sub-binder out). The -//! incompleteness is acceptable because 19a is purely advisory: a -//! missed warning costs nothing; a spurious warning would be -//! actively misleading. The precise variant is queued for a follow-up. +//! 19a originally shipped a conservative cut ("any `match` whose +//! scrutinee is `p` silences the lint") because the precise check +//! seemed to require a new side-table. In practice the side-table +//! is already there: the uniqueness pass populates `consume_count` +//! for every binder including pattern-binders. 19a.1 replaces the +//! cut with a precise per-arm walk: for each `(match p ...)`, we +//! ask whether any **heap-typed** pattern-binder of any arm has +//! `consume_count > 0`. If yes, `(own T)` is genuinely needed and +//! the lint stays silent. If no, the param is purely read by the +//! match and the lint fires — exactly the shape of fixtures like +//! `rc_own_param_drop.head_or_zero` (which only returns the head +//! and never moves the tail). +//! +//! ### Why "heap-typed" matters +//! +//! A pattern-binder of primitive type (`Int` / `Bool` / `Str` / +//! `Unit`) being consumed does not force the scrutinee to be `Own` +//! — primitives are copied out by value, no RC operation is +//! involved. The uniqueness pass bumps `consume_count` for every +//! Consume-position read regardless of type, so the lint must +//! filter primitive-typed binders out via the pattern's parent +//! ctor field types. `head_or_zero`'s body +//! `match xs { Cons(h, t) => h }` returns `h: Int`; without the +//! filter, `h.consume_count == 1` would silence the lint. +//! +//! **Known debt: deeply-nested-match-on-sub-binder.** A pattern like +//! `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }` +//! has the inner match's scrutinee `t` (not `p`), so the inner-arm +//! binder `t2`'s consume is not seen when we ask "did any arm-binder +//! of `match p` get consumed?". The outer-arm binder `t` has +//! `consume_count == 0` (matching is Borrow), so the lint will fire +//! even though `(own T)` is genuinely needed because `t2` is +//! consumed. This is recorded in the JOURNAL as a follow-up; for the +//! current corpus it would cost a spurious warning rather than miss +//! a real one. use crate::diagnostic::Diagnostic; use crate::uniqueness::{infer_module as infer_uniqueness, UniquenessTable}; -use ailang_core::ast::{Arm, Def, FnDef, Module, ParamMode, Pattern, Term, Type}; +use ailang_core::ast::{Arm, Ctor, Def, FnDef, Module, ParamMode, Pattern, Term, Type}; use ailang_surface::{term_to_form_a, type_to_form_a}; use std::collections::HashMap; +/// Iter 19a.1: a `Type::Con` whose name is `Int`/`Bool`/`Str`/`Unit` +/// is a primitive value type — no RC, no heap. Reading a primitive +/// pattern-binder bumps `consume_count` in the uniqueness table but +/// does not force the scrutinee param to be `Own`. The lint filters +/// those out so a fn like `match xs { Cons(h, t) => h }` (where `h` +/// is `Int`) can still fire `over-strict-mode` when `t.consume_count +/// == 0`. +fn is_heap_type(t: &Type) -> bool { + match t { + Type::Con { name, .. } => !matches!(name.as_str(), "Int" | "Bool" | "Str" | "Unit"), + // Type::Var (a polymorphic param) is conservatively heap — + // it could instantiate to a heap type at the call site. + Type::Var { .. } => true, + Type::Fn { .. } => true, + Type::Forall { .. } => true, + } +} + /// Position in which a [`Term::Var`] is being used. See module-level /// docs for the propagation rules. #[derive(Copy, Clone, Debug, PartialEq, Eq)] @@ -140,6 +185,11 @@ struct BinderState { /// in source-order discovery (depth-first left-to-right walk). pub(crate) fn check_module(m: &Module) -> Vec { let mut globals: HashMap = HashMap::new(); + // Iter 19a.1: ctor name → field types, used by the + // `over-strict-mode` lint to filter out primitive-typed + // pattern-binders (Int / Bool / Str / Unit) — their consume + // does not force ownership of the scrutinee. + let mut ctors: HashMap> = HashMap::new(); for def in &m.defs { match def { Def::Fn(f) => { @@ -149,7 +199,12 @@ pub(crate) fn check_module(m: &Module) -> Vec { Def::Const(c) => { globals.insert(c.name.clone(), strip_forall(&c.ty).clone()); } - Def::Type(_) => {} + Def::Type(td) => { + for c in &td.ctors { + let Ctor { name, fields } = c; + ctors.insert(name.clone(), fields.clone()); + } + } } } @@ -162,7 +217,7 @@ pub(crate) fn check_module(m: &Module) -> Vec { let mut diags = Vec::new(); for def in &m.defs { if let Def::Fn(f) = def { - check_fn(f, &globals, &uniq, &mut diags); + check_fn(f, &globals, &ctors, &uniq, &mut diags); } } diags @@ -183,6 +238,7 @@ fn strip_forall(t: &Type) -> &Type { fn check_fn( f: &FnDef, globals: &HashMap, + ctors: &HashMap>, uniq: &UniquenessTable, diags: &mut Vec, ) { @@ -230,19 +286,18 @@ fn check_fn( checker.walk(&f.body, Position::Consume); - // Iter 19a: `over-strict-mode` lint. After the linearity walk has - // completed (and any errors have been recorded), inspect each - // `Own`-annotated param: if `consume_count == 0` AND no `match` - // in the body uses the param as scrutinee, the param could be - // re-annotated `Borrow`. Emit a Warning with a form-A rewrite. + // Iter 19a / 19a.1: `over-strict-mode` lint. After the linearity + // walk has completed (and any errors have been recorded), inspect + // each `Own`-annotated param: if `consume_count(p) == 0` AND no + // pattern-binder of any `(match p ...)` arm in the body has + // `consume_count > 0`, the param could be re-annotated `Borrow`. + // Emit a Warning with a form-A rewrite. // - // Conservative match-scrutinee carve-out: matching on `p` may - // move sub-binders out of `p`'s active ctor, in which case - // `(borrow T)` would *not* suffice — the callee needs `Own` to - // legitimise the sub-consume. The precise rule would inspect the - // arm bodies for sub-binder consumes; the conservative rule - // skips any fn that matches on the param at all. See - // module-level docs for the rationale. + // The precise sub-binder check (19a.1) replaces 19a's + // conservative "any match on `p` silences" cut: matching on `p` + // 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. for (i, mode) in param_modes.iter().enumerate() { if !matches!(mode, ParamMode::Own) { continue; @@ -255,9 +310,9 @@ fn check_fn( if consume_count != 0 { continue; } - if body_matches_on(&f.body, pname) { - // Conservative cut: a `match` whose scrutinee is `pname` - // may move out a sub-binder; staying silent is safe. + if any_sub_binder_consumed_for(&f.body, pname, uniq, &f.name, ctors) { + // A pattern-binder of some `(match p ...)` arm is + // consumed → `(own T)` is genuinely needed. Stay silent. continue; } diags.push(make_over_strict_mode(&f.name, pname, inner, i)); @@ -682,52 +737,158 @@ fn make_use_after_consume_at_reuse_as(def: &str, binder: &str, body: &Term) -> D ) } -/// Iter 19a: returns `true` if any sub-term of `t` is a -/// `Term::Match` whose scrutinee is a bare `Var { name: pname }` (or -/// a `Term::Clone` thereof — clone-then-match is the same shape for -/// the purposes of the carve-out, since both forms read the binder -/// without consuming it but expose its sub-binders to the arms). +/// Iter 19a.1: precise sub-binder check for the over-strict-mode +/// lint. Returns `true` iff some `(match p ...)` somewhere in `t`, +/// where `p` is the param `pname`, has an arm whose pattern-binders +/// include at least one binder with `consume_count > 0` in the +/// uniqueness side table. /// -/// Used by the over-strict-mode lint as a conservative gate: matching -/// on `p` *may* move out a sub-binder of `p` — in which case `(own T)` -/// is genuinely needed and `(borrow T)` would not suffice. We don't -/// yet inspect the arms to refine the answer; any such match silences -/// the lint for `pname`. -fn body_matches_on(t: &Term, pname: &str) -> bool { +/// "Match on `p`" includes `(match p ...)` and +/// `(match (clone p) ...)` — both expose `p`'s sub-binders to the +/// arms. +/// +/// Walks every other Term variant looking for further matches; a +/// `match p ...` may sit arbitrarily deep inside `If` / `Let` / +/// `App` / etc. +/// +/// **Known limit (recorded as debt in JOURNAL.md):** if an arm's +/// body contains a *nested* match on a sub-binder of `p` (e.g. +/// `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }`), +/// we only check `t.consume_count`, not `t2.consume_count`. The +/// inner match's scrutinee is `t`, not `p`, and our recursion looks +/// for `match-on-pname`, so we miss `t2`. For the current corpus +/// this would mean a *spurious* warning (the lint fires but `(own)` +/// is genuinely needed), not a missed one. The fix is to either +/// chase pattern-binder lineage or to check inner matches whose +/// scrutinee transitively traces back to `p`. +fn any_sub_binder_consumed_for( + t: &Term, + pname: &str, + uniq: &UniquenessTable, + def_name: &str, + ctors: &HashMap>, +) -> bool { match t { Term::Lit { .. } | Term::Var { .. } => false, Term::Match { scrutinee, arms } => { if scrutinee_matches_param(scrutinee, pname) { - return true; + for arm in arms { + if pattern_has_consumed_heap_binder(&arm.pat, uniq, def_name, ctors) { + return true; + } + // Recurse into the arm body: a deeper + // `match p ...` could also count. + if any_sub_binder_consumed_for(&arm.body, pname, uniq, def_name, ctors) { + return true; + } + } + false + } else { + // The scrutinee isn't `p`, but `p` could still be + // matched-on inside the scrutinee or inside any arm. + if any_sub_binder_consumed_for(scrutinee, pname, uniq, def_name, ctors) { + return true; + } + arms.iter() + .any(|a| any_sub_binder_consumed_for(&a.body, pname, uniq, def_name, ctors)) } - arms.iter().any(|a| body_matches_on(&a.body, pname)) - || body_matches_on(scrutinee, pname) } Term::App { callee, args, .. } => { - body_matches_on(callee, pname) || args.iter().any(|a| body_matches_on(a, pname)) + any_sub_binder_consumed_for(callee, pname, uniq, def_name, ctors) + || args + .iter() + .any(|a| any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)) } Term::Let { value, body, .. } => { - body_matches_on(value, pname) || body_matches_on(body, pname) + any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors) + || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors) } Term::LetRec { body, in_term, .. } => { - // The recursive fn's body and the continuation can both - // shadow `pname`; we ignore shadowing here — the lint - // is allowed to be over-cautious. - body_matches_on(body, pname) || body_matches_on(in_term, pname) + any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors) + || any_sub_binder_consumed_for(in_term, pname, uniq, def_name, ctors) } Term::If { cond, then, else_ } => { - body_matches_on(cond, pname) - || body_matches_on(then, pname) - || body_matches_on(else_, pname) + any_sub_binder_consumed_for(cond, pname, uniq, def_name, ctors) + || any_sub_binder_consumed_for(then, pname, uniq, def_name, ctors) + || any_sub_binder_consumed_for(else_, pname, uniq, def_name, ctors) } - Term::Seq { lhs, rhs } => body_matches_on(lhs, pname) || body_matches_on(rhs, pname), - Term::Ctor { args, .. } | Term::Do { args, .. } => { - args.iter().any(|a| body_matches_on(a, pname)) + Term::Seq { lhs, rhs } => { + any_sub_binder_consumed_for(lhs, pname, uniq, def_name, ctors) + || any_sub_binder_consumed_for(rhs, pname, uniq, def_name, ctors) } - Term::Lam { body, .. } => body_matches_on(body, pname), - Term::Clone { value } => body_matches_on(value, pname), + Term::Ctor { args, .. } | Term::Do { args, .. } => args + .iter() + .any(|a| any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)), + Term::Lam { body, .. } => any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors), + Term::Clone { value } => any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors), Term::ReuseAs { source, body } => { - body_matches_on(source, pname) || body_matches_on(body, pname) + any_sub_binder_consumed_for(source, pname, uniq, def_name, ctors) + || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors) + } + } +} + +/// Iter 19a.1: returns `true` if `pat` introduces any **heap-typed** +/// binder whose recorded `consume_count` is `> 0`. Primitive-typed +/// pattern-binders (`Int` / `Bool` / `Str` / `Unit`) never count +/// because reading a primitive does not force the scrutinee to be +/// `Own` — the value is copied, not moved out of the scrutinee's +/// allocation. This is the key reason `match xs { Cons(h, t) => h }` +/// (head_or_zero) fires the lint: `h: Int` is filtered out, `t: +/// IntList` has `consume_count == 0`. +/// +/// Walks `Pattern::Ctor` recursively. After 16a's desugar pass, +/// top-level patterns under a Ctor field are flattened into separate +/// matches — but the recursion is defensive (cheap and correct under +/// any pattern shape; nested binders are looked up by their own name +/// in `uniq`, regardless of their pattern depth). +fn pattern_has_consumed_heap_binder( + pat: &Pattern, + uniq: &UniquenessTable, + def_name: &str, + ctors: &HashMap>, +) -> bool { + pattern_has_consumed_heap_binder_at(pat, None, uniq, def_name, ctors) +} + +/// Iter 19a.1: helper carrying the optional declared type of `pat`. +/// At the top of an arm pattern, `declared_ty` is `None` (we don't +/// track the scrutinee's type in the lint); the type becomes known +/// when we descend into a `Pattern::Ctor`'s fields, where the +/// ctor's `Ctor::fields[i]` gives `fields[i]`'s type. +/// +/// For a `Pattern::Var { name }` with `declared_ty == None`, we +/// conservatively treat the binder as heap (we don't know its +/// type from the pattern alone). For `declared_ty == Some(t)`, we +/// only count the binder if `is_heap_type(t)`. +fn pattern_has_consumed_heap_binder_at( + pat: &Pattern, + declared_ty: Option<&Type>, + uniq: &UniquenessTable, + def_name: &str, + ctors: &HashMap>, +) -> bool { + match pat { + Pattern::Wild | Pattern::Lit { .. } => false, + Pattern::Var { name } => { + // Conservative when type unknown: assume heap. + let counts = match declared_ty { + Some(t) => is_heap_type(t), + None => true, + }; + if !counts { + return false; + } + uniq.get(&(def_name.to_string(), name.clone())) + .map(|info| info.consume_count > 0) + .unwrap_or(false) + } + Pattern::Ctor { ctor, fields } => { + let field_tys: &[Type] = ctors.get(ctor).map(|v| v.as_slice()).unwrap_or(&[]); + fields.iter().enumerate().any(|(i, f)| { + let ty = field_tys.get(i); + pattern_has_consumed_heap_binder_at(f, ty, uniq, def_name, ctors) + }) } } } @@ -1090,20 +1251,16 @@ mod tests { ); } - /// Iter 19a, conservatism marker: a fn with `(own T)` whose body - /// is `(match p0 ...)` and never consumes `p0` directly nor any - /// of `p0`'s sub-binders does NOT fire `over-strict-mode` in the - /// conservative cut. This is a known false-negative; the - /// precise variant (which would fire here) is queued for a - /// follow-up. Keep this test as a TODO marker — flipping it - /// to `assert!(some-warning)` is the signal that the precise - /// variant has shipped. + /// Iter 19a.1, positive: a fn with `(own T)` whose body is + /// `(match p0 ...)` and never consumes `p0` directly nor any of + /// `p0`'s sub-binders DOES fire `over-strict-mode` under the + /// precise sub-binder analysis. This is the test that 19a left + /// pinned as a TODO marker; 19a.1 flipped it from a negative to + /// a positive assertion. #[test] - fn over_strict_mode_conservative_skips_match_on_param() { + fn over_strict_mode_fires_when_match_arm_uses_no_sub_binder() { // Body: (match p0 ((pat-wild) 0)) - // — sub-binders are absent; the param is only read. The - // precise rule would fire here. The conservative rule - // silences any `match` whose scrutinee is the param. + // — no sub-binders are bound; the param is only read. let body = Term::Match { scrutinee: Box::new(Term::Var { name: "p0".into() }), arms: vec![Arm { @@ -1118,9 +1275,147 @@ mod tests { defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)], }; let diags = check_module(&m); + let osm: Vec<_> = diags.iter().filter(|d| d.code == "over-strict-mode").collect(); + assert_eq!( + osm.len(), + 1, + "precise rule: expected one over-strict-mode warning when the body matches on `p0` and binds no sub-consume; got {diags:?}" + ); + assert_eq!(osm[0].severity, Severity::Warning); + assert_eq!(osm[0].def.as_deref(), Some("f")); + } + + /// Iter 19a.1: helper to build an `IntList = Nil | Cons(Int, + /// IntList)` ADT def. Used by the head_or_zero-shape tests + /// (positive + negative variants below) so the lint can look up + /// each ctor field's type and filter out primitives. + fn intlist_typedef() -> Def { + Def::Type(ailang_core::ast::TypeDef { + name: "IntList".into(), + vars: vec![], + ctors: vec![ + Ctor { name: "Nil".into(), fields: vec![] }, + Ctor { + name: "Cons".into(), + fields: vec![ + Type::int(), + Type::Con { name: "IntList".into(), args: vec![] }, + ], + }, + ], + doc: None, + drop_iterative: false, + }) + } + + /// Iter 19a.1: helper to build a fn whose single param is + /// `(own IntList)` and whose body is `body`. Distinct from + /// `fn_with_modes` (which uses a generic `List` type for params) + /// so the test exercises a real ctor-field-types lookup. + fn fn_own_intlist(name: &str, body: Term) -> Def { + Def::Fn(FnDef { + name: name.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::Implicit, + effects: vec![], + }, + params: vec!["xs".into()], + body, + doc: None, + }) + } + + /// Iter 19a.1, negative: a fn with `(own IntList)` whose body + /// is `match xs { Cons(h, t) => t }` consumes the *heap-typed* + /// pattern-binder `t`. The lint must NOT fire — the + /// sub-consume forces ownership. + #[test] + fn over_strict_mode_silent_when_match_arm_consumes_sub_binder() { + // Body: (match xs ((pat-ctor Cons (pat-var h) (pat-var t)) t)) + let body = Term::Match { + scrutinee: Box::new(Term::Var { name: "xs".into() }), + arms: vec![Arm { + pat: Pattern::Ctor { + ctor: "Cons".into(), + fields: vec![ + Pattern::Var { name: "h".into() }, + Pattern::Var { name: "t".into() }, + ], + }, + body: Term::Var { name: "t".into() }, + }], + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![intlist_typedef(), fn_own_intlist("f", body)], + }; + let diags = check_module(&m); assert!( !diags.iter().any(|d| d.code == "over-strict-mode"), - "conservative cut: no over-strict-mode expected when the body matches on the param; got {diags:?}" + "no over-strict-mode expected when a heap-typed arm-binder is consumed; got {diags:?}" + ); + } + + /// Iter 19a.1, positive: a fn with `(own IntList)` whose body + /// is `match xs { Nil => 0, Cons(h, t) => h }` returns the + /// **primitive-typed** `h` (`Int`) and never moves the + /// heap-typed `t`. The lint MUST fire — `(borrow IntList)` + /// would have sufficed. This is exactly + /// `rc_own_param_drop.head_or_zero`'s shape. + #[test] + fn over_strict_mode_fires_when_match_arm_binders_unused() { + // Body: (match xs + // ((pat-ctor Nil) 0) + // ((pat-ctor Cons (pat-var h) (pat-var t)) h)) + let body = Term::Match { + scrutinee: Box::new(Term::Var { name: "xs".into() }), + arms: vec![ + Arm { + pat: Pattern::Ctor { + ctor: "Nil".into(), + fields: vec![], + }, + body: Term::Lit { lit: Literal::Int { value: 0 } }, + }, + Arm { + pat: Pattern::Ctor { + ctor: "Cons".into(), + fields: vec![ + Pattern::Var { name: "h".into() }, + Pattern::Var { name: "t".into() }, + ], + }, + body: Term::Var { name: "h".into() }, + }, + ], + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![intlist_typedef(), fn_own_intlist("f", body)], + }; + let diags = check_module(&m); + let osm: Vec<_> = diags.iter().filter(|d| d.code == "over-strict-mode").collect(); + assert_eq!( + osm.len(), + 1, + "expected one over-strict-mode warning (head_or_zero shape); got {diags:?}" + ); + assert_eq!(osm[0].severity, Severity::Warning); + assert_eq!(osm[0].def.as_deref(), Some("f")); + assert_eq!( + osm[0].ctx, + serde_json::json!({ + "binder": "xs", + "current_mode": "own", + "suggested_mode": "borrow", + }) ); } } diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 4734cff..165745d 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -9244,3 +9244,94 @@ JOURNAL queue: empty again. - `docs/JOURNAL.md` — this entry. No code changes. Build/test status unchanged from 20d (green). + +## 2026-05-08 — Iter 19a.1: precise sub-binder analysis (corpus-driven upgrade) + +The 19a-shipping entry queued a sub-binder-precise variant for "if +real-corpus signal warrants." I (orchestrator) ran 19a's lint +across all 65 fixtures: **zero warnings fired**. The conservative +match-scrutinee carve-out filtered every `(own T)` param because +every such fixture's body destructures the param via `match` — +even ones that are deliberately over-strict (RC codegen-test +fixtures like `head_or_zero` and `use_first`). The conservative +cut wasn't "incomplete but valuable"; it was "silent in the only +shapes the corpus actually produces." Real-corpus signal warranted. + +### Precise rule + +For an `Own` param `p` with `consume_count == 0`: + + - For every match arm whose scrutinee is `p`, look at each + pattern-binder. + - If any **heap-typed** pattern-binder has `consume_count > 0`, + `p` must be `Own` (sub-consume forces ownership). Lint stays + silent. + - Otherwise, lint fires. + +### The heap-type filter (design call by implementer) + +The orchestrator's literal brief said "any pattern-binder +`consume_count > 0` → silent." That contradicted the brief's own +positive test (`head_or_zero` MUST fire), because `match xs { +Cons(h, t) => h }` records `consume_count(h) == 1` regardless of +`h: Int` being a primitive. Implementer caught this, made the +design call, documented it in the module-doc rationale. + +The semantic justification: reading a primitive (`h: Int`) is a +load-by-value, no RC traffic, no heap data moved out of the +scrutinee's allocation. Reading a heap-typed sub-binder +(`t: IntList`) IS a heap-pointer move that requires owning the +outer cell. So the filter — "skip primitive-typed pattern-binders +when judging sub-consume" — is exactly what makes the lint +correct. + +This is a real design point that 19a's brief did not document. +Recording it here as a ratification of the implementer's call. + +### Corpus signal after upgrade + +Five of 65 fixtures now produce at least one `over-strict-mode` +warning: + + - `rc_app_let_partial_drop_leak` + - `rc_drop_iterative_long_list` + - `rc_match_arm_partial_drop_leak` + - `rc_own_param_drop` + - `rc_own_param_partial_drop_leak` + +All five are RC codegen-test fixtures — the `(own T)` annotation +is intentional, used to exercise the codegen path that drops Own- +params at fn return / arm close. They are NOT incorrect annotations; +they are deliberate test infrastructure. + +This is the signal that **justifies 19b** (`mode-strict-because` +suppression). Without it, every RC-codegen-test fixture would +permanently emit a warning despite being correct-by-design. With +it, each fixture annotates its strictness intentionally, the +warning suppresses, future-LLM reads the reason, future-iter +edits know whether to preserve or relax. + +19b is dispatched next. + +### Known debt + +**Deeply-nested-match-on-sub-binder** (recorded by implementer in +the module doc): `match p { Ctor(_, t) => match t { Ctor(_, t2) +=> consume(t2) } }` would produce a *spurious* warning under the +current rule — `t.consume_count == 0` (matching is Borrow), so +the inner consume of `t2` doesn't propagate up to `p`'s view. +None of the 65 fixtures hit this shape; queued for follow-up if +real corpus surfaces it. + +### Files / tests + + - `crates/ailang-check/src/linearity.rs` — module-doc § 19a.1 + rationale, `is_heap_type` helper, `any_sub_binder_consumed_for` + + `pattern_has_consumed_heap_binder` walkers, ctor-table + threading through `check_module` / `check_fn`. + - Tests: `over_strict_mode_conservative_skips_match_on_param` + flipped to positive `over_strict_mode_fires_when_match_arm_uses_no_sub_binder`. + New `over_strict_mode_silent_when_match_arm_consumes_sub_binder` + and `over_strict_mode_fires_when_match_arm_binders_unused`. + +`ailang-check` test count: 53 → 55. Workspace build/test green.