From 0c92d177921b804783cc594d04a488fc0be6d21f Mon Sep 17 00:00:00 2001
From: Arthur Adjedj <arthur.adjedj@gmail.com>
Date: Sat, 17 Feb 2024 17:52:28 +0100
Subject: [PATCH] fix: instantiate the types of inductives with the right
 parameters (#3246)

Closes #3242
---
 src/Lean/Elab/Inductive.lean |  5 +++--
 tests/lean/run/3242.lean     | 13 +++++++++++++
 2 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/3242.lean

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index ef27cf7eb6aa..d377da2c3b00 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -756,8 +756,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
       for i in [:views.size] do
         let indFVar := indFVars[i]!
         Term.addLocalVarInfo views[i]!.declId indFVar
-        let r       := rs[i]!
-        let type  ← mkForallFVars params r.type
+        let r     := rs[i]!
+        let type  := r.type |>.abstract r.params |>.instantiateRev params
+        let type  ← mkForallFVars params type
         let ctors ← withExplicitToImplicit params (elabCtors indFVars indFVar params r)
         indTypesArray := indTypesArray.push { name := r.view.declName, type, ctors }
       Term.synthesizeSyntheticMVarsNoPostponing
diff --git a/tests/lean/run/3242.lean b/tests/lean/run/3242.lean
new file mode 100644
index 000000000000..c9ce4f9e1dee
--- /dev/null
+++ b/tests/lean/run/3242.lean
@@ -0,0 +1,13 @@
+mutual
+inductive A (α : Type) : α → Type where
+
+inductive B (α : Type) : α → Type where
+end
+
+mutual
+inductive R (F: α → α → Prop) (a : α) : α → Prop where
+  | ind : ∀ (f: Nat → α) b, (∀ n, And₂ F a b f n) → R F a b
+
+inductive And₂ (F: α → α → Prop) (a : α) : α → (Nat → α) → Nat → Prop where
+  | mk (b : α) (f : Nat → α) (n : Nat): R F a (f n) → F (f n) b → And₂ F a b f n
+end