feat: inject unreachable! after break-less repeat to unblock dead-code warnings

When a `repeat` body has no `break`, the loop does not terminate
normally and the `ForIn.forIn` result type is fixed to `PUnit`. Using
such a `repeat` in a do block that expects a non-`Unit` result type
used to require a trailing `return`/`unreachable!` from the user. To
make matters worse, that trailing element was flagged as dead by the
`ControlInfo`-based warning, yet removing it broke the do block's
type, so the warning was not actionable and had to be suppressed.

This PR teaches `elabDoRepeat` to append its own `unreachable!` after
the `for _ in Loop.mk do ...` expansion when the body cannot `break`.
The `unreachable!` gives the continuation a polymorphic value, so the
enclosing do block's result type is inferred from context and the
user no longer needs to write any trailing filler. The
`ControlInfo` for break-less `repeat` now reports `noFallthrough`
(and `numRegularExits := 0`) honestly, so dead-code warnings fire on
any user-written element after the loop — and because the loop
supplies its own `unreachable!`, those warnings are actionable: the
user can simply delete the flagged element.

Co-authored-by: Rob23oba <robin.arnez@web.de>

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -19,13 +19,19 @@ open Lean.Parser.Term
 /--
 Builtin do-element elaborator for `repeat` (syntax kind `Lean.Parser.Term.doRepeat`).
 
-Expands to `for _ in Loop.mk do ...`. A follow-up change will extend this
-elaborator to choose between `Loop.mk` and a well-founded `Repeat.mk` based on a
-configuration option.
+Expands to `for _ in Loop.mk do ...`. When the body cannot `break`, the loop's own expression
+type is fixed to `PUnit`, yet the surrounding do block may require a different result type;
+we append an `unreachable!` so the continuation has a polymorphic value of any type. The
+`unreachable!` is never actually executed (the loop never terminates normally), and any
+dead-code warning that fires on the surrounding continuation is actionable — the user can
+remove the following code without breaking the do block's type.
 -/
 @[builtin_doElem_elab Lean.Parser.Term.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
   let `(doElem| repeat%$tk $seq) := stx | throwUnsupportedSyntax
-  let expanded ← `(doElem| for%$tk _ in Loop.mk do $seq)
+  let mut expanded ← `(doElem| for%$tk _ in Loop.mk do $seq)
+  let info ← inferControlInfoSeq seq
+  if !info.breaks then
+    expanded ← `(doElem| do $expanded:doElem; unreachable!)
   Term.withMacroExpansion stx expanded <|
     withRef expanded <| elabDoElem ⟨expanded⟩ dec
 

src/Lean/Elab/Do/InferControlInfo.lean

@@ -165,8 +165,7 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
   | `(doElem| unless $_ do $elseSeq) =>
     ControlInfo.alternative {} <$> ofSeq elseSeq
   -- For/Repeat
-  | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq)
-  | `(doRepeat| repeat $bodySeq) =>
+  | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and earlyReturn
       numRegularExits := 1,
@@ -174,6 +173,17 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
       breaks := false,
       noFallthrough := false,
     }
+  | `(doRepeat| repeat $bodySeq) =>
+    -- A break-less `repeat` never falls through; the elaborator injects an `unreachable!` so the
+    -- surrounding continuation still has a polymorphic value to hand back, and any dead-code
+    -- warning on subsequent elements is actionable.
+    let info ← ofSeq bodySeq
+    return { info with  -- keep only reassigns and earlyReturn
+      numRegularExits := if info.breaks then 1 else 0,
+      continues := false,
+      breaks := false,
+      noFallthrough := !info.breaks,
+    }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>
     let mut info ← ofSeq trySeq

tests/elab/doControlInfoAggregate.lean

@@ -69,8 +69,12 @@ example : IO Nat := do
     return 42
   return 1
 
--- The `return 2` is required to give the do block its `Id Nat` result type; no dead-code warning
--- should fire on it.
+-- Neither branch of the `if` can terminate normally, so the dead-code warning fires on
+-- `return 2`. The user can act on the warning: removing `return 2` still leaves the do block
+-- well-typed because `elabDoRepeat` injects an `unreachable!` into each branch's expansion.
+/--
+warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
+-/
 #guard_msgs in
 example (x : Nat) : Id Nat := do
   if x = 3 then
@@ -80,3 +84,14 @@ example (x : Nat) : Id Nat := do
     repeat
       pure ()
   return 2
+
+-- Same as above without the trailing `return 2`: the `unreachable!` that `elabDoRepeat` injects
+-- into each branch gives the do block its `Id Nat` result type.
+#guard_msgs in
+example (x : Nat) : Id Nat := do
+  if x = 3 then
+    repeat
+      pure ()
+  else
+    repeat
+      pure ()