IR Optimizer spec never terminates at hspec seeds 109, 152 and 478 #348

Problem

The IR Optimizer spec group contains optimization keeps expressions well-scoped, a hedgehog property that feeds generated well-scoped IR expressions through the whole optimizedUberModule pipeline (the full optimizer: uniquification, the optimize+dce fixpoint, and everything after it) and asserts that the result has no unbound local reference. On some inputs that call never returns.

The stall is reproducible once hspec's global seed is pinned. Over seeds 1..500 of the group, three of them — 109, 152 and 478 — never finish:

$ timeout 900 spec --match "IR Optimizer" --seed 109
exit=124 elapsed=900s

A complete run of the same group takes 0.35 s, so 900 seconds is over 2500× the normal cost, and the process was still killed by the cap rather than finishing. It is a livelock, not a memory blow-up: sampled over a minute the process holds 99.8 % of one core with a flat 50 MiB resident set, so nothing is growing — the optimizer is spinning.

The output stops at exactly the same place every time. These are the last lines before the process goes quiet, with the property that never reports:

    inlining bindings does not unbind let-bound references [✔]
        ✓ property passed 1 test.
    beta reduction does not unbind a reference shadowed by the binder [✔]
        ✓ property passed 1 test.
    blanking an unused shadowing binder keeps outer references bound [✔]
        ✓ property passed 1 test.

blanking an unused shadowing binder keeps outer references bound is the test declared immediately before the property, so the hang is inside optimization keeps expressions well-scoped itself.

How it shows up

As an intermittent CI/local hang rather than an assertion failure: with no --seed, hspec draws a random one, so roughly 3 runs in 500 of that group wedge and are eventually killed by whatever timeout wraps them. Repository policy already treats a hang as a failing test, not as flakiness, but the failure mode is easy to misread because the suite prints nothing at all — the group simply stops emitting lines.

Approach

The pipeline is a fixpoint (RunFixpoint "optimize+dce", plus the enclosing settle/lower phases), so the likeliest shape is two rewrites that undo each other on some generated term, with each round reporting Rewritten and the fixpoint never converging. A 1000-round backstop was added to the fixpoint in an earlier change; either these seeds spin inside a single round, or the spin is in a loop that the backstop does not cover.

Verification / Measurement

The group must complete for every seed, so the check is the same sweep that found the stall: run spec --match "IR Optimizer" over a range of pinned seeds and require that none of them exceeds a timeout generous against the 0.35 s a full run costs.

$ cabal build test:spec
$ timeout 60 $(cabal list-bin spec) --match "IR Optimizer" --seed 109 ; echo "exit=$?"

Prints the group up to blanking an unused shadowing binder keeps outer references bound and then hangs; exit=124. Seeds 152 and 478 behave the same way. Any other seed in 1..500 completes in about a third of a second. Reproduced on main at d79d95f.

Prerequisites / Relations

Independent — nothing needs to land first.

#345 was a different intermittent red in the same group: freshenBinders renamed a free reference that shared a Let binder's name, which surfaced as inlines expressions referenced once failing an alpha-equivalence check. That is fixed (#347). These three seeds hang identically before and after that fix — the same seed set, {109, 152, 478}, on both builds — so nothing about it is shared.

There is also a structural reason the two cannot be the same bug. optimizedUberModule begins with the uniquify pass:

  settlePhase =
    [ -- The entry pass (issue #139): establishes the global-uniqueness
      -- condition (GUC = 'UniqueBinders') that every
      -- following pass requires and preserves.
      RunPass uniquifyPass
    , RunFixpoint "optimize+dce" (optimizePass :| [dcePass])
    , …

so every expression this property optimizes has globally unique binders, the discipline under which the #345 shape cannot arise. The sibling property that did catch #345 calls optimizedExpression on deliberately non-uniquified terms instead.

Acceptance criteria

• spec --match "IR Optimizer" --seed 109 terminates, and likewise for seeds 152 and 478.
• Whatever term drives the non-termination is captured as an example-based regression test, so the fix is pinned by something that does not depend on a generator draw.
• If the cause is a non-converging rewrite pair, the fixpoint reports a diagnosable failure (naming the passes that keep firing) rather than spinning silently.