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