purescript-lua · Unisay · Jul 29, 2026 · Jul 29, 2026 · Jul 29, 2026
diff --git a/changelog.d/20260729_150000_unisay_bound_nested_rewrites.md b/changelog.d/20260729_150000_unisay_bound_nested_rewrites.md
@@ -0,0 +1,34 @@
+### Fixed
+
+- The bottom-up IR rewrite driver — the traversal that rewrites a node's
+  children before the node and then re-applies the rules to their own result
+  until none fires — no longer loops forever on an expression that has no
+  normal form (#348). The re-application loop was unbounded, so beta reduction
+  spun on the self-application `Ω = (λx. x x) (λy. y y)`, whose every reduction
+  step reproduces it modulo binder names:
+
+  ```
+  AppN (AbsN [x$400] (AppN x$400 [x$400])) [AbsN [x$401] (AppN x$401 [x$401])]
+  AppN (AbsN [x$401] (AppN x$401 [x$401])) [AbsN [x$402] (AppN x$402 [x$402])]
+  AppN (AbsN [x$402] (AppN x$402 [x$402])) [AbsN [x$403] (AppN x$403 [x$403])]
+  ```
+
+  The loop now stops after `maxNestedRewrites` (100) nested rewrites along one
+  path and returns the term it has reached, the same treatment the pass-level
+  fixpoint already gave its own iteration cap: every rewrite preserves
+  semantics and the IR invariants on its own, so abandoning a redex
+  mid-reduction costs optimization and nothing else, and the driver's
+  `Rewritten` flag stays precise. With the pipeline's invariant checking on
+  (`--lint-ir`, and the test suite) the residual redex surfaces as
+  `FixpointDivergence "optimize+dce"` rather than as silence.
+
+  Emitted code is unchanged and the whole golden corpus stays byte-identical:
+  PureScript's type system rejects every term without a normal form, so no
+  compiled program contains one, and a converging rule chain needs a handful of
+  nested rewrites — the whole test suite, the ~300-deep golden constant chains
+  included, peaks at five, twenty times clear of the bound. What the bug did
+  cost was a test suite that hung rather than reddened, because the property
+  `IR Optimizer / optimization keeps expressions well-scoped` feeds the
+  optimizer generated untyped terms and drew `Ω` at 3 of the first 500 hspec
+  seeds (109, 152 and 478), each of which now finishes the group in about five
+  seconds.
diff --git a/lib/Language/PureScript/Backend/IR/Types.hs b/lib/Language/PureScript/Backend/IR/Types.hs
@@ -8,8 +8,8 @@ import Control.Lens
   , foldMapOf
   , makePrisms
   , prism'
-  , rewriteMOf
   , toListOf
+  , transformMOf
   , traverseOf
   )
 import Control.Monad.Writer.CPS (runWriterT, tell)
@@ -850,20 +850,49 @@ thenRewrite rewrite1 rewrite2 e =
     Just e' → Just . fromMaybe e' <$> rewrite2 e'
     Nothing → rewrite2 e
 
