From 0da281fab48d353e9da080d81dc7d736836f84b6 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 28 Feb 2023 11:15:57 -0800
Subject: [PATCH] fix: reject occurrences of inductive type in index

Fixes #2125
---
 src/kernel/inductive.cpp          | 14 ++++++++++++--
 tests/lean/2125.lean              |  9 +++++++++
 tests/lean/2125.lean.expected.out |  1 +
 3 files changed, 22 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/2125.lean
 create mode 100644 tests/lean/2125.lean.expected.out

diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp
index 1ce41d7d26..de61345659 100644
--- a/src/kernel/inductive.cpp
+++ b/src/kernel/inductive.cpp
@@ -330,8 +330,9 @@ public:
     }
 
     /** \brief Return true iff `t` is a term of the form `I As t`
-        where `I` is the inductive datatype at position `i` being declared and
-        `As` are the global parameters of this declaration. */
+        where `I` is the inductive datatype at position `i` being declared,
+        `As` are the global parameters of this declaration,
+        and `t` does not contain any inductive datatype being declared. */
     bool is_valid_ind_app(expr const & t, unsigned i) {
         buffer<expr> args;
         expr I = get_app_args(t, args);
@@ -341,6 +342,15 @@ public:
             if (m_params[i] != args[i])
                 return false;
         }
+        /*
+        Ensure that `t` does not contain the inductive datatype that is being declared.
+        Such occurrences are unsound in general. https://github.com/leanprover/lean4/issues/2125
+        We also used to reject them in Lean 3.
+        */
+        for (unsigned i = m_nparams; i < args.size(); i++) {
+            if (has_ind_occ(args[i]))
+                return false;
+        }
         return true;
     }
 
diff --git a/tests/lean/2125.lean b/tests/lean/2125.lean
new file mode 100644
index 0000000000..d8eb0d6e71
--- /dev/null
+++ b/tests/lean/2125.lean
@@ -0,0 +1,9 @@
+open Classical
+
+noncomputable def f (α : Type) : Bool :=
+  Nonempty α
+
+-- The following inductive is unsound:
+inductive C : Bool → Type
+  -- Must be rejected because `C` occurs inside an index.
+  | c : C (f (C false))
diff --git a/tests/lean/2125.lean.expected.out b/tests/lean/2125.lean.expected.out
new file mode 100644
index 0000000000..8b6d47e073
--- /dev/null
+++ b/tests/lean/2125.lean.expected.out
@@ -0,0 +1 @@
+2125.lean:7:0-9:23: error: (kernel) invalid return type for 'C.c'