From a3cb98bb273d30a09887b1f26c93ea8ab0fc4de9 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 20 Apr 2026 23:13:59 +0200 Subject: [PATCH] fix: aggregate `ControlInfo` past `numRegularExits == 0` elements (#13486) This PR fixes `inferControlInfoSeq` and `ControlInfo.sequence` to keep aggregating `breaks`/`continues`/`returnsEarly`/`reassigns` past elements whose `ControlInfo` reports `numRegularExits := 0`. Previously the analysis short-circuited at such elements, so any trailing `return`/`break`/`continue` was missing from the inferred info. The elaboration framework only skips subsequent doElems syntactically for top-level `return`/`break`/`continue`; for every other `numRegularExits == 0` case (e.g. a `match`/`if`/`try` whose branches all terminate, or a `repeat` without `break`) the elaborator keeps visiting the continuation and the for/match elaborator then tripped its invariant check with `Early returning ... but the info said there is no early return`. With this change the inferred info matches what the elaborator actually sees, which also removes the need for the `numRegularExits := 1` workaround on `repeat` introduced in #13479. --- src/Lean/Elab/Do/InferControlInfo.lean | 28 +++-------- stage0/src/stdlib_flags.h | 1 + tests/elab/doControlInfoAggregate.lean | 67 ++++++++++++++++++++++++++ 3 files changed, 75 insertions(+), 21 deletions(-) create mode 100644 tests/elab/doControlInfoAggregate.lean diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean index e88fad048f..c0595b881f 100644 --- a/src/Lean/Elab/Do/InferControlInfo.lean +++ b/src/Lean/Elab/Do/InferControlInfo.lean @@ -35,12 +35,14 @@ structure ControlInfo where def ControlInfo.pure : ControlInfo := {} -def ControlInfo.sequence (a b : ControlInfo) : ControlInfo := - if a.numRegularExits == 0 then a else { +def ControlInfo.sequence (a b : ControlInfo) : ControlInfo := { breaks := a.breaks || b.breaks, continues := a.continues || b.continues, returnsEarly := a.returnsEarly || b.returnsEarly, - numRegularExits := b.numRegularExits, + -- Once `a` has no regular exits, `b` is statically unreachable, so no regular exit survives. + -- We still aggregate the other effects because the elaborator keeps visiting `b` unless it is + -- skipped via `elabAsSyntacticallyDeadCode`. + numRegularExits := if a.numRegularExits == 0 then 0 else b.numRegularExits, reassigns := a.reassigns ++ b.reassigns, } @@ -139,14 +141,8 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do } | `(doRepeat| repeat $bodySeq) => let info ← ofSeq bodySeq - -- Match `for ... in` and report `numRegularExits := 1` unconditionally. Reporting `0` when - -- the body has no `break` causes `ofSeq` (in any enclosing sequence whose `ControlInfo` is - -- inferred, e.g. a surrounding `for`/`if`/`match`/`try` body) to stop aggregating after this - -- element and miss any `return`/`break`/`continue` that follows. The corresponding elaborator - -- then sees the actual control flow disagree with the inferred info and throws errors like - -- "Early returning ... but the info said there is no early return". See #13437 for details. return { info with - numRegularExits := 1, + numRegularExits := if info.breaks then 1 else 0, continues := false, breaks := false } @@ -218,17 +214,7 @@ partial def ofLetOrReassign (reassigned : Array Ident) (rhs? : Option (TSyntax ` partial def ofSeq (stx : TSyntax ``doSeq) : TermElabM ControlInfo := do let mut info : ControlInfo := {} for elem in getDoElems stx do - if info.numRegularExits == 0 then - break - let elemInfo ← ofElem elem - info := { - info with - breaks := info.breaks || elemInfo.breaks - continues := info.continues || elemInfo.continues - returnsEarly := info.returnsEarly || elemInfo.returnsEarly - numRegularExits := elemInfo.numRegularExits - reassigns := info.reassigns ++ elemInfo.reassigns - } + info := info.sequence (← ofElem elem) return info partial def ofOptionSeq (stx? : Option (TSyntax ``doSeq)) : TermElabM ControlInfo := do diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..20ac9dcd4f 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -22,6 +22,7 @@ options get_default_options() { opts = opts.update({"quotPrecheck"}, true); opts = opts.update({"pp", "rawOnError"}, true); + // bump stage0 to pick up `ControlInfo.sequence` aggregating past `numRegularExits == 0` // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt. diff --git a/tests/elab/doControlInfoAggregate.lean b/tests/elab/doControlInfoAggregate.lean new file mode 100644 index 0000000000..0b3835851f --- /dev/null +++ b/tests/elab/doControlInfoAggregate.lean @@ -0,0 +1,67 @@ +set_option backward.do.legacy false + +-- When an inner doElem's `ControlInfo` has `numRegularExits := 0` (because all branches +-- `break`/`continue`/`return`, or it is a non-terminating `repeat`), the trailing `return` +-- inside the enclosing `for` body used to be dropped during inference, and the for elaborator +-- then threw "Early returning ... but the info said there is no early return" even though the +-- elaborator does visit the trailing element. `ofSeq`/`ControlInfo.sequence` now aggregate +-- `breaks`/`continues`/`returnsEarly`/`reassigns` past `numRegularExits == 0` elements, so the +-- inferred info matches what the elaborator actually sees. + +/-- +warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it. +-/ +#guard_msgs in +example (cond : Bool) : IO Nat := do + for _ in [1, 2] do + if cond then break else break + return 42 + return 1 + +/-- +warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it. +-/ +#guard_msgs in +example (cond : Bool) : IO Nat := do + for _ in [1, 2] do + if cond then continue else continue + return 42 + return 1 + +#guard_msgs in +example (i : Nat) : IO Nat := do + for _ in [1, 2] do + match i with + | 0 => break + | _ => break + return 42 + return 1 + +/-- +warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it. +-/ +#guard_msgs in +example : IO Nat := do + for _ in [1, 2] do + try break catch _ => break + return 42 + return 1 + +/-- +warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it. +-/ +#guard_msgs in +example (cond : Bool) : IO Nat := do + for _ in [1, 2] do + unless cond do break + if cond then break else break + return 42 + return 1 + +#guard_msgs in +example : IO Nat := do + for _ in [1, 2] do + repeat + pure () + return 42 + return 1