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

@@ -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]

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