From eb15c08ea0efc3a30cb8f32dca20cc115ffd854d Mon Sep 17 00:00:00 2001
From: Arthur Adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Fri, 16 Aug 2024 17:19:48 +0200
Subject: [PATCH] fix: instantiate mvars of indices before instantiating fvars
 (#4717)

When elaborating the headers of mutual indexed inductive types, mvars
have to be synthesized and instantiated before replacing the fvars
present there. Otherwise, some fvars present in uninstantiated mvars may
be missed and lead to an error later.
Closes #3242 (again)
---
 src/Lean/Elab/Inductive.lean | 13 +++++++++++--
 tests/lean/run/3242.lean     |  8 ++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index ced5fb2fbf5b..1fe81c39b40d 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -771,6 +771,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
   let isUnsafe          := view0.modifiers.isUnsafe
   withRef view0.ref <| Term.withLevelNames allUserLevelNames do
     let rs ← elabHeader views
+    Term.synthesizeSyntheticMVarsNoPostponing
     withInductiveLocalDecls rs fun params indFVars => do
       trace[Elab.inductive] "indFVars: {indFVars}"
       let mut indTypesArray := #[]
@@ -778,11 +779,19 @@ 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
+        /- At this point, because of `withInductiveLocalDecls`, the only fvars that are in context are the ones related to the first inductive type.
+           Because of this, we need to replace the fvars present in each inductive type's header of the mutual block with those of the first inductive.
+           However, some mvars may still be uninstantiated there, and might hide some of the old fvars.
+           As such we first need to synthesize all possible mvars at this stage, instantiate them in the header types and only
+           then replace the parameters' fvars in the header type.
+
+           See issue #3242 (`https://github.com/leanprover/lean4/issues/3242`)
+        -/
+        let type  ←  instantiateMVars r.type
+        let type  := type.replaceFVars r.params 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
       let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars
       trace[Elab.inductive] "numExplicitParams: {numExplicitParams}"
       let indTypes := indTypesArray.toList
diff --git a/tests/lean/run/3242.lean b/tests/lean/run/3242.lean
index c9ce4f9e1dee..b1dac6403890 100644
--- a/tests/lean/run/3242.lean
+++ b/tests/lean/run/3242.lean
@@ -11,3 +11,11 @@ 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