ITADN

vera compile never terminates on a self-referential refinement used in a signature (closure-lift queue feeds itself)

#1234Openaallan 创建于 22 天前
bug
A
aallancommented
Found during the #1213 burndown (PR #1232 round 7) — pre-existing, verified at the pre-round tree with a 90s timeout + faulthandler dump; NOT introduced by the burndown work. `type R = { @Int | ... fn(@R -> @Int) ... };` plus `fn f(@R -> @Int)` type-checks clean, then `vera compile`/`vera run` never finishes: each lifted closure's refined-formal guard lowers a predicate containing the same `AnonFn`, which queues another closure — `closures.py::_lift_pending_closures` / `_compile_lifted_closure` loop forever. Check-green program, no diagnostic, no bound. The #1232 pre-scan gained a cycle guard for the REGISTRATION walk (asserted both directions), so registration is immune — the lift loop itself is the residual. Fix direction: cycle detection keyed on the (closure, refinement) identity in the lift queue → loud E602-class skip naming the self-reference, mirroring the pre-scan's guard. Lands in the burndown (PR C, precision + lowering).
0 条评论