chore: remove repeat/while macro_rules bootstrap from Init.While

This PR removes the transitional `macro_rules` for `repeat`, `while`, and
`repeat ... until` from `Init.While`. After the latest stage0 update, the
`@[builtin_macro]` and `@[builtin_doElem_elab]` definitions in
`Lean.Elab.BuiltinDo.Repeat` are picked up directly, so the bootstrap
duplicates in `Init.While` are no longer needed. `Init.While` now only
provides the `Loop` type and its `ForIn` instance.

This PR also adjusts `repeat`'s `ControlInfo` to match `for ... in`:
its `numRegularExits` is now unconditionally `1` rather than
`if info.breaks then 1 else 0`. Reporting `0` when the body has no
`break` made callers treat the continuation as dead code, which broke
common patterns where the continuation has a non-`Unit` result type
(see discussion on #13437).

src/Init/While.lean

@@ -13,10 +13,11 @@ public section
 namespace Lean
 
 /-!
-# `while` and `repeat` loop support
+# `Loop` type backing `repeat`/`while`/`repeat ... until`
 
-The parsers for `repeat`, `while`, and `repeat ... until` are
-`@[builtin_doElem_parser]` definitions in `Lean.Parser.Do`.
+The parsers and elaborators for `repeat`, `while`, and `repeat ... until` live in
+`Lean.Parser.Do` and `Lean.Elab.BuiltinDo.Repeat`. This module only provides the
+`Loop` type (and `ForIn` instance) that those elaborators expand to.
 -/
 
 inductive Loop where
@@ -33,23 +34,4 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
--- The canonical parsers for `repeat`/`while`/`repeat ... until` live in `Lean.Parser.Do`
--- as `@[builtin_doElem_parser]` definitions. We register the expansion macros here so
--- they are available to `prelude` files in `Init`, which do not import `Lean.Elab`.
-
-macro_rules
-  | `(doElem| repeat%$tk $seq) => `(doElem| for%$tk _ in Loop.mk do $seq)
-
-macro_rules
-  | `(doElem| while%$tk $h : $cond do $seq) =>
-    `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
-
-macro_rules
-  | `(doElem| while%$tk $cond do $seq) =>
-    `(doElem| repeat%$tk if $cond then $seq else break)
-
-macro_rules
-  | `(doElem| repeat%$tk $seq until $cond) =>
-    `(doElem| repeat%$tk do $seq:doSeq; if $cond then break)
-
 end Lean

src/Lean/Elab/Do/InferControlInfo.lean

@@ -139,8 +139,14 @@ 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 := if info.breaks then 1 else 0,
+      numRegularExits := 1,
       continues := false,
       breaks := false
     }

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 new builtin `repeat`/`while` elaborators
 
     // 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/newdo.lean

@@ -489,4 +489,18 @@ example : IO Bool := do
   for (x, y) in ([] : List (Nat × Nat)) do count := count + 1
   return Float.abs count > 0
 
+-- A `repeat` (without `break`) followed by an early `return` inside an enclosing `for`. The for
+-- elaborator computes the loop body's `ControlInfo` via `inferControlInfoSeq`, which stops
+-- aggregating once it encounters an element with `numRegularExits := 0`. If `repeat` reported
+-- `numRegularExits := 0` for break-less bodies, the trailing `return 2` would be skipped during
+-- inference and the for elaborator would later throw "Early returning ... but the info said there
+-- is no early return". This test pins down that `repeat` reports `numRegularExits := 1`, matching
+-- `for ... in`.
+example : IO Nat := do
+  for _ in [1, 2] do
+    repeat
+      pure ()
+    return 2
+  return 1
+
 end Repros