From 87e6581e6bdb3c5db0588b721a1cb10731914358 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Apr 2022 18:19:06 -0700 Subject: [PATCH] fix: constructor elaboration fixes #1098 --- src/Lean/Elab/Inductive.lean | 15 ++++++++++++--- src/Lean/Elab/Term.lean | 7 ++++--- tests/lean/1098.lean | 23 +++++++++++++++++++++++ tests/lean/1098.lean.expected.out | 12 ++++++++++++ 4 files changed, 51 insertions(+), 6 deletions(-) create mode 100644 tests/lean/1098.lean create mode 100644 tests/lean/1098.lean.expected.out diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 37ae5dd701..af6cd068e9 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/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 := diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 1110e12c28..b191e3faf5 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/tests/lean/1098.lean b/tests/lean/1098.lean new file mode 100644 index 0000000000..c689743222 --- /dev/null +++ b/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 diff --git a/tests/lean/1098.lean.expected.out b/tests/lean/1098.lean.expected.out new file mode 100644 index 0000000000..85da7a2f4f --- /dev/null +++ b/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' }