From fe77e4d2d19500e361b3a2f3a07f1eee7511d674 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Wed, 15 Apr 2026 19:50:31 +0100
Subject: [PATCH] fix: `coinductive` syntax causing panic in macro scopes
 (#13420)

This PR fixes a panic when `coinductive` predicates are defined inside
macro scopes where constructor names carry macro scopes. The existing
guard only checked the declaration name for macro scopes, missing the
case where constructor identifiers are generated inside a macro
quotation and thus carry macro scopes. This caused
`removeFunctorPostfixInCtor` to panic on `Name.num` components from
macro scope encoding.

Closes #13415
---
 src/Lean/Elab/Inductive.lean |  2 ++
 tests/elab/13415.lean        | 13 +++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 tests/elab/13415.lean

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 28a282d91e..5a23a3f860 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -73,6 +73,8 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
         throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
       checkValidCtorModifier ctorModifiers
       let ctorName := ctor.getIdAt 3
+      if ctorName.hasMacroScopes && isCoinductive then
+        throwError "Coinductive predicates are not allowed inside of macro scopes"
       let ctorName := declName ++ ctorName
       let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
       let (binders, type?) := expandOptDeclSig ctor[4]
diff --git a/tests/elab/13415.lean b/tests/elab/13415.lean
new file mode 100644
index 0000000000..b7c43def5a
--- /dev/null
+++ b/tests/elab/13415.lean
@@ -0,0 +1,13 @@
+macro "co " x:ident : command => do
+  `(coinductive $x : Prop where | ok)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co f
+
+macro "co2" : command => do
+  `(coinductive test : Prop where | ctor)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co2