The two halves of the global-uniqueness condition (GUC, #139) become
checkable: UniqueBinders (no binder name bound twice per top-level
site, the magic-do discard binder _ exempt while unreferenced) and
IndicesZero (every local ref at De Bruijn index 0). The checked runner
dispatches each declared invariant to its own linter. No pass declares
the new invariants yet, so behaviour is unchanged.

lintUberModule is renamed to lintWellScoped now that it is one check
of three; discardName moves to IR.Names so the linter and magic-do
share one definition.

A strengthened renameShadowedNamesInExpr: a used-names accumulator is
threaded sequentially through the whole top-level site (on top of the
scope map that resolves (name, index) references), so parallel
duplicate binders are renamed as well as shadowing ones — full
per-site uniqueness with every reference at index 0. Foreigns are
covered alongside bindings and exports, and the runtime lazy factory
name seeds the accumulator so it is never minted.

Not wired into the pipeline yet: that switch, with its golden churn,
comes separately.

uniquifyNames becomes the entry pass, establishing UniqueBinders +
IndicesZero (GUC) which every later pass declares and preserves; the
checked runner lints the contract at every pass boundary. Term
duplication now freshens binders through the shared supply:
substituteCopyM freshens every inserted copy (local and cross-entry
inlining), substituteMoveM keeps the first occurrence verbatim when
the source binder is consumed (beta reduction, magic-do spine
classification). Zero matching occurrences draw no supply names, which
keeps the optimize fixpoint convergent and golden numbering stable.

The De Bruijn index arithmetic is dismantled: shift/unshift/
overFreeIndex and the capture-avoiding substitute are gone, DCE
resolves references by name without index-keyed scopes and drops dead
binders with no unshift, magicDo and renameShadowedNames-era ordering
constraints disappear (the rename pass itself is deleted; uniquify
subsumes it). FlattenDeepBinds mints fresh helper parameters instead
of reusing chain binder names, which UniqueBinders now forbids.

One module-wide wave of structural golden churn (76 files); all 23
eval oracles pass unchanged.

The GHCi-daemon build/test monitor (github:atelier-hub/tricorder),
plus its cachix binary cache, for a faster feedback loop than
re-running cabal build.

freshenBinders and substituteCopyM/substituteMoveM had only indirect
coverage through the pipeline and goldens. Pin their contracts:
copy-vs-move freshening, no descent into insertions, free references
untouched, alpha-equivalence on GUC-shaped input, and the zero-match ⇒
zero-supply-draws guarantee the optimize fixpoint depends on. The
whole-pipeline property now asserts all three invariants, not just
well-scopedness.

Note [Sequential scoping of Let bindings] now also lists alphaEq and
the linter's unboundLocals among the walkers that must implement the
pre-GUC convention.

The scopedExp generator deliberately excluded Let while the sequential
scoping convention was each pass's job to re-implement; now that the
GUC properties (uniquify, freshenBinders, the full optimizer pipeline,
the linters) all ride on this generator, Let is exactly the binding
form they must see. Groupings thread the scope sequentially per Note
[Sequential scoping of Let bindings]: a Standalone RHS is generated
under the pre-binding scope, recursive-group members (distinct names)
see the whole group. Names come from the shared pool, so shadowing and
parallel duplicates arise naturally.

DCE resolves references by name alone now and requires GUC input, but
the spec neither supplied it nor checked that DCE keeps it. Add the
unit-level twin of the dcePass ensures-contract: on uniquified
scopedExp input (Let forms included since the previous commit), the
output satisfies all three invariants. Make the unused-parameter test
honest about the precondition by uniquifying the body and keeping the
minted binder out of its bound names, and drop the let*-resolution
test: two same-named Let siblings cannot reach DCE anymore, and the
sequential scoping it exercised is covered by Uniquify.Spec.

The --lint-ir failure message was rendered inline in the executable,
unreachable from the test suite. Move the rendering (verbatim) next to
the PassCheckFailure type and pin the exact user-facing text with a
unit test; the CLI handler now just dies with the rendered message.

Reflexivity was the only algebraic law pinned. Independent Gen.exp
pairs cover the mismatch branches; the flipped uniquify direction
covers the equivalent case, which the Uniquify.Spec property checks
only one way around.

Every producer of a nonzero index is gone: the CoreFn translation
emits references that resolve to the innermost binder of their name
(which is what lexical scoping means), and the optimizer rewrites
freshen binders instead of shifting indices. The Ref node therefore
carries a name only, and the IndicesZero invariant, its linter check,
and the index arithmetic in alphaEq, countFreeRefs, qualifyTopRefs,
uniquify and the well-scopedness lint are deleted; scopes become name
sets. GUC is UniqueBinders alone: a nonzero index is unrepresentable
rather than linted against.

The uniquify pass keeps its per-name rename stack (the stack depth
seeds the digit-suffix numbering), so minted names are unchanged:
golden.lua files are untouched and eval oracles pass byte-identical;
golden.ir files lose only the printed index field.

The Lua backend renders every local reference as a plain variable,
which retires the UnexpectedRefBound error. The inliner test that
expected a verbatim inserted copy now compares up to alpha-equivalence
(substituteCopyM freshens the binders of every insertion) — the
verbatim expectation was latently flaky whenever the generated inlinee
contained a binder.