AILang/docs/plans/0111-unique-binder-names.md

Unique Binder Names per Fn — Implementation Plan

Parent spec: docs/specs/0056-unique-binder-names.md

For agentic workers: REQUIRED SUB-SKILL: use the implement skill to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Make every binder name unique within its fn by alpha-renaming shadowing binders during desugaring, so the uniqueness side-table key (def_name, binder_name) is injective again — closing the A2b leg of RawBuf drop-leak #43.

Architecture: The lexical scope threaded through desugar_term becomes a small Scope struct carrying two maps: entries keyed by each binder's effective (post-rename) name (feeding the existing type/capture lookups unchanged), and rename mapping every in-scope authored name to its current effective name (the shadow-detector and the Term::Var resolver). At each binder-introduction site (Let, flat-Match pattern-binders, Lam params, Loop binders) a binder whose authored name is already bound gets a fresh <name>$<n> name; its references resolve through rename. Never-renamed binders (fn-params, LetRec name/params) record an identity rename so an inner renamable binder that shadows them is still detected. No consumer of the uniqueness table changes — they all key by name, and the name is now a per-fn injective identity.

Tech Stack: crates/ailang-core/src/desugar.rs (the entire fix), crates/ailang-check/src/uniqueness.rs (doc-comment correction only). The four RED tests and their fixtures already exist in the tree (crates/ail/tests/e2e.rs, examples/{raw_buf_*,flat_pat_shadow_*}.ail).

---

Files this plan creates or modifies

• Modify: crates/ailang-core/src/desugar.rs — add Scope struct + impl after ScopeEntry (line 144); add Desugarer::fresh_binder (after line 455); add free fn rename_pattern_binders; change desugar_term's scope parameter type and rewrite every binder site + Term::Var + the two def-boundary scope constructions.
• Modify: crates/ailang-check/src/uniqueness.rs:90-98 — correct the UniquenessTable doc-comment (pop-order + "every fixture unique" claims are both wrong).
• Test (pre-existing, RED today): crates/ail/tests/e2e.rs — raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats, flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed.
• Test (new, regression guard): crates/ailang-core/src/desugar.rs in-source #[cfg(test)] mod tests — a shadowing-let desugar unit test and a letrec-captures-shadowed-binder robustness test.

---

Task 1: Scope-with-renames + rename-on-shadow across all binder sites

This task is one atomic compilation unit: changing desugar_term's scope parameter type forces every scope-construction and scope-mutation site to update in the same task. It ends with a clean cargo build -p ailang-core and the existing in-source desugar tests still green (non-shadowing output is byte-identical).

Files:

• Modify: crates/ailang-core/src/desugar.rs

• Step 1: Add the Scope struct and impl

Insert immediately after the ScopeEntry enum's closing brace (after line 144, before the /// Rewrite m … doc-comment on line 146):

/// Lexical scope threaded through desugaring.
///
/// `entries` is keyed by each binder's **effective** (post-shadow-
/// rename) name and feeds the existing type-/capture-lookups
/// unchanged. `rename` maps every in-scope **authored** name to its
/// current effective name; it is the shadow-detector ([`is_bound`])
/// and the [`Term::Var`] resolver ([`resolved_name`]).
///
/// For a program with no shadowing, every effective name equals its
/// authored name and `rename` is all-identity, so the desugared
/// output is byte-identical to the pre-rename pass.
///
/// [`is_bound`]: Scope::is_bound
/// [`resolved_name`]: Scope::resolved_name
#[derive(Clone, Default)]
struct Scope {
    entries: BTreeMap<String, ScopeEntry>,
    rename: BTreeMap<String, String>,
}

impl Scope {
    /// Is the **effective** name `eff` an entry here? (capture /
    /// type lookups, which operate on the desugared tree's names).
    fn contains_key(&self, eff: &str) -> bool {
        self.entries.contains_key(eff)
    }

