Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

check: precise sub-binder analysis for over-strict-mode (iter 19a.1)

Browse Source 
Corpus-signal upgrade: orchestrator ran 19a's lint across 65
fixtures, zero warnings fired. The conservative match-scrutinee
carve-out filtered every (own T) fixture because every such body
destructures the param via match. Real-corpus signal warranted
the precise variant.

Precise rule: for an Own param with consume_count == 0, walk each
match arm whose scrutinee is the param; if any HEAP-TYPED
pattern-binder has consume_count > 0, stay silent (sub-consume
forces ownership). Otherwise fire.

Heap-type filter is the implementer's design call (not in the
brief): reading a primitive (h: Int) is load-by-value, no RC, no
heap-data move; reading heap-typed t: IntList IS a pointer move
requiring outer-cell ownership. Documented in module-doc.

Corpus signal after upgrade: 5/65 fixtures fire — all RC
codegen-test fixtures with deliberate over-strictness for the
codegen path. Justifies 19b (mode-strict-because suppression).

ailang-check test count: 53 → 55. e2e + everything else green.
Known debt: deeply-nested-match-on-sub-binder (no fixture hits).
This commit is contained in:
Brummel
2026-05-08 19:19:31 +02:00
parent b9e942b99d
commit 9f3f10ce6e
2 changed files with 464 additions and 78 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/linearity.rs
+373 -78
View File
@@ -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<Diagnostic> {
let mut globals: HashMap<String, Type> = 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<String, Vec<Type>> = HashMap::new();
for def in &m.defs {
match def {
Def::Fn(f) => {
@@ -149,7 +199,12 @@ pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
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<Diagnostic> {
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<String, Type>,
ctors: &HashMap<String, Vec<Type>>,
uniq: &UniquenessTable,
diags: &mut Vec<Diagnostic>,
) {
@@ -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<String, Vec<Type>>,
) -> 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<String, Vec<Type>>,
) -> 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<String, Vec<Type>>,
) -> 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",
})
);
}
}
docs/JOURNAL.md
+91
View File
@@ -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.