fix: instantiate the types of inductives with the right parameters

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

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