    /// The [`ScopeEntry`] for an **effective** name.
    fn get(&self, eff: &str) -> Option<&ScopeEntry> {
        self.entries.get(eff)
    }

    /// Is the **authored** name already lexically bound here? — the
    /// shadow test. True for any binder kind, including identity-
    /// renamed fixed binders (fn-params, LetRec name/params).
    fn is_bound(&self, authored: &str) -> bool {
        self.rename.contains_key(authored)
    }

    /// Resolve an **authored** name to its current effective name.
    /// Verbatim for free names (module-level fns, builtins, ctors),
    /// which were never bound at a binder site in this fn.
    fn resolved_name(&self, authored: &str) -> String {
        self.rename
            .get(authored)
            .cloned()
            .unwrap_or_else(|| authored.to_string())
    }

    /// Install a possibly-renamed binder: record `entries[effective]`
    /// and `rename[authored → effective]`.
    fn insert_effective(&mut self, authored: &str, effective: String, entry: ScopeEntry) {
        self.entries.insert(effective.clone(), entry);
        self.rename.insert(authored.to_string(), effective);
    }

    /// Install a never-renamed binder (fn-params, LetRec name/params).
    /// The identity rename keeps the name visible to [`is_bound`] so an
    /// inner *renamable* binder that shadows it is still detected.
    fn insert_fixed(&mut self, name: &str, entry: ScopeEntry) {
        self.entries.insert(name.to_string(), entry);
        self.rename.insert(name.to_string(), name.to_string());
    }
}

• Step 2: Add the fresh_binder generator

