The IR currently represents locals as name plus per-name De Bruijn index (Ref (Local x) i counts enclosing x binders, Dhall-style), and capture avoidance is index arithmetic: substitute shifts the replacement under same-name binders, passes that drop binders must unshift, and every traversal reimplements the sequential Let scoping convention. The scheme is sound on paper, but its invariant is distributed across every pass, and the bug record shows what that costs: #37 (three walkers with the convention inverted), #56 (missing unshift in beta reduction), #133 (renameShadowedNames wrong scope in recursive groups), #134 (DCE: reversed body scope, missing unshift). Six independent bugs, one root. Because shifts are only needed under shadowing, these bugs are silent until a shadowed name reaches the pass, which is the worst failure mode available.

This issue proposes switching the pipeline to a global uniqueness condition (GUC), the discipline used by the Plutus compiler: make all local binders unique once, up front, and keep them unique, so that every downstream pass can treat names naively. The alternatives considered and rejected, briefly: pure De Bruijn everywhere trades readability of goldens and cheap subtree motion for canonical alpha-equivalence, which fits evaluators and wire formats (UPLC) but not a rewriting optimizer, since every structural edit becomes index migration; GHC's rapier (per-pass substitution plus in-scope set, no global invariant) is the strongest option at GHC's scale but its costs land exactly where pslua is weakest, since a forgotten in-scope-set extension fails silently and the machinery is the trickiest in this design space, while its payoff (no whole-program rename between simplifier iterations) is worthless for programs of pslua's size; locally nameless was tried in this codebase's history and rejected for the monadic boilerplate it spread. GUC with a mechanical linter keeps failures loud, which is the property that matters most for a single-maintainer project whose main safety net is golden tests.

Target invariants

After the entry rename pass and until codegen: all local binders are unique within a top-level binding, every local Ref has index 0, and every pass declares whether it requires and preserves these invariants (via the Pass contract from #138). The linter checks the declarations after every pass in the test harness.

Plan

Prerequisites, tracked separately: #138 (Pass values, linter, deterministic SupplyM) and the #133/#134 fixes. renameShadowedNames becomes the load-bearing entry pass, so its recursive-group defects must be fixed before the move.

The switch:

• uniquifyNames runs as the first IR pass after linking (the fixed renameShadowedNamesInExpr, moved from the end of the pipeline to the start). Establishes UniqueBinders and IndicesZero, which are added to the Invariant vocabulary.
• The inliner, the only pass that duplicates terms, re-uniquifies every inserted copy through the supply. A forgotten freshening turns the linter red on the first test.
• Index bookkeeping is dismantled: substitute drops its shift logic (asserting no shadowing instead), unshift becomes unnecessary (the Undefined variable in compiled code #37/Codegen: 'Unexpected bound reference Local b index 1' compiling Data.Array.foldRecM (index inflated by optimizer) #56/IR DCE mishandles Let bindings: no unshift after dropping a dead shadowing binder, body scope resolved in reverse #134 bug class dies by construction), DCE resolves references by name without scope maps, the final renameShadowedNames pass is deleted, and UnexpectedRefBound in codegen becomes a pure internal-invariant error. The Index field stays in the IR type for now with a linted always-zero invariant; physically removing it is a separate decision.
• Equality-based rules need care: after uniquification, alpha-equivalent branches stop being structurally equal, so removeIfWithEqualBranches would silently stop firing. Add an alphaEq comparison and audit other Eq-on-terms sites.
• Expect one large structural golden churn when uniquification lands (accepted via PSLUA_GOLDEN_ACCEPT); eval goldens must pass unchanged, as the semantic net.

Dividends once the switch is in: the float-in pass (#136) is written as an ordinary Pass requiring UniqueBinders, with no index surgery; the usage-count inefficiencies in optimizeModule become straightforward to fix incrementally.

The rapier remains documented as a possible future migration if compile times ever become a problem: the GUC architecture is a subset of it, so nothing here paints us into a corner.

Prerequisite of: #136. Depends on: #138, #133, #134. Origin: the 2026-07-02 backend audit and a follow-up design discussion of naming strategies (named + alpha-renaming, Barendregt, pure and per-name De Bruijn, locally nameless, GHC's rapier, Plutus GUC).