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