fix: constructor elaboration

fixes #1098

src/Lean/Elab/Inductive.lean

@@ -88,6 +88,7 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
           let indices ← Term.addAutoBoundImplicits #[]
           return (← mkForallFVars indices type, indices.size)
         Term.addAutoBoundImplicits' params type fun params type => do
+          trace[Elab.inductive] "header params: {params}, type: {type}"
           pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
     elabHeaderAux views (i+1) acc
   else
@@ -289,6 +290,7 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
             k <| mkAppN indFVar params
           | some ctorType =>
             let type ← Term.elabType ctorType
+            trace[Elab.inductive] "elabType {ctorView.declName} : {type} "
             Term.synthesizeSyntheticMVars (mayPostpone := true)
             let type ← instantiateMVars type
             let type ← checkParamOccs type
@@ -301,11 +303,18 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
         elabCtorType fun type => do
           Term.synthesizeSyntheticMVarsNoPostponing
           let ctorParams ← Term.addAutoBoundImplicits ctorParams
-          let type  ← mkForallFVars ctorParams type
-          let extraCtorParams ← Term.collectUnassignedMVars type
-          let type ← mkForallFVars extraCtorParams type
+          let except (mvarId : MVarId) := ctorParams.any fun ctorParam => ctorParam.isMVar && ctorParam.mvarId! == mvarId
+          let mut extraCtorParams := #[]
+          for ctorParam in ctorParams do
+            extraCtorParams ← Term.collectUnassignedMVars (← instantiateMVars (← inferType ctorParam)) extraCtorParams except
+          extraCtorParams ← Term.collectUnassignedMVars (← instantiateMVars type) extraCtorParams except
+          trace[Elab.inductive] "extraCtorParams: {extraCtorParams}"
+          /- We must abstract `extraCtorParams` and `ctorParams` simultaneously to make
+             sure we do not create auxiliary metavariables. -/
+          let type  ← mkForallFVars (extraCtorParams ++ ctorParams) type
           let type ← reorderCtorArgs type
           let type ← mkForallFVars params type
+          trace[Elab.inductive] "{ctorView.declName} : {type} "
           return { name := ctorView.declName, type }
 where
   checkParamOccs (ctorType : Expr) : MetaM Expr :=

src/Lean/Elab/Term.lean

@@ -1354,9 +1354,10 @@ def withoutAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
   withReader (fun ctx => { ctx with autoBoundImplicit := false, autoBoundImplicits := {} }) k
 
 /--
-  Collect unassigned metavariables in `type` that are not already in `init`.
+  Collect unassigned metavariables in `type` that are not already in `init` and not satisfying `except`.
 -/
-partial def collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) : TermElabM (Array Expr) := do
+partial def collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) (except : MVarId → Bool := fun _ => false)
+    : TermElabM (Array Expr) := do
   let mvarIds ← getMVars type
   if mvarIds.isEmpty then
     return init
@@ -1369,7 +1370,7 @@ where
     | mvarId :: mvarIds => do
       if (← isExprMVarAssigned mvarId) then
         go mvarIds result
-      else if result.contains (mkMVar mvarId) then
+      else if result.contains (mkMVar mvarId) || except mvarId then
         go mvarIds result
       else
         let mvarType := (← getMVarDecl mvarId).type

tests/lean/1098.lean

@@ -0,0 +1,23 @@
+structure FoldImpl (α β : Type u) where
+  γ   : Type u
+  x₀  : γ
+  f   : γ → α → γ
+  out : γ → β
+
+inductive R : FoldImpl α β → FoldImpl α β → Prop where
+  | intro {γ γ' x₀ y₀ f g out out'} : R ⟨γ, x₀, f, out⟩ ⟨γ', y₀, g, out'⟩
+
+#print R
+
+#check @R.intro
+-- @R.intro : ∀ {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β},
+--   R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' }
+
+namespace Ex2
+
+inductive R : FoldImpl α β → FoldImpl α β → Prop where
+  | intro : R ⟨γ, x₀, f, out⟩ ⟨γ', y₀, g, out'⟩
+
+#print R
+
+end Ex2

tests/lean/1098.lean.expected.out

@@ -0,0 +1,12 @@
+inductive R.{u_1} : {α β : Type u_1} → FoldImpl α β → FoldImpl α β → Prop
+number of parameters: 2
+constructors:
+R.intro : ∀ {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β},
+  R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' }
+@R.intro : ∀ {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β},
+  R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' }
+inductive Ex2.R.{u_1} : {α β : Type u_1} → FoldImpl α β → FoldImpl α β → Prop
+number of parameters: 2
+constructors:
+Ex2.R.intro : ∀ {α β γ : Type u_1} {x₀ : γ} {f : γ → α → γ} {out : γ → β} {γ' : Type u_1} {y₀ : γ'} {g : γ' → α → γ'}
+  {out' : γ' → β}, R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' }