Insert into the impl Desugarer block immediately after fresh_lifted (after line 455, before the /// Recursively rewrites … doc on 457):

    /// A binder name unique within the current fn: `<base>$<n>` with
    /// the lowest `n ≥ 1` free in both `scope` (in-scope effective
    /// names) and `used` (the `$mp_` / `$lr_` synthetic space).
    /// Records the minted name in `used` so a later mint is distinct.
    /// Authored names cannot contain `$` (the lexer reserves it for
    /// synthetic names), so `<base>$<n>` never collides with an
    /// authored binder.
    fn fresh_binder(&mut self, base: &str, scope: &Scope) -> String {
        let mut n = 1u64;
        loop {
            let candidate = format!("{base}${n}");
            n += 1;
            if !self.used.contains(&candidate) && !scope.contains_key(&candidate) {
                self.used.insert(candidate.clone());
                return candidate;
            }
        }
    }

• Step 3: Add the rename_pattern_binders free fn

Insert near the other pattern free fns (immediately before the pattern_binds fn at line 1281 — locate it by fn pattern_binds):

/// Rewrites the `Pattern::Var` binder names in `pat` per `renamed`
/// (authored → effective); leaves `Wild` / `Lit` and any binder not in
/// the map untouched. Threads shadow-renamed flat-pattern binders into
/// the emitted pattern so codegen's arm-close drop gate keys by the
/// same renamed name the arm body references.
fn rename_pattern_binders(pat: &Pattern, renamed: &BTreeMap<String, String>) -> Pattern {
    match pat {
        Pattern::Wild => Pattern::Wild,
        Pattern::Lit { lit } => Pattern::Lit { lit: lit.clone() },
        Pattern::Var { name } => Pattern::Var {
            name: renamed.get(name).cloned().unwrap_or_else(|| name.clone()),
        },
        Pattern::Ctor { ctor, fields } => Pattern::Ctor {
            ctor: ctor.clone(),
            fields: fields
                .iter()
                .map(|f| rename_pattern_binders(f, renamed))
                .collect(),
        },
    }
}

• Step 4: Change desugar_term's signature and split the Var arm

At line 475, change the parameter type:

    fn desugar_term(&mut self, t: &Term, scope: &Scope) -> Term {

At line 477, replace the shared Lit | Var arm:

            Term::Lit { .. } => t.clone(),
            Term::Var { name } => Term::Var {
                name: scope.resolved_name(name),
            },

• Step 5: Rewrite the Term::Let binder site

Replace lines 483-493 (the Term::Let arm):

            Term::Let { name, value, body } => {
                let v = self.desugar_term(value, scope);
                let mut inner = scope.clone();
                let effective = if inner.is_bound(name) {
                    self.fresh_binder(name, &inner)
                } else {
                    name.clone()
                };
                inner.insert_effective(name, effective.clone(), ScopeEntry::LetBound);
                let b = self.desugar_term(body, &inner);
                Term::Let {
                    name: effective,
                    value: Box::new(v),
                    body: Box::new(b),
                }
            }

• Step 6: Rewrite the Term::Match arm loop (rename pattern binders)

Replace lines 509-528 (the Term::Match arm):

            Term::Match { scrutinee, arms } => {
                // Recurse into children first (bottom-up).
                let scrutinee = self.desugar_term(scrutinee, scope);
                let arms: Vec<Arm> = arms
                    .iter()
                    .map(|a| {
                        let mut inner = scope.clone();
                        let mut pat_binds: BTreeSet<String> = BTreeSet::new();
                        pattern_binds(&a.pat, &mut pat_binds);
                        let mut renamed: BTreeMap<String, String> = BTreeMap::new();
                        for n in &pat_binds {
                            let effective = if inner.is_bound(n) {
                                self.fresh_binder(n, &inner)
                            } else {
                                n.clone()
                            };
                            if effective != *n {
                                renamed.insert(n.clone(), effective.clone());
                            }
                            inner.insert_effective(n, effective, ScopeEntry::MatchArm);
                        }
                        let pat = if renamed.is_empty() {
                            a.pat.clone()
                        } else {
                            rename_pattern_binders(&a.pat, &renamed)
                        };
                        Arm {
                            pat,
                            body: self.desugar_term(&a.body, &inner),
                        }
                    })
                    .collect();
                self.desugar_match(scrutinee, arms)
            }

• Step 7: Rewrite the Term::Lam param loop

Replace lines 529-547 (the Term::Lam arm):

            Term::Lam {
                params,
                param_tys,
                ret_ty,
                effects,
                body,
            } => {
                let mut inner = scope.clone();
                let mut new_params: Vec<String> = Vec::with_capacity(params.len());
                for (p, pty) in params.iter().zip(param_tys.iter()) {
                    let effective = if inner.is_bound(p) {
                        self.fresh_binder(p, &inner)
                    } else {
                        p.clone()
                    };
                    inner.insert_effective(p, effective.clone(), ScopeEntry::KnownType(pty.clone()));
                    new_params.push(effective);
                }
                Term::Lam {
                    params: new_params,
                    param_tys: param_tys.clone(),
                    ret_ty: ret_ty.clone(),
                    effects: effects.clone(),
                    body: Box::new(self.desugar_term(body, &inner)),
                }
            }

• Step 8: Rewrite the Term::Loop binder loop

Replace lines 563-586 (the Term::Loop arm):

            Term::Loop { binders, body } => {
                // loop-recur iter 1: structural recursion. Each
                // binder's init is desugared in scope of the outer env
                // plus already-declared binders; the body sees all
                // binders. A binder whose name shadows an enclosing
                // binding is alpha-renamed (uniqueness-table injectivity).
                let mut inner = scope.clone();
                let new_binders: Vec<LoopBinder> = binders
                    .iter()
                    .map(|b| {
                        let init = self.desugar_term(&b.init, &inner);
                        let effective = if inner.is_bound(&b.name) {
                            self.fresh_binder(&b.name, &inner)
                        } else {
                            b.name.clone()
                        };
                        inner.insert_effective(&b.name, effective.clone(), ScopeEntry::LetBound);
                        LoopBinder {
                            name: effective,
                            ty: b.ty.clone(),
                            init,
                        }
                    })
                    .collect();
                Term::Loop {
                    binders: new_binders,
                    body: Box::new(self.desugar_term(body, &inner)),
                }
            }

• Step 9: Update the Term::LetRec arm to the new scope API

The LetRec name and its params are not renamed (out of the spec's renamable set; a lifted LetRec gets its own def namespace, so its binders cannot collide in the (def, name) key). They use insert_fixed so an inner renamable binder that shadows them is still detected, and so capture detection — which reads the effective names of the desugared body — keeps working when an enclosing binder was renamed (the effective name is in entries).

In lines 644-655, replace the four scope mutations:

                // Body's scope: outer ∪ {name → EnclosingLetRec} ∪
                // params with their declared types as KnownType.
                let mut body_scope = scope.clone();
                body_scope.insert_fixed(name, ScopeEntry::EnclosingLetRec);
                for (p, pty) in params.iter().zip(inner_params_tys.iter()) {
                    body_scope.insert_fixed(p, ScopeEntry::KnownType(pty.clone()));
                }
                let desugared_body = self.desugar_term(body, &body_scope);
                // in_term's scope: outer ∪ {name → EnclosingLetRec}
                // (params are lambda-local to the LetRec's body,
                // not visible in `in`).
                let mut in_scope = scope.clone();
                in_scope.insert_fixed(name, ScopeEntry::EnclosingLetRec);
                let desugared_in = self.desugar_term(in_term, &in_scope);

No other change in the LetRec arm: the capture-detection scope.contains_key(*f) (line 714) and scope.get(c) (lines 733, 776) now resolve through the delegating methods and read effective names — exactly the names present in the desugared body. The defer-path Term::LetRec { name: name.clone(), … } (line 765) is unchanged (the LetRec name is never renamed).

• Step 10: Convert the two def-boundary scope constructions

Def::Fn (lines 219-247): change the construction and both param inserts. Replace line 219:

                let mut scope = Scope::default();

Replace line 235 (inside the KnownType arm):

                            scope.insert_fixed(p, ScopeEntry::KnownType(pty.clone()));

Replace line 244 (inside the defensive LetBound fallback):

                            scope.insert_fixed(p, ScopeEntry::LetBound);

Def::Const (line 259): replace:

                let scope = Scope::default();

• Step 11: Build gate — ailang-core compiles clean

Run: cargo build -p ailang-core 2>&1 | tail -5 Expected: finishes with no error[ lines (warnings tolerated).

• Step 12: Non-shadow regression — existing desugar tests green

Run: cargo test -p ailang-core 2>&1 | tail -15 Expected: test result: ok. — every existing in-source desugar test passes. (These feed no shadowing input, so their desugared output is byte-identical; this is the evidence the rename is on-shadow-only.)

---

Task 2: Turn the four RED tests GREEN + correct the doc-comment

Files:

• Modify: crates/ailang-check/src/uniqueness.rs:90-98

• Test (pre-existing): crates/ail/tests/e2e.rs

• Step 1: Correct the UniquenessTable doc-comment

Replace the doc-comment at crates/ailang-check/src/uniqueness.rs:90-98 (the block directly above pub type UniquenessTable = … on line 99):

/// Side table indexed by `(def_name, binder_name)`. Built fresh for
/// each codegen invocation; the side table is not cached.
///
/// The key is injective per fn: desugaring alpha-renames any binder
/// whose name shadows an enclosing binding to a fresh `<name>$<n>`
/// (see `ailang-core::desugar`), so within one `def_name` every
/// `binder_name` denotes exactly one binding. Codegen consumers look
/// up by current-scope binder name and always resolve the binding
/// they mean — there is no shadow collapse.

• Step 2: Let-shadow leak tests pass

Run: cargo test -p ail --test e2e shadow_rebind 2>&1 | tail -8 Expected: PASS for raw_buf_int_shadow_rebind_drop_balances_rc_stats, raw_buf_float_shadow_rebind_drop_balances_rc_stats, raw_buf_bool_shadow_rebind_drop_balances_rc_stats (live == 0; they asserted live == 1 RED before this fix).

• Step 3: Flat-pattern differential test passes

Run: cargo test -p ail --test e2e flat_pat_shadow 2>&1 | tail -8 Expected: PASS for flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed (shadow live now equals the alpha-renamed control's live; it was 5 vs 3 RED before).

• Step 4: Full workspace suite — no regressions

Run: cargo test 2>&1 | tail -20 Expected: every crate reports test result: ok.; no failures, no fixture whose output drifted.

---

Task 3: Regression guard — letrec capture of a shadow-renamed binder

The LetRec-capture interaction (Task 1 Step 9) is load-bearing but has no fixture today. This unit test pins it: a let that shadows an outer let, with a Term::LetRec in the inner scope whose body captures the shadowed binder. The captured Term::Var in the desugared output must carry the renamed name and remain a recognised capture (no UnknownVar-class free var leaks into the lifted/deferred fn).

Files:

• Test (new): crates/ailang-core/src/desugar.rs in-source #[cfg(test)] mod tests.

• Step 1: Add a shadowing-let desugar unit test

Add to the in-source #[cfg(test)] mod tests (locate it by mod tests; place the test beside the existing flat_match_is_unchanged_shape test):

    /// A `let` that shadows an enclosing same-named `let` is
    /// alpha-renamed to a fresh `<name>$<n>`, and references in its
    /// body resolve to the renamed binder — the uniqueness-table
    /// `(def, name)` key is injective per fn (refs #43).
    #[test]
    fn shadowing_let_is_alpha_renamed() {
        let mut d = Desugarer {
            counter: 0,
            used: BTreeSet::new(),
            lifted: Vec::new(),
            module_top_names: BTreeSet::new(),
            current_def_forall_vars: Vec::new(),
        };
        // (let x 1 (let x (+ x 1) x))
        let inner = Term::Let {
            name: "x".into(),
            value: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "+".into() }),
                args: vec![
                    Term::Var { name: "x".into() },
                    Term::Lit { lit: Literal::Int { value: 1 } },
                ],
                tail: false,
            }),
            body: Box::new(Term::Var { name: "x".into() }),
        };
        let outer = Term::Let {
            name: "x".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
            body: Box::new(inner),
        };
        let out = d.desugar_term(&outer, &Scope::default());
        // Outer binder keeps `x`; inner binder becomes `x$1`; the
        // inner value's `x` ref resolves to the outer `x`; the inner
        // body's `x` ref resolves to `x$1`.
        let Term::Let { name: o_name, body: o_body, .. } = &out else {
            panic!("expected outer Let, got {out:?}");
        };
        assert_eq!(o_name, "x");
        let Term::Let { name: i_name, value: i_val, body: i_body } = o_body.as_ref() else {
            panic!("expected inner Let, got {o_body:?}");
        };
        assert_eq!(i_name, "x$1", "shadowing inner binder must be renamed");
        // inner value `(+ x 1)` still refers to the outer `x`
        let Term::App { args, .. } = i_val.as_ref() else {
            panic!("expected App in inner value, got {i_val:?}");
        };
        assert!(
            matches!(&args[0], Term::Var { name } if name == "x"),
            "inner value's ref must resolve to outer `x`, got {:?}",
            args[0]
        );
        // inner body `x` resolves to the renamed `x$1`
        assert!(
            matches!(i_body.as_ref(), Term::Var { name } if name == "x$1"),
            "inner body's ref must resolve to renamed `x$1`, got {i_body:?}",
        );
    }

Term, Literal, Scope, Desugarer, and BTreeSet resolve via the test module's use super::*; (the same path the neighbouring flat_match_is_unchanged_shape test uses); confirm that import is present and add the missing names to it if not.

• Step 2: Run the new unit test

Run: cargo test -p ailang-core shadowing_let_is_alpha_renamed 2>&1 | tail -8 Expected: PASS.

• Step 3: Re-confirm the full ailang-core suite

Run: cargo test -p ailang-core 2>&1 | tail -8 Expected: test result: ok.