# 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):

```rust
/// 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):

```rust
    /// 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`):

```rust
/// 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:

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

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

```rust
            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):

```rust
            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):

```rust
            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):

```rust
            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):

```rust
            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:

```rust
                // 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:

```rust
                let mut scope = Scope::default();
```

Replace line 235 (inside the `KnownType` arm):

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

Replace line 244 (inside the defensive `LetBound` fallback):

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

`Def::Const` (line 259): replace:

```rust
                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):

```rust
/// 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):

```rust
    /// 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.`