+{- | Backstop for the re-application loop of 'rewriteExpBottomUpM': how
+many nested rewrites one path down the expression may take before the
+driver stops re-applying the rule and returns the term it has reached.
+
+The bound is what makes the driver total, because beta reduction has no
+terminating strategy on an arbitrary untyped term: Ω = @(λx. x x) (λy. y
+y)@ reduces to itself modulo binder names, so the loop would re-apply
+forever. The IR is assumed well-typed (Note [IR is assumed well-typed])
+and PureScript's type system rejects every such term, so only the
+untyped terms the property-test generators draw reach the bound.
+
+Stopping early costs optimization and nothing else: each rewrite
+preserves semantics and the IR invariants on its own, so a term the
+driver abandons mid-reduction is as valid as a fully reduced one, and
+'WasRewritten' stays precise (it reports 'Rewritten' iff a rule fired,
+whether or not the loop ran to exhaustion). A converging rule chain
+needs a handful of nested rewrites — the whole test suite, the ~300-deep
+golden constant chains included, peaks at five — so the bound sits two
+orders of magnitude clear of legitimate work.
+-}
+maxNestedRewrites ∷ Natural
+maxNestedRewrites = 100
+
 {- | Rewrite bottom-up: every node's children are fully rewritten before
 the rule sees the node, and the rule is re-applied to its own result
-until it no longer fires ('rewriteMOf' semantics). One pass is
-therefore complete and idempotent — the result contains no node the
-rule still fires on — which is what makes the returned 'WasRewritten'
-precise, and what closes the Recurse-escape bug class (issue #149)
-structurally: a node exposed by a collapsing parent has already been
-fully rewritten.
+until it no longer fires, bounded by 'maxNestedRewrites'. Short of that
+bound one pass is complete and idempotent — the result contains no node
+the rule still fires on — which closes the Recurse-escape bug class
+(issue #149) structurally: a node exposed by a collapsing parent has
+already been fully rewritten.
 -}
 rewriteExpBottomUpM
   ∷ Monad m ⇒ RewriteRuleM m ann → RawExp ann → m (RawExp ann, WasRewritten)
-rewriteExpBottomUpM rule expr =
-  runWriterT $ flip (rewriteMOf subexpressions) expr \e →
-    lift (rule e) >>= traverse \e' → e' <$ tell Rewritten
+rewriteExpBottomUpM rule = runWriterT . reapply maxNestedRewrites
+ where
+  reapply budget = transformMOf subexpressions \e →
+    lift (rule e) >>= \case
+      Nothing → pure e
+      Just e' → do
+        tell Rewritten
+        case budget of
+          0 → pure e'
+          _ → reapply (budget - 1) e'
 
 -- | Pure 'rewriteExpBottomUpM'.
 rewriteExpBottomUp ∷ RewriteRule ann → RawExp ann → (RawExp ann, WasRewritten)

diff --git a/test/Language/PureScript/Backend/IR/Optimizer/Spec.hs b/test/Language/PureScript/Backend/IR/Optimizer/Spec.hs
@@ -43,6 +43,10 @@ import Language.PureScript.Backend.IR.Optimizer
   , shareForeignAccessors
   , sinkProjectionIntoLet
   )
+import Language.PureScript.Backend.IR.Pass
+  ( PassCheckFailure (FixpointDivergence)
+  , maxFixpointIterations
+  )
 import Language.PureScript.Backend.IR.Supply (runSupply)
 import Language.PureScript.Backend.IR.Types
   ( AlgebraicType (ProductType, SumType)
@@ -4015,6 +4019,41 @@ spec = describe "IR Optimizer" do
       annotateShow original
       optimizedUberModule mempty original === expected
 
+  -- Issue #348: Ω = (λx. x x) (λy. y y) is the smallest untyped term with
+  -- no normal form — every beta step reproduces it modulo binder names —
+  -- so the bottom-up driver's "re-apply the rule at this node until it
+  -- stops firing" loop must be bounded ('maxNestedRewrites'). PureScript's
+  -- type system rejects Ω, so no compiled program contains one; the
+  -- generator behind the properties below draws untyped terms and does.
+  describe "terminates on a term with no normal form (#348)" do
+    let selfApplication name =
+          abstraction (paramNamed name) $
+            application (refLocal name) (refLocal name)
+        omega =
+          application
+            (selfApplication (Name "x"))
+            (selfApplication (Name "y"))
+        original =
+          Linker.UberModule
+            { uberModuleForeigns = []
+            , uberModuleBindings = []
+            , uberModuleExports = [(Name "omega", omega)]
+            }
+
+    test "the pipeline gives up on a diverging redex" do
+      let optimized = optimizedUberModule mempty original
+      annotateShow optimized
+      -- Reaching an assertion at all is what this pins: the pipeline
+      -- returned rather than spinning. Abandoning a redex mid-reduction
+      -- leaves the term un-normalized but breaks no invariant, because
+      -- every step taken so far was semantics- and invariant-preserving.
+      lintWellScoped optimized === []
+      lintUniqueBinders optimized === []
+
+    test "the checked pipeline names the fixpoint that keeps firing" do
+      optimizedUberModuleChecked mempty original
+        === Left (FixpointDivergence "optimize+dce" maxFixpointIterations)
+
   describe "scoping invariants" do
     -- Mimics issue #37: an inlined binding contains a let with a
     -- reference bound by an earlier sibling; inlining it under a binder