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

@@ -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

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.

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