From e0a29f43d2e4685febd0ed6bcfad511f7a235b6f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 9 Apr 2026 11:54:24 -0700 Subject: [PATCH] feat: adjust `deriving Inhabited` to use structure field defaults (#9815) This PR changes the `Inhabited` deriving handler for `structure` types to use default field values when present; this ensures that `{}` and `default` are interchangeable when all fields have default values. The handler effectively uses `by refine' {..} <;> exact default` to construct the inhabitant. (Note: when default field values cannot be resolved, they are ignored, as usual for ellipsis mode.) Implementation note: the handler now constructs the `Expr` directly and adds it to the environment, though the `instance` is still added using `elabCommand`. Closes #9463 --- src/Lean/Elab/Deriving/Inhabited.lean | 138 ++++++++++++++++---------- src/Lean/Elab/Term/TermElabM.lean | 10 +- src/Lean/Language/Basic.lean | 9 +- tests/elab/9463.lean | 125 +++++++++++++++++++++++ 4 files changed, 223 insertions(+), 59 deletions(-) create mode 100644 tests/elab/9463.lean diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 0b60bbca64..72f0ce87a5 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -25,25 +25,23 @@ private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name | none => return false where - addLocalInstancesForParamsAux {α} (k : LocalInst2Index → TermElabM α) : List Expr → Nat → LocalInst2Index → TermElabM α - | [], _, map => k map - | x::xs, i, map => + addLocalInstancesForParamsAux {α} (k : Array Expr → LocalInst2Index → TermElabM α) : List Expr → Nat → Array Expr → LocalInst2Index → TermElabM α + | [], _, insts, map => k insts map + | x::xs, i, insts, map => try let instType ← mkAppM `Inhabited #[x] - if (← isTypeCorrect instType) then - withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do - trace[Elab.Deriving.inhabited] "adding local instance {instType}" - addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i) - else - addLocalInstancesForParamsAux k xs (i+1) map + check instType + withLocalDecl (← mkFreshUserName `inst) .instImplicit instType fun inst => do + trace[Elab.Deriving.inhabited] "adding local instance {instType}" + addLocalInstancesForParamsAux k xs (i+1) (insts.push inst) (map.insert inst.fvarId! i) catch _ => - addLocalInstancesForParamsAux k xs (i+1) map + addLocalInstancesForParamsAux k xs (i+1) insts map - addLocalInstancesForParams {α} (xs : Array Expr) (k : LocalInst2Index → TermElabM α) : TermElabM α := do + addLocalInstancesForParams {α} (xs : Array Expr) (k : Array Expr → LocalInst2Index → TermElabM α) : TermElabM α := do if addHypotheses then - addLocalInstancesForParamsAux k xs.toList 0 {} + addLocalInstancesForParamsAux k xs.toList 0 #[] {} else - k {} + k #[] {} collectUsedLocalsInsts (usedInstIdxs : IndexSet) (localInst2Index : LocalInst2Index) (e : Expr) : IndexSet := if localInst2Index.isEmpty then @@ -58,58 +56,88 @@ where runST (fun _ => visit |>.run usedInstIdxs) |>.2 /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters - at position `i` and `i ∈ assumingParamIdxs`. -/ - mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do - let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName + at position `i` and `i ∈ usedInstIdxs`. -/ + mkInstanceCmdWith (instId : Ident) (usedInstIdxs : IndexSet) (auxFunId : Ident) : TermElabM Syntax := do let indVal ← getConstInfoInduct inductiveTypeName - let ctorVal ← getConstInfoCtor ctorName let mut indArgs := #[] let mut binders := #[] for i in *...indVal.numParams + indVal.numIndices do let arg := mkIdent (← mkFreshUserName `a) indArgs := indArgs.push arg - let binder ← `(bracketedBinderF| { $arg:ident }) - binders := binders.push binder - if assumingParamIdxs.contains i then - let binder ← `(bracketedBinderF| [Inhabited $arg:ident ]) - binders := binders.push binder + binders := binders.push <| ← `(bracketedBinderF| { $arg:ident }) + if usedInstIdxs.contains i then + binders := binders.push <| ← `(bracketedBinderF| [Inhabited $arg:ident ]) let type ← `(@$(mkCIdent inductiveTypeName):ident $indArgs:ident*) - let mut ctorArgs := #[] - for _ in *...ctorVal.numParams do - ctorArgs := ctorArgs.push (← `(_)) - for _ in *...ctorVal.numFields do - ctorArgs := ctorArgs.push (← ``(Inhabited.default)) - let val ← `(@$(mkIdent ctorName):ident $ctorArgs*) - let ctx ← mkContext ``Inhabited "default" inductiveTypeName - let auxFunName := ctx.auxFunNames[0]! - `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val - instance $(mkIdent ctx.instName):ident $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩) + `(instance $instId:ident $binders:bracketedBinder* : Inhabited $type := ⟨$auxFunId⟩) + solveMVarsWithDefault (e : Expr) : TermElabM Unit := do + let mvarIds ← getMVarsNoDelayed e + mvarIds.forM fun mvarId => mvarId.withContext do + unless ← mvarId.isAssigned do + let type ← mvarId.getType + withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"synthesizing Inhabited instance for{inlineExprTrailing type}") do + let val ← mkDefault type + mvarId.assign val + trace[Elab.Deriving.inhabited] "value:{inlineExprTrailing val}" - mkInstanceCmd? : TermElabM (Option Syntax) := do - let ctorVal ← getConstInfoCtor ctorName - forallTelescopeReducing ctorVal.type fun xs _ => - addLocalInstancesForParams xs[*...ctorVal.numParams] fun localInst2Index => do - let mut usedInstIdxs := {} - let mut ok := true - for h : i in ctorVal.numParams...xs.size do - let x := xs[i] - let instType ← mkAppM `Inhabited #[(← inferType x)] - trace[Elab.Deriving.inhabited] "checking {instType} for `{ctorName}`" - match (← trySynthInstance instType) with - | LOption.some e => - usedInstIdxs := collectUsedLocalsInsts usedInstIdxs localInst2Index e - | _ => - trace[Elab.Deriving.inhabited] "failed to generate instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}" - ok := false - break - if !ok then - return none + mkDefaultValue (indVal : InductiveVal) : TermElabM (Expr × Expr × IndexSet) := do + let us := indVal.levelParams.map Level.param + forallTelescopeReducing indVal.type fun xs _ => + withImplicitBinderInfos xs do + addLocalInstancesForParams xs[0...indVal.numParams] fun insts localInst2Index => do + let type := mkAppN (.const inductiveTypeName us) xs + let val ← + if isStructure (← getEnv) inductiveTypeName then + withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do + let stx ← `(structInst| {..}) + withoutErrToSorry <| elabTermAndSynthesize stx type else - trace[Elab.Deriving.inhabited] "inhabited instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}" - let cmd ← mkInstanceCmdWith usedInstIdxs - trace[Elab.Deriving.inhabited] "\n{cmd}" - return some cmd + withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do + let val := mkAppN (.const ctorName us) xs[0...indVal.numParams] + let (mvars, _, type') ← forallMetaTelescopeReducing (← inferType val) + unless ← isDefEq type type' do + throwError "cannot unify{indentExpr type}\nand type of constructor{indentExpr type'}" + pure <| mkAppN val mvars + solveMVarsWithDefault val + let val ← instantiateMVars val + if val.hasMVar then + throwError "default value contains metavariables{inlineExprTrailing val}" + let fvars := Lean.collectFVars {} val + let insts' := insts.filter fvars.visitedExpr.contains + let usedInstIdxs := collectUsedLocalsInsts {} localInst2Index val + assert! insts'.size == usedInstIdxs.size + trace[Elab.Deriving.inhabited] "inhabited instance using{inlineExpr val}{if insts'.isEmpty then m!"" else m!"(assuming parameters {insts'} are inhabited)"}" + let xs' := xs ++ insts' + let auxType ← mkForallFVars xs' type + let auxVal ← mkLambdaFVars xs' val + return (auxType, auxVal, usedInstIdxs) + + mkInstanceCmd? : TermElabM (Option Syntax) := + withExporting (isExporting := !isPrivateName ctorName) do + let ctx ← mkContext ``Inhabited "default" inductiveTypeName + let auxFunName := (← getCurrNamespace) ++ ctx.auxFunNames[0]! + let indVal ← getConstInfoInduct inductiveTypeName + let (auxType, auxVal, usedInstIdxs) ← + try + withDeclName auxFunName do mkDefaultValue indVal + catch e => + trace[Elab.Deriving.inhabited] "error: {e.toMessageData}" + return none + addDecl <| .defnDecl <| ← mkDefinitionValInferringUnsafe + (name := auxFunName) + (levelParams := indVal.levelParams) + (type := auxType) + (value := auxVal) + (hints := ReducibilityHints.regular (getMaxHeight (← getEnv) auxVal + 1)) + if isMarkedMeta (← getEnv) inductiveTypeName then + modifyEnv (markMeta · auxFunName) + unless (← read).isNoncomputableSection do + compileDecls #[auxFunName] + enableRealizationsForConst auxFunName + trace[Elab.Deriving.inhabited] "defined {.ofConstName auxFunName}" + let cmd ← mkInstanceCmdWith (mkIdent ctx.instName) usedInstIdxs (mkCIdent auxFunName) + trace[Elab.Deriving.inhabited] "\n{cmd}" + return some cmd private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do withoutExposeFromCtors declName do diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index 94aa9998b2..ccd3eda652 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -232,7 +232,10 @@ structure TacticFinishedSnapshot extends Language.Snapshot where state? : Option SavedState /-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation. -/ moreSnaps : Array (SnapshotTask SnapshotTree) -deriving Inhabited + +instance : Inhabited TacticFinishedSnapshot where + default := { toSnapshot := default, state? := default, moreSnaps := default } + instance : ToSnapshotTree TacticFinishedSnapshot where toSnapshotTree s := ⟨s.toSnapshot, s.moreSnaps⟩ @@ -246,7 +249,10 @@ structure TacticParsedSnapshot extends Language.Snapshot where finished : SnapshotTask TacticFinishedSnapshot /-- Tasks for subsequent, potentially parallel, tactic steps. -/ next : Array (SnapshotTask TacticParsedSnapshot) := #[] -deriving Inhabited + +instance : Inhabited TacticParsedSnapshot where + default := { toSnapshot := default, stx := default, finished := default } + partial instance : ToSnapshotTree TacticParsedSnapshot where toSnapshotTree := go where go := fun s => ⟨s.toSnapshot, diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 08f9b688fc..d5bc696a29 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -67,7 +67,9 @@ structure Snapshot where `diagnostics`) occurred that prevents processing of the remainder of the file. -/ isFatal := false -deriving Inhabited + +instance : Inhabited Snapshot where + default := { desc := "", diagnostics := default } /-- Range that is marked as being processed by the server while a task is running. -/ inductive SnapshotTask.ReportingRange where @@ -236,7 +238,10 @@ partial def SnapshotTask.cancelRec [ToSnapshotTree α] (t : SnapshotTask α) : B /-- Snapshot type without child nodes. -/ structure SnapshotLeaf extends Snapshot -deriving Inhabited, TypeName +deriving TypeName + +instance : Inhabited SnapshotLeaf where + default := { toSnapshot := default } instance : ToSnapshotTree SnapshotLeaf where toSnapshotTree s := SnapshotTree.mk s.toSnapshot #[] diff --git a/tests/elab/9463.lean b/tests/elab/9463.lean new file mode 100644 index 0000000000..94f6b0bd16 --- /dev/null +++ b/tests/elab/9463.lean @@ -0,0 +1,125 @@ +module +/-! +# `deriving Inhabited` uses structure field defaults + +https://github.com/leanprover/lean4/issues/9463 +-/ + +/-! +This used to use `false` in the `default` instance. +-/ +structure Config where + iota := true +deriving Inhabited + +/-- info: true -/ +#guard_msgs in #eval (default : Config).iota + +/-- info: instInhabitedConfig : Inhabited Config -/ +#guard_msgs in #check instInhabitedConfig + +/-! +We don't require that every field have a default value. +-/ +structure Config' where + iota := true + n : Nat +deriving Inhabited + +/-- info: true -/ +#guard_msgs in #eval (default : Config').iota +/-- info: 0 -/ +#guard_msgs in #eval (default : Config').n + +/-- info: instInhabitedConfig' : Inhabited Config' -/ +#guard_msgs in #check instInhabitedConfig' + +/-! +It still includes an `[Inhabited _]` parameter when needed. +-/ +structure Config'' (α : Type) where + iota := true + n : α +deriving Inhabited + +/-- info: true -/ +#guard_msgs in #eval (default : Config'' Nat).iota +/-- info: 0 -/ +#guard_msgs in #eval (default : Config'' Nat).n + +/-- info: instInhabitedConfig'' {a✝ : Type} [Inhabited a✝] : Inhabited (Config'' a✝) -/ +#guard_msgs in #check instInhabitedConfig'' + +/-! +In this example we can see that it adds an inhabited parameter. +-/ +structure Config''' (α : Type) where + n : α → α +deriving Inhabited + +/-- info: instInhabitedConfig''' {a✝ : Type} [Inhabited a✝] : Inhabited (Config''' a✝) -/ +#guard_msgs in #check instInhabitedConfig''' + +/-! +Providing a default value inhibits adding an inhabited parameter. +-/ +structure Config'''' (α : Type) where + n : α → α := id +deriving Inhabited + +/-- info: instInhabitedConfig'''' {a✝ : Type} : Inhabited (Config'''' a✝) -/ +#guard_msgs in #check instInhabitedConfig'''' + +/-! +Mixed needs for `Inhabited` parameters. +-/ +structure S (α β : Type) where + f : α → α := id + g : β +deriving Inhabited + +/-- info: instInhabitedS {a✝ a✝¹ : Type} [Inhabited a✝¹] : Inhabited (S a✝ a✝¹) -/ +#guard_msgs in #check instInhabitedS + +/-! +When there are structure field default value cycles, those defaults can be ignored. +-/ +structure A (α : Type) where + (x y : α) +deriving Inhabited +structure B extends A Nat where + n : Nat := 2 + x := y + 1 + y := x + 1 +deriving Inhabited + +/-- info: 2 -/ +#guard_msgs in #eval (default : B).n +/-- info: 0 -/ +#guard_msgs in #eval (default : B).x +/-- info: 0 -/ +#guard_msgs in #eval (default : B).y + +/-! +Regression test: take `meta` into account. +-/ +public meta section + +inductive AliasInfo where + | plain (n : Nat) +deriving Inhabited, Repr + +/-- info: AliasInfo.plain 0 -/ +#guard_msgs in #eval repr (default : AliasInfo) +end + +/-! +Regression test: take namespace into account. +-/ +structure MyNS.MyStruct where + x : Nat + deriving Inhabited +/-- info: MyNS.instInhabitedMyStruct.default : MyNS.MyStruct -/ +#guard_msgs in #check MyNS.instInhabitedMyStruct.default +/-- info: MyNS.instInhabitedMyStruct : Inhabited MyNS.MyStruct -/ +#guard_msgs in #check MyNS.instInhabitedMyStruct