check: over-strict-mode lint (iter 19a)
When a fn-param is annotated (own T) but the body never consumes it (consume_count == 0) and never destructures it via match, the linearity pass now emits a Severity::Warning diagnostic with a form-A-rendered (borrow T) rewrite as suggested_rewrite. Pure advisory, Decision 10 unchanged. First Warning-severity diagnostic the typechecker emits; three CLI exit paths gated on Error-only. JOURNAL: design entry + iter 19a shipping entry.
This commit is contained in:
+26
-3
@@ -399,7 +399,16 @@ fn main() -> Result<()> {
|
||||
d.message,
|
||||
);
|
||||
}
|
||||
std::process::exit(1);
|
||||
// Iter 19a: only Error-severity diagnostics fail the
|
||||
// command. Warning-severity diagnostics (e.g. the
|
||||
// `over-strict-mode` lint) print to stderr but the
|
||||
// module is still considered to have typechecked.
|
||||
if diags
|
||||
.iter()
|
||||
.any(|d| matches!(d.severity, ailang_check::Severity::Error))
|
||||
{
|
||||
std::process::exit(1);
|
||||
}
|
||||
}
|
||||
let total: usize = ws.modules.values().map(|m| m.defs.len()).sum();
|
||||
println!(
|
||||
@@ -430,7 +439,13 @@ fn main() -> Result<()> {
|
||||
d.message,
|
||||
);
|
||||
}
|
||||
std::process::exit(1);
|
||||
// Iter 19a: only Error-severity blocks codegen.
|
||||
if diags
|
||||
.iter()
|
||||
.any(|d| matches!(d.severity, ailang_check::Severity::Error))
|
||||
{
|
||||
std::process::exit(1);
|
||||
}
|
||||
}
|
||||
let ir = ailang_codegen::lower_workspace(&ws)?;
|
||||
match out {
|
||||
@@ -1653,7 +1668,15 @@ fn build_to(
|
||||
d.message,
|
||||
);
|
||||
}
|
||||
std::process::exit(1);
|
||||
// Iter 19a: only Error-severity blocks the build. Warning-
|
||||
// severity diagnostics (e.g. `over-strict-mode`) print but
|
||||
// do not abort.
|
||||
if diags
|
||||
.iter()
|
||||
.any(|d| matches!(d.severity, ailang_check::Severity::Error))
|
||||
{
|
||||
std::process::exit(1);
|
||||
}
|
||||
}
|
||||
// Iter 16b.3: run `lift_letrecs` per module on the post-desugar
|
||||
// form. Codegen's internal desugar pass is idempotent on a
|
||||
|
||||
@@ -46,6 +46,14 @@
|
||||
//! spell the fix in form-A AILang.
|
||||
//! - `consume-while-borrowed` — `ctx`: `{"binder": "<n>"}` (Iter 18c.2);
|
||||
//! ditto on `suggested_rewrites`.
|
||||
//! - `over-strict-mode` (Iter 19a) — `severity: warning`. Emitted by
|
||||
//! the linearity pass when a fn parameter is annotated `(own T)` but
|
||||
//! the body never consumes it (and never destructures it via
|
||||
//! `match`). `ctx`: `{"binder": "<n>", "current_mode": "own",
|
||||
//! "suggested_mode": "borrow"}`. Carries one
|
||||
//! [`SuggestedRewrite`] whose `replacement` is the relaxed
|
||||
//! `(fn-type ...)` in form-A. Pure advisory; the typechecker still
|
||||
//! accepts the original signature.
|
||||
|
||||
use serde::Serialize;
|
||||
|
||||
@@ -53,15 +61,16 @@ use serde::Serialize;
|
||||
///
|
||||
/// Serializes as a lowercase string (`"error"` / `"warning"`) so that
|
||||
/// `ail check --json` consumers can branch on it without parsing prose.
|
||||
/// The MVP only emits [`Severity::Error`]; [`Severity::Warning`] is
|
||||
/// reserved for future lints.
|
||||
/// Iter 19a is the first iter to emit [`Severity::Warning`] (via the
|
||||
/// linearity-pass `over-strict-mode` lint); pre-19a the variant was
|
||||
/// reserved.
|
||||
#[derive(Serialize, Debug, Clone, Copy, PartialEq, Eq)]
|
||||
#[serde(rename_all = "lowercase")]
|
||||
pub enum Severity {
|
||||
/// Hard failure. The module did not typecheck.
|
||||
Error,
|
||||
/// Non-fatal observation. Reserved; the typechecker does not emit
|
||||
/// warnings yet.
|
||||
/// Non-fatal observation. Module typechecked; the lint is
|
||||
/// advisory.
|
||||
Warning,
|
||||
}
|
||||
|
||||
@@ -131,6 +140,22 @@ impl Diagnostic {
|
||||
}
|
||||
}
|
||||
|
||||
/// Iter 19a: builds a [`Severity::Warning`] diagnostic. Same shape
|
||||
/// as [`Diagnostic::error`] otherwise. Used by lint-style passes
|
||||
/// that report observations rather than hard typecheck failures
|
||||
/// (currently the only emitter is the linearity pass's
|
||||
/// `over-strict-mode` lint).
|
||||
pub fn warning(code: impl Into<String>, message: impl Into<String>) -> Self {
|
||||
Self {
|
||||
severity: Severity::Warning,
|
||||
code: code.into(),
|
||||
message: message.into(),
|
||||
def: None,
|
||||
ctx: serde_json::Value::Object(serde_json::Map::new()),
|
||||
suggested_rewrites: Vec::new(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Iter 18c.2: append a [`SuggestedRewrite`]. Builder-style. Used by
|
||||
/// the linearity check to attach the form-A fix it computed. Other
|
||||
/// diagnostics leave the field empty.
|
||||
|
||||
@@ -70,10 +70,38 @@
|
||||
//! the unique consume.
|
||||
//! - `consume-while-borrowed` on `Var x`: replacement `(clone <name>)`
|
||||
//! — the author should clone here so the original keeps the borrow.
|
||||
//!
|
||||
//! ## Iter 19a: `over-strict-mode` lint
|
||||
//!
|
||||
//! After the linearity walk has finished for a fn whose every param
|
||||
//! 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.
|
||||
//!
|
||||
//! ### Why the match-scrutinee carve-out is conservative
|
||||
//!
|
||||
//! 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.
|
||||
|
||||
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_surface::term_to_form_a;
|
||||
use ailang_surface::{term_to_form_a, type_to_form_a};
|
||||
use std::collections::HashMap;
|
||||
|
||||
/// Position in which a [`Term::Var`] is being used. See module-level
|
||||
@@ -125,10 +153,16 @@ pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
|
||||
}
|
||||
}
|
||||
|
||||
// Iter 19a: the over-strict-mode lint reads `consume_count` from
|
||||
// the uniqueness side table. Build it once for the whole module;
|
||||
// reusing the existing pass keeps the "what counts as a consume"
|
||||
// definition in a single place.
|
||||
let uniq = infer_uniqueness(m);
|
||||
|
||||
let mut diags = Vec::new();
|
||||
for def in &m.defs {
|
||||
if let Def::Fn(f) = def {
|
||||
check_fn(f, &globals, &mut diags);
|
||||
check_fn(f, &globals, &uniq, &mut diags);
|
||||
}
|
||||
}
|
||||
diags
|
||||
@@ -146,7 +180,12 @@ fn strip_forall(t: &Type) -> &Type {
|
||||
|
||||
/// Per-fn check. Skips fns whose signature has any `Implicit` param —
|
||||
/// see module-level scope rules.
|
||||
fn check_fn(f: &FnDef, globals: &HashMap<String, Type>, diags: &mut Vec<Diagnostic>) {
|
||||
fn check_fn(
|
||||
f: &FnDef,
|
||||
globals: &HashMap<String, Type>,
|
||||
uniq: &UniquenessTable,
|
||||
diags: &mut Vec<Diagnostic>,
|
||||
) {
|
||||
let inner = strip_forall(&f.ty);
|
||||
let (param_tys, param_modes) = match inner {
|
||||
Type::Fn { params, param_modes, .. } => (params.as_slice(), param_modes.as_slice()),
|
||||
@@ -190,6 +229,39 @@ fn check_fn(f: &FnDef, globals: &HashMap<String, Type>, diags: &mut Vec<Diagnost
|
||||
}
|
||||
|
||||
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.
|
||||
//
|
||||
// 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.
|
||||
for (i, mode) in param_modes.iter().enumerate() {
|
||||
if !matches!(mode, ParamMode::Own) {
|
||||
continue;
|
||||
}
|
||||
let pname = &f.params[i];
|
||||
let consume_count = uniq
|
||||
.get(&(f.name.clone(), pname.clone()))
|
||||
.map(|info| info.consume_count)
|
||||
.unwrap_or(0);
|
||||
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.
|
||||
continue;
|
||||
}
|
||||
diags.push(make_over_strict_mode(&f.name, pname, inner, i));
|
||||
}
|
||||
}
|
||||
|
||||
/// Per-fn linearity walker.
|
||||
@@ -610,6 +682,130 @@ 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).
|
||||
///
|
||||
/// 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 t {
|
||||
Term::Lit { .. } | Term::Var { .. } => false,
|
||||
Term::Match { scrutinee, arms } => {
|
||||
if scrutinee_matches_param(scrutinee, pname) {
|
||||
return true;
|
||||
}
|
||||
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))
|
||||
}
|
||||
Term::Let { value, body, .. } => {
|
||||
body_matches_on(value, pname) || body_matches_on(body, pname)
|
||||
}
|
||||
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)
|
||||
}
|
||||
Term::If { cond, then, else_ } => {
|
||||
body_matches_on(cond, pname)
|
||||
|| body_matches_on(then, pname)
|
||||
|| body_matches_on(else_, pname)
|
||||
}
|
||||
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::Lam { body, .. } => body_matches_on(body, pname),
|
||||
Term::Clone { value } => body_matches_on(value, pname),
|
||||
Term::ReuseAs { source, body } => {
|
||||
body_matches_on(source, pname) || body_matches_on(body, pname)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Iter 19a: a scrutinee "is" `pname` if it's a bare `Var { pname }`
|
||||
/// or `Clone(Var { pname })`. Anything else (a fresh App result, a
|
||||
/// let-binder, …) does not put `pname` directly in scrutinee
|
||||
/// position.
|
||||
fn scrutinee_matches_param(scrutinee: &Term, pname: &str) -> bool {
|
||||
match scrutinee {
|
||||
Term::Var { name } => name == pname,
|
||||
Term::Clone { value } => scrutinee_matches_param(value, pname),
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
|
||||
/// Iter 19a: build the `over-strict-mode` warning. `inner` is the
|
||||
/// fn-type with the original mode; we synthesise a relaxed copy with
|
||||
/// `param_modes[i] = Borrow` and render it through
|
||||
/// [`type_to_form_a`] to produce the suggested rewrite.
|
||||
fn make_over_strict_mode(def: &str, binder: &str, inner: &Type, i: usize) -> Diagnostic {
|
||||
let relaxed = relax_param_to_borrow(inner, i);
|
||||
let replacement = type_to_form_a(&relaxed);
|
||||
Diagnostic::warning(
|
||||
"over-strict-mode",
|
||||
format!(
|
||||
"param `{binder}` is annotated `(own ...)` but the body does not consume it; `(borrow ...)` would suffice"
|
||||
),
|
||||
)
|
||||
.with_def(def)
|
||||
.with_ctx(serde_json::json!({
|
||||
"binder": binder,
|
||||
"current_mode": "own",
|
||||
"suggested_mode": "borrow",
|
||||
}))
|
||||
.with_suggested_rewrite(
|
||||
format!("relax param `{binder}` mode from `(own ...)` to `(borrow ...)`"),
|
||||
replacement,
|
||||
)
|
||||
}
|
||||
|
||||
/// Iter 19a: clone of `inner` (assumed `Type::Fn`) with
|
||||
/// `param_modes[i]` rewritten to `ParamMode::Borrow`. Other slots
|
||||
/// are preserved bit-for-bit. Falls back to returning `inner`
|
||||
/// unchanged if `inner` is not a `Type::Fn` (defensive — caller
|
||||
/// should have screened this).
|
||||
fn relax_param_to_borrow(inner: &Type, i: usize) -> Type {
|
||||
match inner {
|
||||
Type::Fn {
|
||||
params,
|
||||
param_modes,
|
||||
ret,
|
||||
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();
|
||||
if i < new_modes.len() {
|
||||
new_modes[i] = ParamMode::Borrow;
|
||||
}
|
||||
Type::Fn {
|
||||
params: params.clone(),
|
||||
param_modes: new_modes,
|
||||
ret: ret.clone(),
|
||||
ret_mode: *ret_mode,
|
||||
effects: effects.clone(),
|
||||
}
|
||||
}
|
||||
other => other.clone(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Build a `consume-while-borrowed` diagnostic for `binder` in `def`.
|
||||
/// Suggested rewrite: clone here so the original retains the borrow.
|
||||
fn make_consume_while_borrowed(def: &str, binder: &str) -> Diagnostic {
|
||||
@@ -688,7 +884,11 @@ mod tests {
|
||||
assert!(check_module(&m).is_empty());
|
||||
}
|
||||
|
||||
/// All-explicit fn that NEVER uses its params: clean.
|
||||
/// All-explicit fn that NEVER uses its params, annotated `Borrow`:
|
||||
/// clean. (Pre-19a this test exercised the same shape with `Own`
|
||||
/// and asserted clean; 19a's `over-strict-mode` lint now fires on
|
||||
/// `Own` + zero-consume — moved into a dedicated positive test
|
||||
/// below. With `Borrow`, the lint does not apply.)
|
||||
#[test]
|
||||
fn explicit_fn_with_no_uses_is_clean() {
|
||||
let m = Module {
|
||||
@@ -697,7 +897,7 @@ mod tests {
|
||||
imports: vec![],
|
||||
defs: vec![fn_with_modes(
|
||||
"f",
|
||||
vec![ParamMode::Own],
|
||||
vec![ParamMode::Borrow],
|
||||
Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
)],
|
||||
};
|
||||
@@ -772,4 +972,155 @@ mod tests {
|
||||
assert_eq!(d.code, "use-after-consume");
|
||||
assert_eq!(d.ctx, serde_json::json!({"binder": "p0"}));
|
||||
}
|
||||
|
||||
// ---- Iter 19a: over-strict-mode -----------------------------------
|
||||
|
||||
use crate::diagnostic::Severity;
|
||||
|
||||
/// Iter 19a, positive: a fn with `(own T)` whose body merely
|
||||
/// borrows the param via a `Borrow`-mode call → fires
|
||||
/// `over-strict-mode` (Warning) with binder=p0, current=own,
|
||||
/// suggested=borrow, and a non-empty rewrite.
|
||||
#[test]
|
||||
fn over_strict_mode_fires_when_param_only_borrowed() {
|
||||
// Module shape:
|
||||
// (fn read (params (borrow (con List))) ... ) ; helper, body irrelevant
|
||||
// (fn f (params (own (con List))) ; over-strict
|
||||
// body = (app read p0))
|
||||
let read_def = Def::Fn(FnDef {
|
||||
name: "read".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::Con { name: "List".into(), args: vec![] }],
|
||||
param_modes: vec![ParamMode::Borrow],
|
||||
ret: Box::new(Type::int()),
|
||||
ret_mode: ParamMode::Implicit,
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["xs".into()],
|
||||
body: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
doc: None,
|
||||
});
|
||||
let f_body = Term::App {
|
||||
callee: Box::new(Term::Var { name: "read".into() }),
|
||||
args: vec![Term::Var { name: "p0".into() }],
|
||||
tail: false,
|
||||
};
|
||||
let m = Module {
|
||||
schema: ailang_core::SCHEMA.into(),
|
||||
name: "t".into(),
|
||||
imports: vec![],
|
||||
defs: vec![read_def, fn_with_modes("f", vec![ParamMode::Own], f_body)],
|
||||
};
|
||||
let diags = check_module(&m);
|
||||
// Filter to over-strict-mode in case the helper triggers anything
|
||||
// (it shouldn't — `read` is `Borrow` and param is unused).
|
||||
let osm: Vec<_> = diags.iter().filter(|d| d.code == "over-strict-mode").collect();
|
||||
assert_eq!(osm.len(), 1, "expected one over-strict-mode, got {diags:?}");
|
||||
let d = osm[0];
|
||||
assert_eq!(d.severity, Severity::Warning);
|
||||
assert_eq!(d.def.as_deref(), Some("f"));
|
||||
assert_eq!(
|
||||
d.ctx,
|
||||
serde_json::json!({
|
||||
"binder": "p0",
|
||||
"current_mode": "own",
|
||||
"suggested_mode": "borrow",
|
||||
})
|
||||
);
|
||||
assert!(
|
||||
!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 ...)`.
|
||||
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}"
|
||||
);
|
||||
}
|
||||
|
||||
/// Iter 19a, negative: a fn with `(own T)` whose body consumes
|
||||
/// the param directly does not fire `over-strict-mode`.
|
||||
#[test]
|
||||
fn over_strict_mode_silent_when_body_consumes_param() {
|
||||
// Body: (seq p0 0) — `p0` is consumed in seq.lhs.
|
||||
let body = Term::Seq {
|
||||
lhs: Box::new(Term::Var { name: "p0".into() }),
|
||||
rhs: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
|
||||
};
|
||||
let m = Module {
|
||||
schema: ailang_core::SCHEMA.into(),
|
||||
name: "t".into(),
|
||||
imports: vec![],
|
||||
defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
|
||||
};
|
||||
let diags = check_module(&m);
|
||||
assert!(
|
||||
!diags.iter().any(|d| d.code == "over-strict-mode"),
|
||||
"no over-strict-mode expected; got {diags:?}"
|
||||
);
|
||||
}
|
||||
|
||||
/// Iter 19a, negative: a fn with `(borrow T)` and a borrowing
|
||||
/// body never fires `over-strict-mode` (the lint is gated on
|
||||
/// `Own`).
|
||||
#[test]
|
||||
fn over_strict_mode_silent_when_param_is_borrow() {
|
||||
// Body shape: literal — no use of the param at all.
|
||||
let m = Module {
|
||||
schema: ailang_core::SCHEMA.into(),
|
||||
name: "t".into(),
|
||||
imports: vec![],
|
||||
defs: vec![fn_with_modes(
|
||||
"f",
|
||||
vec![ParamMode::Borrow],
|
||||
Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
)],
|
||||
};
|
||||
let diags = check_module(&m);
|
||||
assert!(
|
||||
!diags.iter().any(|d| d.code == "over-strict-mode"),
|
||||
"no over-strict-mode expected for borrow-mode param; got {diags:?}"
|
||||
);
|
||||
}
|
||||
|
||||
/// 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.
|
||||
#[test]
|
||||
fn over_strict_mode_conservative_skips_match_on_param() {
|
||||
// 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.
|
||||
let body = Term::Match {
|
||||
scrutinee: Box::new(Term::Var { name: "p0".into() }),
|
||||
arms: vec![Arm {
|
||||
pat: Pattern::Wild,
|
||||
body: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
}],
|
||||
};
|
||||
let m = Module {
|
||||
schema: ailang_core::SCHEMA.into(),
|
||||
name: "t".into(),
|
||||
imports: vec![],
|
||||
defs: vec![fn_with_modes("f", vec![ParamMode::Own], 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:?}"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -36,4 +36,4 @@ pub mod parse;
|
||||
pub mod print;
|
||||
|
||||
pub use parse::{parse, parse_term, ParseError};
|
||||
pub use print::{print, term_to_form_a};
|
||||
pub use print::{print, term_to_form_a, type_to_form_a};
|
||||
|
||||
@@ -43,6 +43,16 @@ pub fn term_to_form_a(t: &Term) -> String {
|
||||
out
|
||||
}
|
||||
|
||||
/// Iter 19a: render a [`Type`] as form-A. Used by diagnostics that want
|
||||
/// to suggest a relaxed signature (e.g. `over-strict-mode` shows the
|
||||
/// `(fn-type ...)` with `(borrow T)` in place of `(own T)`). Output is
|
||||
/// the same shape that appears as the `type` slot of a `(fn ...)` def.
|
||||
pub fn type_to_form_a(t: &Type) -> String {
|
||||
let mut out = String::new();
|
||||
write_type(&mut out, t);
|
||||
out
|
||||
}
|
||||
|
||||
// ---- helpers --------------------------------------------------------------
|
||||
|
||||
fn indent(out: &mut String, level: usize) {
|
||||
|
||||
+150
@@ -8591,3 +8591,153 @@ implementation" — it is the literal RED-step that the discipline
|
||||
prescribes. The three fixtures shipped here are exactly that:
|
||||
each pins one of the three carve-out sites, observable via the
|
||||
RC stats line, kept as regression. JOURNAL queue: empty.
|
||||
|
||||
## 2026-05-08 — Design: explicit annotations stay mandatory; `over-strict-mode` diagnostic
|
||||
|
||||
User pushback on the queue-driven dispatch: the orchestrator
|
||||
floated "uniqueness inference replaces fn-signature mode
|
||||
annotations" as a candidate direction. Re-read of DESIGN.md
|
||||
§ "Decision 10" (lines 685–795) shows that pitch was a
|
||||
**Decision-10 reversal**, not an iter within it:
|
||||
|
||||
> *"AILang makes it mandatory because the LLM author can carry
|
||||
> the cognitive cost trivially, and the compiler gains a precise
|
||||
> contract at every call site instead of a probabilistic guess."*
|
||||
|
||||
Three reasons mandatory annotations are not redundancy in the
|
||||
harmful sense:
|
||||
|
||||
1. **Inference picks weakest-supporting; annotation states
|
||||
intent.** These often coincide today but are conceptually
|
||||
different. The annotation captures what the author committed
|
||||
to, not what the current body needs (e.g. `(own T)` reserved
|
||||
for a planned in-place mutation that hasn't landed).
|
||||
2. **Annotation is a drift-bremse.** Body change that flips
|
||||
the inferred mode → caller-side breakage at remote sites.
|
||||
Annotation enforces the local-conflict-error pattern instead.
|
||||
3. **Forcing function specific to LLM authoring.** Without
|
||||
mandatory annotation, an LLM never has to commit to ownership
|
||||
intent before writing the body — the contract becomes a
|
||||
by-product of local code choice. With it, the contract is a
|
||||
first-order variable the body must satisfy.
|
||||
|
||||
The "redundancy" between annotation and body is therefore the
|
||||
feature, not the bug — analogous to test code redundantly
|
||||
restating implementation behaviour, where the redundancy is what
|
||||
catches drift.
|
||||
|
||||
### What survives of the original pitch
|
||||
|
||||
One narrow but real observation: today, when the author writes
|
||||
`(own T)` and the body would compile under `(borrow T)`, the
|
||||
typechecker silently accepts. No warning, no diagnostic. The
|
||||
runtime cost is real (one inc/dec pair per call, plus potential
|
||||
rec-cascade at fn return), but invisible.
|
||||
|
||||
The Rust analogue is `clippy::needless_pass_by_value`: an
|
||||
informational lint with a suppression mechanism. AILang sharpens
|
||||
this to "suppression carries a mandatory reason" — consistent
|
||||
with the explicit-intent philosophy.
|
||||
|
||||
### Iter scope
|
||||
|
||||
Two iters, dispatched separately so 19a's diagnostic frequency
|
||||
on real code informs whether 19b's escape hatch is needed at all:
|
||||
|
||||
- **Iter 19a — `over-strict-mode` diagnostic.** Linearity pass
|
||||
detects: `param_modes[i] == Own` + `consume_count(p) == 0` +
|
||||
no consume of any sub-binder of p in the body. Emits
|
||||
`Severity::Warning` (the first warning-level diagnostic the
|
||||
typechecker has emitted; reserves no longer reserved). Carries
|
||||
a `suggested_rewrite` showing the relaxed `(borrow T)`
|
||||
signature. No schema change; pure detection.
|
||||
|
||||
- **Iter 19b — `mode-strict-because` suppression** (deferred
|
||||
pending 19a's signal). Optional schema field on fn defs:
|
||||
`suppress: [{code: String, because: String}]`. `because` is
|
||||
non-empty (schema-validation error otherwise). The suppress
|
||||
mechanism is generic across diagnostic codes but the only
|
||||
consumer initially is `over-strict-mode`.
|
||||
|
||||
### Why split
|
||||
|
||||
19a alone is shippable: users who see the warning either accept
|
||||
the rewrite or live with the noise on intentional-strict fns.
|
||||
19b is only worth building if real code surfaces enough
|
||||
intentional-strict cases to make the noise unbearable. This lets
|
||||
the data drive whether 19b ships at all.
|
||||
|
||||
### What this is NOT
|
||||
|
||||
Not a relaxation of Decision 10. Annotations stay mandatory.
|
||||
Authors cannot omit `param_modes` / `ret_mode`; the compiler
|
||||
will not infer them. The diagnostic is purely advisory: "you
|
||||
wrote this, here's a tighter alternative." If suppressed (19b),
|
||||
the annotation stays exactly as authored.
|
||||
|
||||
## 2026-05-08 — Iter 19a: `over-strict-mode` diagnostic shipped
|
||||
|
||||
The diagnostic-side of the design entry above. Linearity pass
|
||||
gained a post-walk loop over `Own`-annotated params; uniqueness
|
||||
side-table provides `consume_count`. When `consume_count == 0`
|
||||
*and* the body never destructures the param via match, the lint
|
||||
fires with a form-A-rendered fn-type rewrite as `suggested_rewrite`.
|
||||
|
||||
### Conservative cut
|
||||
|
||||
The precise rule is "no consume of any sub-binder of `p`". The
|
||||
shipped check approximates with "no `match` whose scrutinee is
|
||||
`pname`" — sound (never false-positive) but incomplete (misses
|
||||
match-on-p-without-sub-consume). Documented in `linearity.rs`'s
|
||||
module doc and pinned by the test
|
||||
`over_strict_mode_conservative_skips_match_on_param`. Acceptable
|
||||
because the lint is purely advisory: a missed warning costs
|
||||
nothing, a spurious warning would actively mislead. The precise
|
||||
variant is queued for a follow-up if real-corpus signal warrants.
|
||||
|
||||
### CLI side-effect
|
||||
|
||||
This is the first `Severity::Warning` diagnostic the typechecker
|
||||
emits. Three CLI exit paths (`Cmd::Check` non-JSON, `Cmd::EmitIr`,
|
||||
`build_to`) previously aborted on any non-empty diagnostic list;
|
||||
now they only abort when at least one diagnostic is `Severity::Error`.
|
||||
The `--json` path was already correct (returns the list, doesn't
|
||||
exit). No observable behaviour change for any pre-19a input —
|
||||
nothing emitted Warning before this iter — but the gate is now
|
||||
in place for future warning-level lints.
|
||||
|
||||
### Tests
|
||||
|
||||
Four new tests in `linearity.rs::tests`:
|
||||
|
||||
- `over_strict_mode_fires_when_param_only_borrowed` — positive.
|
||||
- `over_strict_mode_silent_when_body_consumes_param` — negative.
|
||||
- `over_strict_mode_silent_when_param_is_borrow` — negative.
|
||||
- `over_strict_mode_conservative_skips_match_on_param` — pins the
|
||||
conservatism; flips to a positive assertion when the precise
|
||||
variant lands.
|
||||
|
||||
`ailang-check` test count: 49 → 53. e2e unchanged at 69. Workspace
|
||||
build + test green.
|
||||
|
||||
### Files touched
|
||||
|
||||
- `crates/ailang-check/src/diagnostic.rs` — registered
|
||||
`over-strict-mode` code, refreshed `Severity::Warning` doc,
|
||||
added `Diagnostic::warning` ctor.
|
||||
- `crates/ailang-check/src/linearity.rs` — module-doc § 19a, the
|
||||
post-walk loop, helpers (`body_matches_on`,
|
||||
`scrutinee_matches_param`, `make_over_strict_mode`,
|
||||
`relax_param_to_borrow`), `check_fn` signature gained a
|
||||
`&UniquenessTable` arg.
|
||||
- `crates/ailang-surface/src/print.rs` — new
|
||||
`pub fn type_to_form_a(&Type) -> String` (re-exported from `lib.rs`).
|
||||
- `crates/ail/src/main.rs` — three exit-on-Error gates.
|
||||
|
||||
### What stays queued
|
||||
|
||||
- Iter 19b (`mode-strict-because` suppression): waits for
|
||||
real-corpus signal on whether intentional-strict fns are
|
||||
common enough to warrant the schema field.
|
||||
- Precise sub-binder analysis for the lint: waits for evidence
|
||||
that the conservative cut misses real cases.
|
||||
|
||||
Reference in New Issue
Block a user