From e07c59c8318374be324949527537e09a34e96b3d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 10 Apr 2025 17:19:53 -0700 Subject: [PATCH] fix: eliminate panic when `inductive` has autoparam parameter with underdetermined type (#7905) This PR fixes an issue introduced bug #6125 where an `inductive` or `structure` with an autoimplicit parameter with a type that has a metavariable would lead to a panic. Closes #7788. This was due to switching from `Term.addAutoBoundImplicits'` to `Term.addAutoBoundImplicits` and not properly handling metavariables in the parameters list. To fix this, now the inductive type headers record the abstracted type and the number of parameters, rather than record the parameters, the type, the local context, and the local instances. A benefit to this over `Term.addAutoBoundImplicits'` is that the type's parameters do not appear twice in the local context. --- src/Lean/Elab/MutualInductive.lean | 64 ++++++++----------------- src/Lean/Elab/Structure.lean | 8 +--- src/Lean/Elab/Term.lean | 9 ++-- tests/lean/run/7788.lean | 77 ++++++++++++++++++++++++++++++ 4 files changed, 104 insertions(+), 54 deletions(-) create mode 100644 tests/lean/run/7788.lean diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index fa71d64d79..a83c5c12d2 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -109,11 +109,11 @@ structure InductiveView where /-- Elaborated header for an inductive type before fvars for each inductive are added to the local context. -/ structure PreElabHeaderResult where view : InductiveView - lctx : LocalContext - localInsts : LocalInstances levelNames : List Name - params : Array Expr + numParams : Nat type : Expr + /-- The parameters in the header's initial local context. Used for adding fvar alias terminfo. -/ + origParams : Array Expr deriving Inhabited /-- The elaborated header with the `indFVar` registered for this inductive type. -/ @@ -228,16 +228,12 @@ private def checkClass (rs : Array PreElabHeaderResult) : TermElabM Unit := do throwErrorAt r.view.ref "invalid inductive type, mutual classes are not supported" private def checkNumParams (rs : Array PreElabHeaderResult) : TermElabM Nat := do - let numParams := rs[0]!.params.size + let numParams := rs[0]!.numParams for r in rs do - unless r.params.size == numParams do + unless r.numParams == numParams do throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes" return numParams -private def mkTypeFor (r : PreElabHeaderResult) : TermElabM Expr := do - withLCtx r.lctx r.localInsts do - mkForallFVars r.params r.type - /-- Execute `k` with updated binder information for `xs`. Any `x` that is explicit becomes implicit. -/ @@ -276,7 +272,7 @@ private def checkHeaders (rs : Array PreElabHeaderResult) (numParams : Nat) (i : checkHeaders rs numParams (i+1) type where checkHeader (r : PreElabHeaderResult) (numParams : Nat) (firstType? : Option Expr) : TermElabM Expr := do - let type ← mkTypeFor r + let type := r.type match firstType? with | none => return type | some firstType => @@ -306,7 +302,8 @@ private def elabHeadersAux (views : Array InductiveView) (i : Nat) (acc : Array let params ← Term.addAutoBoundImplicits params (view.declId.getTailPos? (canonicalOnly := true)) trace[Elab.inductive] "header params: {params}, type: {type}" let levelNames ← Term.getLevelNames - return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view } + let type ← mkForallFVars params type + return acc.push { levelNames, numParams := params.size, type, view, origParams := params } elabHeadersAux views (i+1) acc else return acc @@ -326,21 +323,21 @@ private def elabHeaders (views : Array InductiveView) : TermElabM (Array PreElab /-- Create a local declaration for each inductive type in `rs`, and execute `x params indFVars`, where `params` are the inductive type parameters and `indFVars` are the new local declarations. -We use the local context/instances and parameters of rs[0]. +We use the parameters of rs[0]. Note that this method is executed after we executed `checkHeaders` and established all parameters are compatible. -/ private def withInductiveLocalDecls (rs : Array PreElabHeaderResult) (x : Array Expr → Array Expr → TermElabM α) : TermElabM α := do - let namesAndTypes ← rs.mapM fun r => do - let type ← mkTypeFor r - pure (r.view.declName, r.view.shortDeclName, type) - let r0 := rs[0]! - let params := r0.params - withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do + let r0 := rs[0]! + forallBoundedTelescope r0.type r0.numParams fun params _ => withRef r0.view.ref do let rec loop (i : Nat) (indFVars : Array Expr) := do - if h : i < namesAndTypes.size then - let (declName, shortDeclName, type) := namesAndTypes[i] - withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar) + if h : i < rs.size then + let r := rs[i] + for param in params, origParam in r.origParams do + if let .fvar origFVar := origParam then + Elab.pushInfoLeaf <| .ofFVarAliasInfo { id := param.fvarId!, baseId := origFVar, userName := ← param.fvarId!.getUserName } + withAuxDecl r.view.shortDeclName r.type r.view.declName fun indFVar => + loop (i+1) (indFVars.push indFVar) else x params indFVars loop 0 #[] @@ -359,26 +356,6 @@ private def ElabHeaderResult.checkLevelNames (rs : Array PreElabHeaderResult) : unless r.levelNames == levelNames do throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes" -/-- -We need to work inside a single local context across all the inductive types, so we need to update the `ElabHeaderResult`s -so that resultant types refer to the fvars in `params`, the parameters for `rs[0]!` specifically. -Also updates the local contexts and local instances in each header. --/ -private def updateElabHeaderTypes (params : Array Expr) (rs : Array PreElabHeaderResult) (indFVars : Array Expr) : TermElabM (Array ElabHeaderResult) := do - rs.mapIdxM fun i r => do - /- - 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 - pure { r with lctx := ← getLCtx, localInsts := ← getLocalInstances, type := type, indFVar := indFVars[i]! } - private def getArity (indType : InductiveType) : MetaM Nat := forallTelescopeReducing indType.type fun xs _ => return xs.size @@ -878,7 +855,7 @@ private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep trace[Elab.inductive] "level names: {allUserLevelNames}" let res ← withInductiveLocalDecls rs fun params indFVars => do trace[Elab.inductive] "indFVars: {indFVars}" - let rs ← updateElabHeaderTypes params rs indFVars + let rs := Array.zipWith (fun r indFVar => { r with indFVar : ElabHeaderResult }) rs indFVars let mut indTypesArray : Array InductiveType := #[] let mut elabs' := #[] for h : i in [:views.size] do @@ -886,8 +863,7 @@ private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep let r := rs[i]! let elab' ← elabs[i]!.elabCtors rs r params elabs' := elabs'.push elab' - let type ← mkForallFVars params r.type - indTypesArray := indTypesArray.push { name := r.view.declName, type, ctors := elab'.ctors } + indTypesArray := indTypesArray.push { name := r.view.declName, type := r.type, ctors := elab'.ctors } Term.synthesizeSyntheticMVarsNoPostponing let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars trace[Elab.inductive] "numExplicitParams: {numExplicitParams}" diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 682aa9701f..bf94082fe9 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -1260,12 +1260,8 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace let fieldInfos := (← get).fields let lctx ← instantiateLCtxMVars (← getLCtx) /- The parameters `params` for the auxiliary "default value" definitions must be marked as implicit, and all others as explicit. -/ - let lctx := - params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) => - if p.isFVar then - lctx.setBinderInfo p.fvarId! BinderInfo.implicit - else - lctx + let lctx := params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) => + lctx.setBinderInfo p.fvarId! BinderInfo.implicit let parentFVarIds := fieldInfos |>.filter (·.kind.isParent) |>.map (·.fvar.fvarId!) let fields := fieldInfos |>.filter (!·.kind.isParent) withLCtx lctx (← getLocalInstances) do diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index b8bb6d4b9e..91ebb71f6d 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1878,13 +1878,14 @@ where go todo (autos.push auto) /-- - Similar to `autoBoundImplicits`, but immediately if the resulting array of expressions contains metavariables, - it immediately uses `mkForallFVars` + `forallBoundedTelescope` to convert them into free variables. + Similar to `addAutoBoundImplicits`, but converts all metavariables into free variables. + + It uses `mkForallFVars` + `forallBoundedTelescope` to convert metavariables into free variables. The type `type` is modified during the process if type depends on `xs`. We use this method to simplify the conversion of code using `autoBoundImplicitsOld` to `autoBoundImplicits`. -/ -def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → Expr → TermElabM α) : TermElabM α := do - let xs ← addAutoBoundImplicits xs none +def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → Expr → TermElabM α) (inlayHintPos? : Option String.Pos := none) : TermElabM α := do + let xs ← addAutoBoundImplicits xs inlayHintPos? if xs.all (·.isFVar) then k xs type else diff --git a/tests/lean/run/7788.lean b/tests/lean/run/7788.lean new file mode 100644 index 0000000000..4d72267070 --- /dev/null +++ b/tests/lean/run/7788.lean @@ -0,0 +1,77 @@ +/-! +# Regression test for autoparam panic in `inductive` parameters + +In the issue https://github.com/leanprover/lean4/issues/7788 +there's an error that appears in these circumstances: +Given an `inductive` command whose header induces an autoparam, +and that autoparam has a metavariable in its type, +then there is a panic in `Expr.fvarId!`. + +The problem came from not properly handling metavariables that appear in the parameter list, +which is how autoparams handle metavariables in their types (allowing them to be specialized later, +rather than committing to a free variable). +The fix was to be sure to abstract the parameters to create the type constructor types +(which incidentally simplified the handling of mutual inductives). +-/ + +set_option pp.mvars false + +namespace Ex1 + +def const (a : A) (_ : B) := a + +/-! +Here, `A` has an underdetermined type. +This results in two autoimplicits, one for `A` and one for its type. +-/ +inductive X (h : const Unit A) where + | a + +/-- info: Ex1.X.{u_1} {x✝ : Sort u_1} {A : x✝} (h : const Unit A) : Type -/ +#guard_msgs in #check X + +/-! +Because `A` and its type are abstracted at header elaboration time, +it is too late to be able to specialize its type from within the constructor. +-/ +/-- +error: type expected, got + (A : x✝) +-/ +#guard_msgs in +inductive X' (h : const Unit A) where + | a (x : A) + +end Ex1 + +namespace Ex2 + +def const (a : A) (_ : B) := a + +/-! +Make sure that `structure` can handle setting all the parameters to implicit +when processing default values. +(There used to be code that was conditional on a parameter being an fvar.) +-/ +structure S (a : const Unit A) where + x := a + +/-- info: Ex2.S.x._default.{u_1} {x✝ : Sort u_1} {A : x✝} {a : const Unit A} : const Unit A -/ +#guard_msgs in #check S.x._default + +end Ex2 + +namespace Ex3 +/-! +Example from issue #7788. Used to panic. +-/ + +/-- +error: function expected at + A +term has type + ?_ +-/ +#guard_msgs in inductive X (h : A 1) where + +end Ex3