fix: instantiate mvars of indices before instantiating fvars

src/Lean/Elab/Inductive.lean

@@ -778,7 +778,8 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
         let indFVar := indFVars[i]!
         Term.addLocalVarInfo views[i]!.declId indFVar
         let r     := rs[i]!
-        let type  := r.type |>.abstract r.params |>.instantiateRev params
+        let type  ←  instantiateMVars r.type
+        let type  := 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 }

tests/lean/run/3242.lean

@@ -11,3 +11,12 @@ inductive R (F: α → α → Prop) (a : α) : α → Prop where
 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
+
+
+structure Salg (n k: Nat) where
+  D: Type
+
+mutual
+inductive Ins (salg: Salg n k) : salg.D → Prop
+inductive Out (salg: Salg n k) : salg.D → Prop
+end