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

feat(check): tee let-binder types, exempt value-typed let-binders (#57, 0064 iter 1)

Browse Source 
First iteration of spec 0064 (the #55-cutover hardening, #57). Closes
false-positive class 3: a value-typed `let`-binder (e.g. a `Float`
result bound and read more than once) tripped `use-after-consume`
because the linearity walk installed every `let`-binder as a default
heap-tracked BinderState. Spec 0063 deferred exactly this class
("value-typed let-binders ... deferred until a corpus shape demands
it"); eqord_3_newton_sqrt.iterate's `(let xnew (app / …) …)` is that
shape.

Mechanism (the design call, user-delegated): the let-binder's type is
ALREADY computed at synth's Let arm and discarded. Stop discarding it.
synth gains a (def,binder)->Type out-param (LetBinderTypes, defined in
linearity.rs); the Let arm records `subst.apply(&v)`. The table is
allocated per-module in check_workspace, threaded through
check_in_workspace -> check_def -> check_fn/check_const/check_instance
-> synth, and passed (immutable) into check_module_with_visible ->
Checker. linearity's Term::Let seeds BinderState.is_value from the
table via the existing type_is_value predicate -- the same per-binder
flag #56 seeds at param/pattern/lam sites, now extended to the let
site. No schema change, no hash shift, no codegen change; the check
stays diagnostic-only.

Not a re-run of inference in the walk (ruled out by aaa70d4 / 0063):
the type is teed from the one pass that already knows it.

RED-first: examples/c3_value_let.ail added to
harden_ownership_false_positives_are_clean (RED: use-after-consume on
xnew) before the fix; GREEN after. Two in-source unit tests pin the
seeding (value-typed let clean via a hand-built Float table) and its
type-gating (heap-typed let still errors). Full ailang-check suite
green (117 linearity + 14 workspace); cargo test --workspace green;
the heap-double-consume must-stay-RED guard still fires.

Implementation notes (verified against the diff):
- The live call graph routes check_in_workspace through check_def, not
  directly to check_fn (the plan's fixed line numbers predated that);
  the table is threaded through check_def's three arms. Required to
  reach every synth, not an extra.
- Step-10 compiler enumeration surfaced 26 synth call sites: 22
  recursive (the plan's "~22") plus 4 post-typecheck re-synth
  re-entries (lift.rs, lower_to_mir.rs, mono.rs x2). The four are
  write-only re-synth callers that discard their side-channels and
  never query the table, so each got a throwaway table -- the typed-MIR
  re-synth path (it re-enters canonical synth), consistent with the
  plan's const-def/test-caller pattern.

Fixes 1 (local fn-param modes), 2 (let-alias redirect), 4
(partition_eithers rewrite) are later iterations of spec 0064.

refs #57
This commit is contained in:
Brummel
2026-06-01 17:44:40 +02:00
parent ba981689fc
commit 47964abf7c
8 changed files with 168 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/builtins.rs
+2
View File
@@ -325,6 +325,7 @@ mod tests {
&mut residuals, &mut residuals,
&mut free_fn_calls, &mut free_fn_calls,
&mut warnings, &mut warnings,
&mut crate::linearity::LetBinderTypes::new(),
) )
.expect("synth"); .expect("synth");
subst.apply(&ty) subst.apply(&ty)
@@ -559,6 +560,7 @@ mod tests {
&mut residuals, &mut residuals,
&mut free_fn_calls, &mut free_fn_calls,
&mut warnings, &mut warnings,
&mut crate::linearity::LetBinderTypes::new(),
) )
.expect_err("must reject"); .expect_err("must reject");
assert!( assert!(
crates/ailang-check/src/lib.rs
+60 -35
View File
@@ -1233,7 +1233,9 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
// shadowed-class-method warning is visible even when the // shadowed-class-method warning is visible even when the
// module also has unrelated errors. // module also has unrelated errors.
let mut synth_warnings: Vec<Diagnostic> = Vec::new(); let mut synth_warnings: Vec<Diagnostic> = Vec::new();
let typecheck_errors = check_in_workspace(m, ws, &module_globals, &mut synth_warnings); let mut let_binder_types = crate::linearity::LetBinderTypes::new();
let typecheck_errors =
check_in_workspace(m, ws, &module_globals, &mut synth_warnings, &mut let_binder_types);
let had_typecheck_errors = !typecheck_errors.is_empty(); let had_typecheck_errors = !typecheck_errors.is_empty();
// Per-module diagnostic accumulator. The suppress filter // Per-module diagnostic accumulator. The suppress filter
// (Iter 19b) runs at the end of the per-module block, so // (Iter 19b) runs at the end of the per-module block, so
@@ -1273,7 +1275,7 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
} }
}) })
.collect(); .collect();
module_diags.extend(linearity::check_module_with_visible(m, &visible_extra)); module_diags.extend(linearity::check_module_with_visible(m, &visible_extra, &let_binder_types));
// reuse-as shape compatibility check. Runs on // reuse-as shape compatibility check. Runs on
// the same activation gate as linearity (all-explicit-mode // the same activation gate as linearity (all-explicit-mode
// fns only). The check resolves each `(reuse-as <var> // fns only). The check resolves each `(reuse-as <var>
@@ -1422,7 +1424,12 @@ pub fn check(m: &Module) -> Result<CheckedModule> {
// discarded — `check`'s legacy contract returns only the first // discarded — `check`'s legacy contract returns only the first
// error, and warnings on this path have no surface to flow to. // error, and warnings on this path have no surface to flow to.
let mut synth_warnings: Vec<Diagnostic> = Vec::new(); let mut synth_warnings: Vec<Diagnostic> = Vec::new();
if let Some(first) = check_in_workspace(m, &ws, &module_globals, &mut synth_warnings).into_iter().next() { let mut let_binder_types = crate::linearity::LetBinderTypes::new();
if let Some(first) =
check_in_workspace(m, &ws, &module_globals, &mut synth_warnings, &mut let_binder_types)
.into_iter()
.next()
{
return Err(first); return Err(first);
} }
// Collect symbols for the return value (existing semantics). // Collect symbols for the return value (existing semantics).
@@ -1883,6 +1890,7 @@ fn check_in_workspace(
// only `class-method-shadowed-by-fn` flows through this channel // only `class-method-shadowed-by-fn` flows through this channel
// (emitted from `synth` via `check_fn`'s warnings accumulator). // (emitted from `synth` via `check_fn`'s warnings accumulator).
out_warnings: &mut Vec<Diagnostic>, out_warnings: &mut Vec<Diagnostic>,
let_binder_types: &mut crate::linearity::LetBinderTypes,
) -> Vec<CheckError> { ) -> Vec<CheckError> {
let mut env = build_check_env(ws); let mut env = build_check_env(ws);
let mut errors: Vec<CheckError> = Vec::new(); let mut errors: Vec<CheckError> = Vec::new();
@@ -1975,7 +1983,7 @@ fn check_in_workspace(
env.current_module_kernel_tier = m.kernel || m.name == "prelude"; env.current_module_kernel_tier = m.kernel || m.name == "prelude";
for def in &m.defs { for def in &m.defs {
match check_def(def, &env, out_warnings) { match check_def(def, &env, out_warnings, let_binder_types) {
Ok(()) => {} Ok(()) => {}
Err(e) => { Err(e) => {
errors.push(CheckError::Def(def.name().to_string(), Box::new(e))); errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
@@ -1994,10 +2002,11 @@ fn check_def(
def: &Def, def: &Def,
env: &Env, env: &Env,
out_warnings: &mut Vec<Diagnostic>, out_warnings: &mut Vec<Diagnostic>,
let_binder_types: &mut crate::linearity::LetBinderTypes,
) -> Result<()> { ) -> Result<()> {
match def { match def {
Def::Fn(f) => check_fn(f, env, out_warnings), Def::Fn(f) => check_fn(f, env, out_warnings, let_binder_types),
Def::Const(c) => check_const(c, env, out_warnings), Def::Const(c) => check_const(c, env, out_warnings, let_binder_types),
Def::Type(td) => check_type_def(td, env), Def::Type(td) => check_type_def(td, env),
// bugfix-instance-body-unbound-var (2026-05-13): each instance // bugfix-instance-body-unbound-var (2026-05-13): each instance
// method body is walked through `check_fn` via a synthetic // method body is walked through `check_fn` via a synthetic
@@ -2016,7 +2025,7 @@ fn check_def(
// malformed instance never reaches this body-walk. `Def::Class` // malformed instance never reaches this body-walk. `Def::Class`
// remains schema-only at this layer. // remains schema-only at this layer.
Def::Class(_) => Ok(()), Def::Class(_) => Ok(()),
Def::Instance(inst) => check_instance(inst, env, out_warnings), Def::Instance(inst) => check_instance(inst, env, out_warnings, let_binder_types),
} }
} }
@@ -2052,6 +2061,7 @@ fn check_instance(
inst: &InstanceDef, inst: &InstanceDef,
env: &Env, env: &Env,
out_warnings: &mut Vec<Diagnostic>, out_warnings: &mut Vec<Diagnostic>,
let_binder_types: &mut crate::linearity::LetBinderTypes,
) -> Result<()> { ) -> Result<()> {
let qualified_class = qualify_class_ref_in_check(&inst.class, &env.current_module); let qualified_class = qualify_class_ref_in_check(&inst.class, &env.current_module);
for im in &inst.methods { for im in &inst.methods {
@@ -2094,7 +2104,7 @@ fn check_instance(
suppress: Vec::new(), suppress: Vec::new(),
export: None, export: None,
}; };
check_fn(&synthetic, env, out_warnings)?; check_fn(&synthetic, env, out_warnings, let_binder_types)?;
} }
Ok(()) Ok(())
} }
@@ -2235,7 +2245,12 @@ pub(crate) fn is_intrinsic_body(f: &FnDef) -> bool {
|| matches!(&f.body, Term::Lam { body, .. } if matches!(**body, Term::Intrinsic)) || matches!(&f.body, Term::Lam { body, .. } if matches!(**body, Term::Intrinsic))
} }
fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> { fn check_fn(
f: &FnDef,
env: &Env,
out_warnings: &mut Vec<Diagnostic>,
let_binder_types: &mut crate::linearity::LetBinderTypes,
) -> Result<()> {
// Peel an outer Forall (Iter 12a). The vars become rigid in the // Peel an outer Forall (Iter 12a). The vars become rigid in the
// inner env so they pass `check_type_well_formed` and unify only // inner env so they pass `check_type_well_formed` and unify only
// with themselves. An empty `vars` list (vacuously polymorphic) // with themselves. An empty `vars` list (vacuously polymorphic)
@@ -2407,7 +2422,7 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
// Empty at fn entry; pushed/popped by `Term::Loop` arms during // Empty at fn entry; pushed/popped by `Term::Loop` arms during
// the synth walk; discarded after the body type-checks. // the synth walk; discarded after the body type-checks.
let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new(); let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
let body_ty = synth(&f.body, &env, &mut locals, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?; let body_ty = synth(&f.body, &env, &mut locals, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings, let_binder_types)?;
unify(&ret_ty, &body_ty, &mut subst)?; unify(&ret_ty, &body_ty, &mut subst)?;
// surface synth-time warnings into the caller-supplied // surface synth-time warnings into the caller-supplied
// accumulator. The warnings already carry `def: Some(f.name)` // accumulator. The warnings already carry `def: Some(f.name)`
@@ -3283,7 +3298,12 @@ fn verify_loop_body(t: &Term, in_loop_tail: bool) -> Result<()> {
} }
} }
fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> { fn check_const(
c: &ConstDef,
env: &Env,
out_warnings: &mut Vec<Diagnostic>,
let_binder_types: &mut crate::linearity::LetBinderTypes,
) -> Result<()> {
// Const types are never polymorphic — a Forall here is rejected // Const types are never polymorphic — a Forall here is rejected
// outright. Any other type passes through to `synth` as before. // outright. Any other type passes through to `synth` as before.
if matches!(&c.ty, Type::Forall { .. }) { if matches!(&c.ty, Type::Forall { .. }) {
@@ -3303,7 +3323,7 @@ fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> R
// loop-recur iter 2: a const value has no enclosing loop; any // loop-recur iter 2: a const value has no enclosing loop; any
// `recur` in a const body correctly fires `RecurOutsideLoop`. // `recur` in a const body correctly fires `RecurOutsideLoop`.
let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new(); let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
let v = synth(&c.value, env, &mut locals, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?; let v = synth(&c.value, env, &mut locals, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings, let_binder_types)?;
out_warnings.extend(warnings); out_warnings.extend(warnings);
unify(&c.ty, &v, &mut subst)?; unify(&c.ty, &v, &mut subst)?;
if !effects.is_empty() { if !effects.is_empty() {
@@ -3342,6 +3362,7 @@ pub(crate) fn synth(
// `class-method-shadowed-by-fn` warning is emitted here; future // `class-method-shadowed-by-fn` warning is emitted here; future
// synth-time warnings (if any) would flow through the same channel. // synth-time warnings (if any) would flow through the same channel.
warnings: &mut Vec<crate::diagnostic::Diagnostic>, warnings: &mut Vec<crate::diagnostic::Diagnostic>,
let_binder_types: &mut crate::linearity::LetBinderTypes,
) -> Result<Type> { ) -> Result<Type> {
match t { match t {
Term::Lit { lit } => Ok(match lit { Term::Lit { lit } => Ok(match lit {
@@ -3752,7 +3773,7 @@ pub(crate) fn synth(
Ok(maybe_instantiate(raw, counter)) Ok(maybe_instantiate(raw, counter))
} }
Term::App { callee, args, .. } => { Term::App { callee, args, .. } => {
let cty = synth(callee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let cty = synth(callee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
let cty = subst.apply(&cty); let cty = subst.apply(&cty);
let (params, ret, fx) = match &cty { let (params, ret, fx) = match &cty {
Type::Fn { params, ret, effects: fx, .. } => { Type::Fn { params, ret, effects: fx, .. } => {
@@ -3788,7 +3809,7 @@ pub(crate) fn synth(
}); });
} }
for (a, exp) in args.iter().zip(params.iter()) { for (a, exp) in args.iter().zip(params.iter()) {
let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
// Reconcile the post-mono own-module spelling split: a // Reconcile the post-mono own-module spelling split: a
// cross-module callee may name the consumer's own ADT // cross-module callee may name the consumer's own ADT
// qualified (`<current_module>.T`) where the consumer // qualified (`<current_module>.T`) where the consumer
@@ -3805,9 +3826,10 @@ pub(crate) fn synth(
Ok(subst.apply(&ret)) Ok(subst.apply(&ret))
} }
Term::Let { name, value, body } => { Term::Let { name, value, body } => {
let v = synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let v = synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
let_binder_types.insert((in_def.to_string(), name.clone()), subst.apply(&v));
let prev = locals.insert(name.clone(), v); let prev = locals.insert(name.clone(), v);
let r = synth(body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let r = synth(body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
match prev { match prev {
Some(p) => { Some(p) => {
locals.insert(name.clone(), p); locals.insert(name.clone(), p);
@@ -3819,10 +3841,10 @@ pub(crate) fn synth(
Ok(r) Ok(r)
} }
Term::If { cond, then, else_ } => { Term::If { cond, then, else_ } => {
let c = synth(cond, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let c = synth(cond, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
unify(&Type::bool_(), &c, subst)?; unify(&Type::bool_(), &c, subst)?;
let t1 = synth(then, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let t1 = synth(then, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
let t2 = synth(else_, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let t2 = synth(else_, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
unify(&t1, &t2, subst)?; unify(&t1, &t2, subst)?;
Ok(subst.apply(&t1)) Ok(subst.apply(&t1))
} }
@@ -3840,7 +3862,7 @@ pub(crate) fn synth(
}); });
} }
for (a, exp) in args.iter().zip(sig.params.iter()) { for (a, exp) in args.iter().zip(sig.params.iter()) {
let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
unify(exp, &actual, subst)?; unify(exp, &actual, subst)?;
} }
effects.insert(sig.effect.clone()); effects.insert(sig.effect.clone());
@@ -3960,7 +3982,7 @@ pub(crate) fn synth(
} }
for (a, exp) in args.iter().zip(qualified_fields.iter()) { for (a, exp) in args.iter().zip(qualified_fields.iter()) {
let exp_inst = substitute_rigids(exp, &mapping); let exp_inst = substitute_rigids(exp, &mapping);
let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
unify(&exp_inst, &actual, subst)?; unify(&exp_inst, &actual, subst)?;
} }
Ok(Type::Con { Ok(Type::Con {
@@ -3969,7 +3991,7 @@ pub(crate) fn synth(
}) })
} }
Term::Match { scrutinee, arms } => { Term::Match { scrutinee, arms } => {
let s_ty = synth(scrutinee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let s_ty = synth(scrutinee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
if arms.is_empty() { if arms.is_empty() {
return Err(CheckError::NonExhaustive { return Err(CheckError::NonExhaustive {
ty: ailang_core::pretty::type_to_string(&s_ty), ty: ailang_core::pretty::type_to_string(&s_ty),
@@ -3987,7 +4009,7 @@ pub(crate) fn synth(
let prev = locals.insert(n.clone(), t.clone()); let prev = locals.insert(n.clone(), t.clone());
pushed.push((n.clone(), prev)); pushed.push((n.clone(), prev));
} }
let body_ty = synth(&arm.body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let body_ty = synth(&arm.body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
for (n, prev) in pushed.into_iter().rev() { for (n, prev) in pushed.into_iter().rev() {
match prev { match prev {
Some(p) => { Some(p) => {
@@ -4062,9 +4084,9 @@ pub(crate) fn synth(
Ok(subst.apply(&result_ty.expect("checked arms is non-empty"))) Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
} }
Term::Seq { lhs, rhs } => { Term::Seq { lhs, rhs } => {
let lty = synth(lhs, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let lty = synth(lhs, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
unify(&Type::unit(), &lty, subst)?; unify(&Type::unit(), &lty, subst)?;
synth(rhs, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) synth(rhs, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)
} }
Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => { Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
// reject lambda-captures-of-loop-binder. // reject lambda-captures-of-loop-binder.
@@ -4103,7 +4125,7 @@ pub(crate) fn synth(
pushed.push((n.clone(), prev)); pushed.push((n.clone(), prev));
} }
let mut body_effects: BTreeSet<String> = BTreeSet::new(); let mut body_effects: BTreeSet<String> = BTreeSet::new();
let body_ty = synth(body, env, locals, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings); let body_ty = synth(body, env, locals, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types);
for (n, prev) in pushed.into_iter().rev() { for (n, prev) in pushed.into_iter().rev() {
match prev { match prev {
Some(p) => { Some(p) => {
@@ -4191,7 +4213,7 @@ pub(crate) fn synth(
// subset rule against `declared_effs` — exactly like // subset rule against `declared_effs` — exactly like
// `Term::Lam`. // `Term::Lam`.
let mut body_effects: BTreeSet<String> = BTreeSet::new(); let mut body_effects: BTreeSet<String> = BTreeSet::new();
let body_ty = synth(body, env, locals, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings); let body_ty = synth(body, env, locals, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types);
// Restore body-scope locals (params + name). // Restore body-scope locals (params + name).
for (n, prev) in pushed.into_iter().rev() { for (n, prev) in pushed.into_iter().rev() {
@@ -4218,7 +4240,7 @@ pub(crate) fn synth(
// scope (params are not visible here; only the recursive // scope (params are not visible here; only the recursive
// binding is). // binding is).
let prev_in = locals.insert(name.clone(), ty.clone()); let prev_in = locals.insert(name.clone(), ty.clone());
let in_ty = synth(in_term, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings); let in_ty = synth(in_term, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types);
match prev_in { match prev_in {
Some(p) => { Some(p) => {
locals.insert(name.clone(), p); locals.insert(name.clone(), p);
@@ -4234,7 +4256,7 @@ pub(crate) fn synth(
// No constraint generated, no environment change. The // No constraint generated, no environment change. The
// wrapper records author intent for the future RC inc/dec // wrapper records author intent for the future RC inc/dec
// emission pass (18c.3); typing is pure passthrough. // emission pass (18c.3); typing is pure passthrough.
synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)
} }
Term::ReuseAs { source, body } => { Term::ReuseAs { source, body } => {
// `(reuse-as SRC NEW-CTOR)` requires `body` to // `(reuse-as SRC NEW-CTOR)` requires `body` to
@@ -4248,7 +4270,7 @@ pub(crate) fn synth(
// shape-compatibility check (18d.2 will add a // shape-compatibility check (18d.2 will add a
// `reuse-as-shape-mismatch` diagnostic when codegen has // `reuse-as-shape-mismatch` diagnostic when codegen has
// the actual size info). // the actual size info).
let _ = synth(source, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let _ = synth(source, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)?;
match body.as_ref() { match body.as_ref() {
Term::Ctor { .. } | Term::Lam { .. } => {} Term::Ctor { .. } | Term::Lam { .. } => {}
other => { other => {
@@ -4278,7 +4300,7 @@ pub(crate) fn synth(
} }
// Body's type is the result type of the whole reuse-as // Body's type is the result type of the whole reuse-as
// expression. // expression.
synth(body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) synth(body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types)
} }
// loop-recur iter 2: each binder init is synthed in the // loop-recur iter 2: each binder init is synthed in the
// outer scope plus already-declared binder names of THIS // outer scope plus already-declared binder names of THIS
@@ -4296,7 +4318,7 @@ pub(crate) fn synth(
for b in binders { for b in binders {
let init_ty = synth( let init_ty = synth(
&b.init, env, locals, loop_stack, effects, &b.init, env, locals, loop_stack, effects,
in_def, subst, counter, residuals, free_fn_calls, warnings, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types,
)?; )?;
unify(&b.ty, &init_ty, subst)?; unify(&b.ty, &init_ty, subst)?;
binder_frame.push((b.name.clone(), b.ty.clone())); binder_frame.push((b.name.clone(), b.ty.clone()));
@@ -4306,7 +4328,7 @@ pub(crate) fn synth(
loop_stack.push(binder_frame); loop_stack.push(binder_frame);
let body_result = synth( let body_result = synth(
body, env, locals, loop_stack, effects, body, env, locals, loop_stack, effects,
in_def, subst, counter, residuals, free_fn_calls, warnings, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types,
); );
loop_stack.pop(); loop_stack.pop();
for (name, prev) in restore.into_iter().rev() { for (name, prev) in restore.into_iter().rev() {
@@ -4344,7 +4366,7 @@ pub(crate) fn synth(
for (i, a) in args.iter().enumerate() { for (i, a) in args.iter().enumerate() {
let arg_ty = synth( let arg_ty = synth(
a, env, locals, loop_stack, effects, a, env, locals, loop_stack, effects,
in_def, subst, counter, residuals, free_fn_calls, warnings, in_def, subst, counter, residuals, free_fn_calls, warnings, let_binder_types,
)?; )?;
let applied_binder = subst.apply(&binder_frame[i].1); let applied_binder = subst.apply(&binder_frame[i].1);
let applied_arg = subst.apply(&arg_ty); let applied_arg = subst.apply(&arg_ty);
@@ -4559,7 +4581,7 @@ pub(crate) fn synth(
let expected_inst = substitute_rigids(expected_param, &mapping); let expected_inst = substitute_rigids(expected_param, &mapping);
let actual = synth( let actual = synth(
v, env, locals, loop_stack, effects, in_def, subst, counter, v, env, locals, loop_stack, effects, in_def, subst, counter,
residuals, free_fn_calls, warnings, residuals, free_fn_calls, warnings, let_binder_types,
)?; )?;
unify(&expected_inst, &actual, subst)?; unify(&expected_inst, &actual, subst)?;
} }
@@ -5309,6 +5331,7 @@ mod tests {
&mut residuals, &mut residuals,
&mut free_fn_calls, &mut free_fn_calls,
&mut warnings, &mut warnings,
&mut crate::linearity::LetBinderTypes::new(),
) )
.expect("synth must succeed"); .expect("synth must succeed");
subst.apply(&ty) subst.apply(&ty)
@@ -5408,6 +5431,7 @@ mod tests {
&term, &env, &mut locals, &mut loop_stack, &mut effects, &term, &env, &mut locals, &mut loop_stack, &mut effects,
"<test>", &mut subst, &mut counter, &mut residuals, "<test>", &mut subst, &mut counter, &mut residuals,
&mut free_fn_calls, &mut warnings, &mut free_fn_calls, &mut warnings,
&mut crate::linearity::LetBinderTypes::new(),
) )
.expect_err("lambda capturing loop binder must be rejected"); .expect_err("lambda capturing loop binder must be rejected");
match err { match err {
@@ -7957,6 +7981,7 @@ mod tests {
&mut residuals, &mut residuals,
&mut free_fn_calls, &mut free_fn_calls,
&mut warnings, &mut warnings,
&mut crate::linearity::LetBinderTypes::new(),
) )
.expect("synth must succeed (fn wins precedence)"); .expect("synth must succeed (fn wins precedence)");
assert!( assert!(
crates/ailang-check/src/lift.rs
+1 -1
View File
@@ -742,7 +742,7 @@ impl<'a> Lifter<'a> {
// one term at a time from a top-of-body position; fresh empty // one term at a time from a top-of-body position; fresh empty
// loop-stack is correct (any `Term::Loop` pushes its own frame). // loop-stack is correct (any `Term::Loop` pushes its own frame).
let mut loop_stack: Vec<Vec<(String, crate::Type)>> = Vec::new(); let mut loop_stack: Vec<Vec<(String, crate::Type)>> = Vec::new();
let ty = synth(t, &self.env, locals, &mut loop_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?; let ty = synth(t, &self.env, locals, &mut loop_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded, &mut crate::linearity::LetBinderTypes::new())?;
Ok(subst.apply(&ty)) Ok(subst.apply(&ty))
} }
} }
crates/ailang-check/src/linearity.rs
+90 -5
View File
@@ -149,6 +149,13 @@ use ailang_core::ast::{Arm, Ctor, Def, FnDef, Module, NewArg, ParamMode, Pattern
use ailang_surface::{term_to_form_a, type_to_form_a}; use ailang_surface::{term_to_form_a, type_to_form_a};
use std::collections::HashMap; use std::collections::HashMap;
/// Per-fn inferred type of each `Term::Let` binder, teed out of the
/// typecheck pass (`synth`'s `Let` arm) so the linearity walk — which
/// runs after typechecking and does not re-infer — can read a
/// `let`-binder's type where the source pins no annotation. Keyed
/// `(def_name, binder_name)`.
pub(crate) type LetBinderTypes = HashMap<(String, String), Type>;
/// a `Type::Con` whose name is `Int`/`Bool`/`Str`/`Unit` /// a `Type::Con` whose name is `Int`/`Bool`/`Str`/`Unit`
/// is a primitive value type — no RC, no heap. Reading a primitive /// is a primitive value type — no RC, no heap. Reading a primitive
/// pattern-binder bumps `consume_count` in the uniqueness table but /// pattern-binder bumps `consume_count` in the uniqueness table but
@@ -221,7 +228,7 @@ struct BinderState {
/// auto-injected prelude's polymorphic free fns and class methods. /// auto-injected prelude's polymorphic free fns and class methods.
#[cfg(test)] #[cfg(test)]
pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> { pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
check_module_with_visible(m, &[]) check_module_with_visible(m, &[], &LetBinderTypes::new())
} }
/// workspace-aware entry. `visible_extra` is a slice of /// workspace-aware entry. `visible_extra` is a slice of
@@ -234,7 +241,11 @@ pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
/// Symmetric to the iter 23.4-prep extension that made class methods /// Symmetric to the iter 23.4-prep extension that made class methods
/// visible. Bodies of the visible-extra modules are NOT walked here /// visible. Bodies of the visible-extra modules are NOT walked here
/// — they are checked when their own module is processed. /// — they are checked when their own module is processed.
pub(crate) fn check_module_with_visible(m: &Module, visible_extra: &[&Module]) -> Vec<Diagnostic> { pub(crate) fn check_module_with_visible(
m: &Module,
visible_extra: &[&Module],
let_binder_types: &LetBinderTypes,
) -> Vec<Diagnostic> {
let mut globals: HashMap<String, Type> = HashMap::new(); let mut globals: HashMap<String, Type> = HashMap::new();
// ctor name → field types, used by the // ctor name → field types, used by the
// `over-strict-mode` lint to filter out primitive-typed // `over-strict-mode` lint to filter out primitive-typed
@@ -319,7 +330,7 @@ pub(crate) fn check_module_with_visible(m: &Module, visible_extra: &[&Module]) -
let mut diags = Vec::new(); let mut diags = Vec::new();
for def in &m.defs { for def in &m.defs {
if let Def::Fn(f) = def { if let Def::Fn(f) = def {
check_fn(f, &globals, &ctors, &uniq, &mut diags); check_fn(f, &globals, &ctors, &uniq, let_binder_types, &mut diags);
} }
} }
diags diags
@@ -342,6 +353,7 @@ fn check_fn(
globals: &HashMap<String, Type>, globals: &HashMap<String, Type>,
ctors: &HashMap<String, Vec<Type>>, ctors: &HashMap<String, Vec<Type>>,
uniq: &UniquenessTable, uniq: &UniquenessTable,
let_binder_types: &LetBinderTypes,
diags: &mut Vec<Diagnostic>, diags: &mut Vec<Diagnostic>,
) { ) {
let inner = strip_forall(&f.ty); let inner = strip_forall(&f.ty);
@@ -370,6 +382,7 @@ fn check_fn(
diags, diags,
def_name: &f.name, def_name: &f.name,
ctors, ctors,
let_binder_types,
binders: HashMap::new(), binders: HashMap::new(),
}; };
@@ -439,6 +452,10 @@ struct Checker<'a> {
/// from consume-tracking. Mirrors the `ctors` map built in /// from consume-tracking. Mirrors the `ctors` map built in
/// `check_module_with_visible`. /// `check_module_with_visible`.
ctors: &'a HashMap<String, Vec<Type>>, ctors: &'a HashMap<String, Vec<Type>>,
/// `(def, let-binder) → inferred type`, teed from the typecheck
/// pass. Read at the `Term::Let` arm to seed `is_value` for a
/// value-typed `let`-binder (the source pins no annotation there).
let_binder_types: &'a LetBinderTypes,
/// Live binder state, keyed by name. Modified in place; lexical /// Live binder state, keyed by name. Modified in place; lexical
/// scoping is restored by [`Checker::with_binder`]. /// scoping is restored by [`Checker::with_binder`].
binders: HashMap<String, BinderState>, binders: HashMap<String, BinderState>,
@@ -504,9 +521,18 @@ impl<'a> Checker<'a> {
} }
Term::Let { name, value, body } => { Term::Let { name, value, body } => {
self.walk(value, Position::Consume); self.walk(value, Position::Consume);
self.with_binder(name, BinderState::default(), |this| { let is_value = self
.let_binder_types
.get(&(self.def_name.to_string(), name.clone()))
.map(type_is_value)
.unwrap_or(false);
self.with_binder(
name,
BinderState { is_value, ..BinderState::default() },
|this| {
this.walk(body, pos); this.walk(body, pos);
}); },
);
} }
Term::LetRec { name, body, in_term, .. } => { Term::LetRec { name, body, in_term, .. } => {
// The body is the recursive fn's own body; treating it as // The body is the recursive fn's own body; treating it as
@@ -1494,6 +1520,65 @@ mod tests {
); );
} }
/// A value-typed `let`-binder (type teed as `Float`) read twice
/// (`(let x 0 (seq x x))`) must NOT fire use-after-consume — the
/// `is_value` flag is seeded from the let-binder type table. RED
/// until the class-3 fix.
#[test]
fn value_let_binder_multi_read_is_clean() {
let body = Term::Let {
name: "x".into(),
value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
body: Box::new(Term::Seq {
lhs: Box::new(Term::Var { name: "x".into() }),
rhs: Box::new(Term::Var { name: "x".into() }),
}),
};
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_int_own("f", body)],
};
let mut lbt = LetBinderTypes::new();
lbt.insert(("f".into(), "x".into()), Type::Con { name: "Float".into(), args: vec![] });
let diags = check_module_with_visible(&m, &[], &lbt);
assert!(
!diags.iter().any(|d| d.code == "use-after-consume"),
"a value-typed let-binder is never consumed; multi-read is legal; got {diags:?}"
);
}
/// Type-gating guard: a HEAP-typed `let`-binder (teed as `List`)
/// read twice MUST still fire use-after-consume — the exemption is
/// value-type-only, not blanket. (Regression guard, green after fix.)
#[test]
fn heap_let_binder_multi_read_still_errors() {
let body = Term::Let {
name: "x".into(),
value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
body: Box::new(Term::Seq {
lhs: Box::new(Term::Var { name: "x".into() }),
rhs: Box::new(Term::Var { name: "x".into() }),
}),
};
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_int_own("f", body)],
};
let mut lbt = LetBinderTypes::new();
lbt.insert(("f".into(), "x".into()), Type::Con { name: "List".into(), args: vec![] });
let diags = check_module_with_visible(&m, &[], &lbt);
assert!(
diags.iter().any(|d| d.code == "use-after-consume"),
"a heap-typed let-binder consumed twice must still fire; got {diags:?}"
);
}
/// Type-gating guard: a HEAP param (`List`) consumed twice in a ctor /// Type-gating guard: a HEAP param (`List`) consumed twice in a ctor
/// (`(term-ctor Pair Pair p0 p0)`) MUST still fire use-after-consume /// (`(term-ctor Pair Pair p0 p0)`) MUST still fire use-after-consume
/// after the fix — the exemption is value-type-only, not blanket. /// after the fix — the exemption is value-type-only, not blanket.
crates/ailang-check/src/lower_to_mir.rs
+1
View File
@@ -49,6 +49,7 @@ impl<'a> Ctx<'a> {
&mut residuals, &mut residuals,
&mut free_fn_calls, &mut free_fn_calls,
&mut warnings, &mut warnings,
&mut crate::linearity::LetBinderTypes::new(),
)?; )?;
Ok(wildcard_residual_metavars(&subst.apply(&ty))) Ok(wildcard_residual_metavars(&subst.apply(&ty)))
} }
crates/ailang-check/src/mono.rs
+2
View File
@@ -836,6 +836,7 @@ pub fn collect_mono_targets(
&mut residuals, &mut residuals,
&mut free_fn_calls, &mut free_fn_calls,
&mut warnings_discarded, &mut warnings_discarded,
&mut crate::linearity::LetBinderTypes::new(),
)?; )?;
// Filter residuals to fully-concrete ones; look up // Filter residuals to fully-concrete ones; look up
@@ -1641,6 +1642,7 @@ pub(crate) fn collect_residuals_ordered(
&mut residuals, &mut residuals,
&mut free_fn_calls, &mut free_fn_calls,
&mut warnings_discarded, &mut warnings_discarded,
&mut crate::linearity::LetBinderTypes::new(),
)?; )?;
// Build two per-channel slot lists — one for class-method // Build two per-channel slot lists — one for class-method
crates/ailang-check/tests/workspace.rs
+1 -1
View File
@@ -725,7 +725,7 @@ fn borrow_own_demo_is_linearity_clean() {
/// is active today) and were RED before the hardening (docs/specs/0063). /// is active today) and were RED before the hardening (docs/specs/0063).
#[test] #[test]
fn harden_ownership_false_positives_are_clean() { fn harden_ownership_false_positives_are_clean() {
for name in ["fp_value", "fp_hof", "fp_map"] { for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let"] {
let entry = examples_dir().join(format!("{name}.ail")); let entry = examples_dir().join(format!("{name}.ail"));
let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}")); let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}"));
let diags = check_workspace(&ws); let diags = check_workspace(&ws);
examples/c3_value_let.ail
+10
View File
@@ -0,0 +1,10 @@
(module c3_value_let
(fn iterate
(doc "xnew is a Float let-binder used in cond and both branches")
(type (fn-type (params (own (con Float)) (own (con Float))) (ret (own (con Float)))))
(params x tol)
(body
(let xnew (app / x 2.0)
(if (app float_lt (app - xnew x) tol)
xnew
xnew)))))