chore: add ControlInfo handler for doRepeat

This PR names the `repeat` syntax (`doRepeat`) and installs dedicated
elaborators for it in both the legacy and new do-elaborators. Both
currently expand to `for _ in Loop.mk do ...`, identical to the existing
fallback macro in `Init.While`.

The elaborators are dead code today because that fallback macro fires
first. A follow-up PR will drop the macro (after this PR's stage0 update
lands) and extend `elabDoRepeat` to choose between `Loop.mk` and a
well-founded `Repeat.mk` based on a `backward.do.while` option.

src/Init/Data/Order/LemmasExtra.lean

@@ -87,7 +87,7 @@ public theorem IsLinearOrder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderO
 /--
 This lemma derives a `LawfulOrderLT α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
     (lt_iff_compare_eq_lt : ∀ a b : α, a < b ↔ compare a b = .lt) :
     LawfulOrderLT α where
   lt_iff a b := by
@@ -96,7 +96,7 @@ public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [Law
 /--
 This lemma derives a `LawfulOrderBEq α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
     (beq_iff_compare_eq_eq : ∀ a b : α, a == b ↔ compare a b = .eq) :
     LawfulOrderBEq α where
   beq_iff_le_and_ge := by
@@ -105,7 +105,7 @@ public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderInf α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE) :
     LawfulOrderInf α where
@@ -114,7 +114,7 @@ public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderMin α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
@@ -125,7 +125,7 @@ public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderSup α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE) :
     LawfulOrderSup α where
@@ -134,7 +134,7 @@ public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderMax α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :

src/Init/While.lean

@@ -32,7 +32,7 @@ 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
 
-syntax "repeat " doSeq : doElem
+syntax (name := doRepeat) "repeat " doSeq : doElem
 
 macro_rules
   | `(doElem| repeat%$tk $seq) => `(doElem| for%$tk _ in Loop.mk do $seq)

src/Lean/Elab/BuiltinDo.lean

@@ -15,3 +15,4 @@ public import Lean.Elab.BuiltinDo.Jump
 public import Lean.Elab.BuiltinDo.Misc
 public import Lean.Elab.BuiltinDo.For
 public import Lean.Elab.BuiltinDo.TryCatch
+public import Lean.Elab.BuiltinDo.Repeat

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Lean.Elab.BuiltinDo.Basic
+meta import Lean.Parser.Do
+import Lean.Elab.BuiltinDo.For
+
+public section
+
+namespace Lean.Elab.Do
+
+open Lean.Parser.Term
+
+/--
+Builtin do-element elaborator for `repeat` (syntax kind `Lean.doRepeat`).
+
+Expands to `for _ in Loop.mk do ...`. A follow-up PR will drop the fallback macro
+in `Init.While` (which currently preempts this elaborator) and extend this
+elaborator to choose between `Loop.mk` and a well-founded `Repeat.mk` based on a
+configuration option.
+-/
+@[builtin_doElem_elab Lean.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
+  let `(doElem| repeat $seq) := stx | throwUnsupportedSyntax
+  let expanded ← `(doElem| for _ in Loop.mk do $seq)
+  Term.withMacroExpansion stx expanded <|
+    withRef expanded <| elabDoElem ⟨expanded⟩ dec
+
+end Lean.Elab.Do

src/Lean/Elab/Do/InferControlInfo.lean

@@ -129,6 +129,7 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return thenInfo.alternative info
   | `(doElem| unless $_ do $elseSeq) =>
     ControlInfo.alternative {} <$> ofSeq elseSeq
+  -- For/Repeat
   | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and earlyReturn
@@ -136,6 +137,13 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
       continues := false,
       breaks := false
     }
+  | `(doRepeat| repeat $bodySeq) =>
+    let info ← ofSeq bodySeq
+    return { info with
+      numRegularExits := if info.breaks then 1 else 0,
+      continues := false,
+      breaks := false
+    }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>
     let mut info ← ofSeq trySeq

src/Lean/Elab/Do/Legacy.lean

@@ -1782,6 +1782,10 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
+          else if k == `Lean.doRepeat then
+            let seq := doElem[1]
+            let expanded ← `(doElem| for _ in Loop.mk do $seq)
+            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Meta/Instances.lean

@@ -229,8 +229,33 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
 
   return synthed
 
+def checkImpossibleInstance (c : Expr) : MetaM Unit := do
+  let cTy ← inferType c
+  forallTelescopeReducing cTy fun args ty => do
+    let argTys ← args.mapM inferType
+    let impossibleArgs ← args.zipIdx.filterMapM fun (arg, i) => do
+      let fv := arg.fvarId!
+      if (← fv.getDecl).binderInfo.isInstImplicit then return none
+      if ty.containsFVar fv then return none
+      if argTys[i+1:].any (·.containsFVar fv) then return none
+      return some m!"{arg} : {← inferType arg}"
+    if impossibleArgs.isEmpty then return
+    let impossibleArgs := MessageData.joinSep impossibleArgs.toList ", "
+    throwError m!"Instance {c} has arguments "
+      ++ impossibleArgs
+      ++ " that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type."
+
+def checkNonClassInstance (declName : Name) (c : Expr) : MetaM Unit := do
+  let type ← inferType c
+  forallTelescopeReducing type fun _ target => do
+    unless (← isClass? target).isSome do
+      unless target.isSorry do
+      throwError m!"instance `{declName}` target `{target}` is not a type class."
+
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let c ← mkConstWithLevelParams declName
+  checkImpossibleInstance c
+  checkNonClassInstance declName c
   let keys ← mkInstanceKey c
   let status ← getReducibilityStatus declName
   unless status matches .reducible | .implicitReducible do

src/Std/Data/DHashMap/RawDecidableEquiv.lean

@@ -18,7 +18,7 @@ open Std.DHashMap.Internal
 
 namespace Std.DHashMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   Raw₀.decidableEquiv ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ h₁ h₂
 
 end Std.DHashMap.Raw

src/Std/Data/DTreeMap/Raw/DecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DTreeMap.Internal.Impl
 
 namespace Std.DTreeMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := decidableEquiv t₁.1 t₂.1 h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/HashMap/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DHashMap.Raw
 
 namespace Std.HashMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := DHashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/HashSet/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.HashMap.Raw
 
 namespace Std.HashSet.Raw
 
-instance instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := HashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/TreeMap/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.DTreeMap.Raw
 
 namespace Std.TreeMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := DTreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/TreeSet/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.TreeMap.Raw
 
 namespace Std.TreeSet.Raw
 
-instance instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := TreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

stage0/src/stdlib_flags.h

@@ -1,5 +1,6 @@
 #include "util/options.h"
 
+// bump for ControlInfo handler
 namespace lean {
 options get_default_options() {
     options opts;