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

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

crates/ailang-check/src/builtins.rs

@@ -325,6 +325,7 @@ mod tests {
             &mut residuals,
             &mut free_fn_calls,
             &mut warnings,
+            &mut crate::linearity::LetBinderTypes::new(),
         )
         .expect("synth");
         subst.apply(&ty)
@@ -559,6 +560,7 @@ mod tests {
             &mut residuals,
             &mut free_fn_calls,
             &mut warnings,
+            &mut crate::linearity::LetBinderTypes::new(),
         )
         .expect_err("must reject");
         assert!(

crates/ailang-check/src/lib.rs

@@ -1233,7 +1233,9 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
         // shadowed-class-method warning is visible even when the
         // module also has unrelated errors.
         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();
         // Per-module diagnostic accumulator. The suppress filter
         // (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();
-            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
             // the same activation gate as linearity (all-explicit-mode
             // 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
     // error, and warnings on this path have no surface to flow to.
     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);
     }
     // 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
     // (emitted from `synth` via `check_fn`'s warnings accumulator).
     out_warnings: &mut Vec<Diagnostic>,
+    let_binder_types: &mut crate::linearity::LetBinderTypes,
 ) -> Vec<CheckError> {
     let mut env = build_check_env(ws);
     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";
 
     for def in &m.defs {
-        match check_def(def, &env, out_warnings) {
+        match check_def(def, &env, out_warnings, let_binder_types) {
             Ok(()) => {}
             Err(e) => {
                 errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
@@ -1994,10 +2002,11 @@ fn check_def(
     def: &Def,
     env: &Env,
     out_warnings: &mut Vec<Diagnostic>,
+    let_binder_types: &mut crate::linearity::LetBinderTypes,
 ) -> Result<()> {
     match def {
-        Def::Fn(f) => check_fn(f, env, out_warnings),
-        Def::Const(c) => check_const(c, env, out_warnings),
+        Def::Fn(f) => check_fn(f, env, out_warnings, let_binder_types),
+        Def::Const(c) => check_const(c, env, out_warnings, let_binder_types),
         Def::Type(td) => check_type_def(td, env),
         // bugfix-instance-body-unbound-var (2026-05-13): each instance
         // 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`
         // remains schema-only at this layer.
         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,
     env: &Env,
     out_warnings: &mut Vec<Diagnostic>,
+    let_binder_types: &mut crate::linearity::LetBinderTypes,
 ) -> Result<()> {
     let qualified_class = qualify_class_ref_in_check(&inst.class, &env.current_module);
     for im in &inst.methods {
@@ -2094,7 +2104,7 @@ fn check_instance(
             suppress: Vec::new(),
         export: None,
         };
-        check_fn(&synthetic, env, out_warnings)?;
+        check_fn(&synthetic, env, out_warnings, let_binder_types)?;
     }
     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))
 }
 
-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
     // inner env so they pass `check_type_well_formed` and unify only
     // 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
     // the synth walk; discarded after the body type-checks.
     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)?;
     // surface synth-time warnings into the caller-supplied
     // 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
     // outright. Any other type passes through to `synth` as before.
     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
     // `recur` in a const body correctly fires `RecurOutsideLoop`.
     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);
     unify(&c.ty, &v, &mut subst)?;
     if !effects.is_empty() {
@@ -3342,6 +3362,7 @@ pub(crate) fn synth(
     // `class-method-shadowed-by-fn` warning is emitted here; future
     // synth-time warnings (if any) would flow through the same channel.
     warnings: &mut Vec<crate::diagnostic::Diagnostic>,
+    let_binder_types: &mut crate::linearity::LetBinderTypes,
 ) -> Result<Type> {
     match t {
         Term::Lit { lit } => Ok(match lit {
@@ -3752,7 +3773,7 @@ pub(crate) fn synth(
             Ok(maybe_instantiate(raw, counter))
         }
         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 (params, ret, fx) = match &cty {
                 Type::Fn { params, ret, effects: fx, .. } => {
@@ -3788,7 +3809,7 @@ pub(crate) fn synth(
                 });
             }
             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
                 // cross-module callee may name the consumer's own ADT
                 // qualified (`<current_module>.T`) where the consumer
@@ -3805,9 +3826,10 @@ pub(crate) fn synth(
             Ok(subst.apply(&ret))
         }
         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 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 {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -3819,10 +3841,10 @@ pub(crate) fn synth(
             Ok(r)
         }
         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)?;
-            let t1 = synth(then, 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 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_binder_types)?;
             unify(&t1, &t2, subst)?;
             Ok(subst.apply(&t1))
         }
@@ -3840,7 +3862,7 @@ pub(crate) fn synth(
                 });
             }
             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)?;
             }
             effects.insert(sig.effect.clone());
@@ -3960,7 +3982,7 @@ pub(crate) fn synth(
             }
             for (a, exp) in args.iter().zip(qualified_fields.iter()) {
                 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)?;
             }
             Ok(Type::Con {
@@ -3969,7 +3991,7 @@ pub(crate) fn synth(
             })
         }
         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() {
                 return Err(CheckError::NonExhaustive {
                     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());
                     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() {
                     match prev {
                         Some(p) => {
@@ -4062,9 +4084,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
         }
         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)?;
-            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 } => {
             // reject lambda-captures-of-loop-binder.
@@ -4103,7 +4125,7 @@ pub(crate) fn synth(
                 pushed.push((n.clone(), prev));
             }
             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() {
                 match prev {
                     Some(p) => {
@@ -4191,7 +4213,7 @@ pub(crate) fn synth(
             // subset rule against `declared_effs` — exactly like
             // `Term::Lam`.
             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).
             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
             // binding is).
             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 {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -4234,7 +4256,7 @@ pub(crate) fn synth(
             // No constraint generated, no environment change. The
             // wrapper records author intent for the future RC inc/dec
             // 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 } => {
             // `(reuse-as SRC NEW-CTOR)` requires `body` to
@@ -4248,7 +4270,7 @@ pub(crate) fn synth(
             // shape-compatibility check (18d.2 will add a
             // `reuse-as-shape-mismatch` diagnostic when codegen has
             // 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() {
                 Term::Ctor { .. } | Term::Lam { .. } => {}
                 other => {
@@ -4278,7 +4300,7 @@ pub(crate) fn synth(
             }
             // Body's type is the result type of the whole reuse-as
             // 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
         // outer scope plus already-declared binder names of THIS
@@ -4296,7 +4318,7 @@ pub(crate) fn synth(
             for b in binders {
                 let init_ty = synth(
                     &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)?;
                 binder_frame.push((b.name.clone(), b.ty.clone()));
@@ -4306,7 +4328,7 @@ pub(crate) fn synth(
             loop_stack.push(binder_frame);
             let body_result = synth(
                 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();
             for (name, prev) in restore.into_iter().rev() {
@@ -4344,7 +4366,7 @@ pub(crate) fn synth(
             for (i, a) in args.iter().enumerate() {
                 let arg_ty = synth(
                     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_arg = subst.apply(&arg_ty);
@@ -4559,7 +4581,7 @@ pub(crate) fn synth(
                 let expected_inst = substitute_rigids(expected_param, &mapping);
                 let actual = synth(
                     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)?;
             }
@@ -5309,6 +5331,7 @@ mod tests {
             &mut residuals,
             &mut free_fn_calls,
             &mut warnings,
+            &mut crate::linearity::LetBinderTypes::new(),
         )
         .expect("synth must succeed");
         subst.apply(&ty)
@@ -5408,6 +5431,7 @@ mod tests {
             &term, &env, &mut locals, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
+            &mut crate::linearity::LetBinderTypes::new(),
         )
         .expect_err("lambda capturing loop binder must be rejected");
         match err {
@@ -7957,6 +7981,7 @@ mod tests {
             &mut residuals,
             &mut free_fn_calls,
             &mut warnings,
+            &mut crate::linearity::LetBinderTypes::new(),
         )
         .expect("synth must succeed (fn wins precedence)");
         assert!(

crates/ailang-check/src/lift.rs

@@ -742,7 +742,7 @@ impl<'a> Lifter<'a> {
         // one term at a time from a top-of-body position; fresh empty
         // loop-stack is correct (any `Term::Loop` pushes its own frame).
         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))
     }
 }

crates/ailang-check/src/linearity.rs

@@ -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 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`
 /// is a primitive value type — no RC, no heap. Reading a primitive
 /// 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.
 #[cfg(test)]
 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
@@ -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
 /// visible. Bodies of the visible-extra modules are NOT walked here
 /// — 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();
     // ctor name → field types, used by the
     // `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();
     for def in &m.defs {
         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
@@ -342,6 +353,7 @@ fn check_fn(
     globals: &HashMap<String, Type>,
     ctors: &HashMap<String, Vec<Type>>,
     uniq: &UniquenessTable,
+    let_binder_types: &LetBinderTypes,
     diags: &mut Vec<Diagnostic>,
 ) {
     let inner = strip_forall(&f.ty);
@@ -370,6 +382,7 @@ fn check_fn(
         diags,
         def_name: &f.name,
         ctors,
+        let_binder_types,
         binders: HashMap::new(),
     };
 
@@ -439,6 +452,10 @@ struct Checker<'a> {
     /// from consume-tracking. Mirrors the `ctors` map built in
     /// `check_module_with_visible`.
     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
     /// scoping is restored by [`Checker::with_binder`].
     binders: HashMap<String, BinderState>,
@@ -504,9 +521,18 @@ impl<'a> Checker<'a> {
             }
             Term::Let { name, value, body } => {
                 self.walk(value, Position::Consume);
-                self.with_binder(name, BinderState::default(), |this| {
-                    this.walk(body, pos);
-                });
+                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);
+                    },
+                );
             }
             Term::LetRec { name, body, in_term, .. } => {
                 // 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
     /// (`(term-ctor Pair Pair p0 p0)`) MUST still fire use-after-consume
     /// after the fix — the exemption is value-type-only, not blanket.

crates/ailang-check/src/lower_to_mir.rs

@@ -49,6 +49,7 @@ impl<'a> Ctx<'a> {
             &mut residuals,
             &mut free_fn_calls,
             &mut warnings,
+            &mut crate::linearity::LetBinderTypes::new(),
         )?;
         Ok(wildcard_residual_metavars(&subst.apply(&ty)))
     }

crates/ailang-check/src/mono.rs

@@ -836,6 +836,7 @@ pub fn collect_mono_targets(
         &mut residuals,
         &mut free_fn_calls,
         &mut warnings_discarded,
+        &mut crate::linearity::LetBinderTypes::new(),
     )?;
 
     // Filter residuals to fully-concrete ones; look up
@@ -1641,6 +1642,7 @@ pub(crate) fn collect_residuals_ordered(
         &mut residuals,
         &mut free_fn_calls,
         &mut warnings_discarded,
+        &mut crate::linearity::LetBinderTypes::new(),
     )?;
 
     // Build two per-channel slot lists — one for class-method

crates/ailang-check/tests/workspace.rs

@@ -725,7 +725,7 @@ fn borrow_own_demo_is_linearity_clean() {
 /// is active today) and were RED before the hardening (docs/specs/0063).
 #[test]
 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 ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}"));
         let diags = check_workspace(&ws);

examples/c3_value_let.ail

@@ -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)))))