feat: inject unreachable! after break-less repeat (#13506)

This PR appends `unreachable!` to the expansion of `break`-less `repeat`
when the expected result type does not unify with `PUnit`. The
continuation then has a polymorphic value, so the enclosing do block's
result type is inferred without a user-written filler, and `ControlInfo`
for break-less `repeat` can report `noFallthrough` honestly — dead-code
warnings on subsequent elements are now actionable.

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

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -19,13 +19,20 @@ 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
+    if !(← Meta.isDefEqGuarded dec.resultType (← mkPUnit)) 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,22 @@ example (x : Nat) : Id Nat := do
     repeat
       pure ()
   return 2
+
+-- A break-less `repeat` whose body early-returns: `elabDoRepeat` injects an `unreachable!`, so
+-- the do block's `Id Nat` result type is recovered from the body's `return`.
+#guard_msgs in
+example (n : Nat) : Id Nat := do
+  let mut i := 0
+  repeat
+    if i = n then return i
+    i := i + 1
+
+-- Break-less, return-less `repeat` inside an action whose result type is polymorphic. The loop
+-- body never terminates, so `elabDoRepeat` leaves the expansion as a plain `for _ in Loop.mk`
+-- and the inner do block types as `m PUnit`, letting `BaseIO.asTask`'s polymorphic `α` resolve
+-- to `PUnit`.
+#guard_msgs in
+example : BaseIO Unit := do
+  let _ ← BaseIO.asTask do
+    repeat
+      pure ()