max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: no default values for structure instance notation patterns (#13243)

Browse source 
This PR changes elaboration of structure instance notation when used in
patterns (e.g. `s matches { x := 1, y := [] }`) so that the structure's
default values are not used to elaborate the pattern. The motivation is
that default values frequently lead to surprisingly over-specific
patterns. It will now report "field missing" errors. The error can be
suppressed using `{ x := 1, .. }` ellipsis notation, which has the same
behavior as before. The pretty printer is also modified to stay in sync
with this feature. **Breaking change:** patterns using structure
instance notation may need missing fields or a `..` added, as
appropriate.

The rationale for the previous behavior is that with `..` you could
opt-in to not using default values, and now with this PR's behavior you
cannot opt-in. However, default values in structure instance patterns
are very likely to silently cause bugs. There are a couple examples in
this PR of unintentional default values in patterns in core Lean
(luckily these were not triggering bugs). With the new behavior, you can
now tell for sure whether every explicit field in a structure is being
matched explicitly or not, by the absence or presence of `..`.

Closes #10753
This commit is contained in:
Kyle Miller 2026-04-02 20:25:23 -07:00 • committed by GitHub
parent fcc070f18f
commit acae2b44fd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 118 additions and 59 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/PatternVar.lean
View file

@ -320,7 +320,7 @@ where
if f.getKind == ``Parser.Term.dotIdent then
let namedArgsNew ← namedArgs.mapM fun
-- We must ensure that `ref[1]` remains original to allow named-argument hints
| { ref, name, val := Arg.stx arg } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(ref[1]) := $(← collect arg)))
| { ref, name, val := Arg.stx arg, .. } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(ref[1]) := $(← collect arg)))
| _ => unreachable!
let mut argsNew ← args.mapM fun | Arg.stx arg => collect arg | _ => unreachable!
if ellipsis then

124
src/Lean/Elab/StructInst.lean
View file

@ -574,8 +574,14 @@ private def addSourceFields (structName : Name) (sources : Array ExplicitSourceV
private structure StructInstContext where
view : StructInstView
/-- True if the structure instance has a trailing `..`. -/
ellipsis : Bool
/-- If true, then try using parent instances for missing fields. -/
useParentInstanceFields : Bool
/-- If true, then try using default values or autoParams for missing fields.
(Considered after `useParentInstanceFields`.) -/
useDefaults : Bool
/-- If true, then missing fields after default value synthesis remain as metavariables rather than yielding an error.
Only applies if `useDefaults` is true. -/
unsynthesizedAsMVars : Bool
structName : Name
structType : Expr
/-- Structure universe levels. -/
@ -748,6 +754,8 @@ private structure PendingField where
deps : NameSet
val? : Option Expr
private def registerFieldMVarError (e : Expr) (ref : Syntax) (fieldName : Name) : StructInstM Unit :=
registerCustomErrorIfMVar e ref m!"Cannot synthesize placeholder for field `{fieldName}`"
/--
Synthesize pending optParams.
@ -778,7 +786,7 @@ private def synthOptParamFields : StructInstM Unit := do
-- Process default values for pending optParam fields.
let mut pendingFields : Array PendingField ← optParamFields.filterMapM fun (fieldName, fieldType, required) => do
if required || (← isFieldNotSolved? fieldName).isSome then
let (deps, val?) ← getFieldDefaultValue? fieldName
let (deps, val?) ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure ({}, none)
if let some val := val? then
trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
else
@ -831,44 +839,46 @@ private def synthOptParamFields : StructInstM Unit := do
pending
toRemove := toRemove.push selected.fieldName
if toRemove.isEmpty then
if (← read).ellipsis then
for pendingField in pendingFields do
if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
registerCustomErrorIfMVar (.mvar mvarId) (← read).view.ref m!"\
Cannot synthesize placeholder for field `{pendingField.fieldName}`"
return
let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList ""
let mut requiredErrors : Array MessageData := #[]
let mut unsolvedFields : Std.HashSet Name := {}
for pendingField in pendingFields do
if (← isFieldNotSolved? pendingField.fieldName).isNone then
unsolvedFields := unsolvedFields.insert pendingField.fieldName
let e := (← get).fieldMap.get! pendingField.fieldName
requiredErrors := requiredErrors.push m!"\
Field `{pendingField.fieldName}` must be explicitly provided; its synthesized value is{indentExpr e}"
let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList ""
let missingFields := pendingFields |>.filter (fun pending => pending.val?.isNone)
-- TODO(kmill): when fields are all stuck, report better.
-- For now, just report all pending fields in case there are no obviously missing ones.
let missingFields := if missingFields.isEmpty then pendingFields else missingFields
let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList
let missingFieldsValues ← missingFields.mapM fun field => do
if unsolvedFields.contains field.fieldName then
pure <| (field.fieldName, some <| (← get).fieldMap.get! field.fieldName)
else pure (field.fieldName, none)
let missingFieldsHint ← mkMissingFieldsHint missingFieldsValues (← read).view.ref
let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}"
if (← readThe Term.Context).errToSorry then
-- Assign all pending problems using synthetic sorries and log an error.
for pendingField in pendingFields do
if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
mvarId.assign <| ← mkLabeledSorry (← mvarId.getType) (synthetic := true) (unique := true)
logError msg
return
else
throwError msg
return ← handleStuck pendingFields assignErrors
pendingSet := pendingSet.filter (!toRemove.contains ·)
pendingFields := pendingFields.filter fun pendingField => pendingField.val?.isNone || !toRemove.contains pendingField.fieldName
where
handleStuck (pendingFields : Array PendingField) (assignErrors : Array MessageData) : StructInstM Unit := do
if (← read).unsynthesizedAsMVars then
for pendingField in pendingFields do
if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
registerFieldMVarError (.mvar mvarId) (← read).view.ref pendingField.fieldName
return
let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList ""
let mut requiredErrors : Array MessageData := #[]
let mut unsolvedFields : Std.HashSet Name := {}
for pendingField in pendingFields do
if (← isFieldNotSolved? pendingField.fieldName).isNone then
unsolvedFields := unsolvedFields.insert pendingField.fieldName
let e := (← get).fieldMap.get! pendingField.fieldName
requiredErrors := requiredErrors.push m!"\
Field `{pendingField.fieldName}` must be explicitly provided; its synthesized value is{indentExpr e}"
let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList ""
let missingFields := pendingFields |>.filter (fun pending => pending.val?.isNone)
-- TODO(kmill): when fields are all stuck, report better.
-- For now, just report all pending fields in case there are no obviously missing ones.
let missingFields := if missingFields.isEmpty then pendingFields else missingFields
let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList
let missingFieldsValues ← missingFields.mapM fun field => do
if unsolvedFields.contains field.fieldName then
pure <| (field.fieldName, some <| (← get).fieldMap.get! field.fieldName)
else pure (field.fieldName, none)
let missingFieldsHint ← mkMissingFieldsHint missingFieldsValues (← read).view.ref
let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}"
if (← readThe Term.Context).errToSorry then
-- Assign all pending problems using synthetic sorries and log an error.
for pendingField in pendingFields do
if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
mvarId.assign <| ← mkLabeledSorry (← mvarId.getType) (synthetic := true) (unique := true)
logError msg
return
else
throwError msg
private def finalize : StructInstM Expr := withViewRef do
let val := (← read).val.beta (← get).fields
@ -1049,19 +1059,13 @@ These fields can still be solved for by parent instance synthesis later.
-/
private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : BinderInfo) (fieldType : Expr) : StructInstM α := do
trace[Elab.struct] "processNoField `{fieldName}` of type {fieldType}"
if (← read).ellipsis && (← readThe Term.Context).inPattern then
-- See the note in `ElabAppArgs.processExplicitArg`
-- In ellipsis & pattern mode, do not use optParams or autoParams.
let e ← addStructFieldMVar fieldName fieldType
registerCustomErrorIfMVar e (← read).view.ref m!"don't know how to synthesize placeholder for field `{fieldName}`"
loop
else
if (← read).useDefaults then
let autoParam? := fieldType.getAutoParamTactic?
let fieldType := fieldType.consumeTypeAnnotations
if binfo.isInstImplicit then
let e ← addStructFieldMVar fieldName fieldType .synthetic
modify fun s => { s with instMVars := s.instMVars.push e.mvarId! }
loop
return ← loop
else if let some (.const tacticDecl ..) := autoParam? then
match evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl with
| .error err => throwError err
@ -1078,12 +1082,11 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
-- (See `processExplicitArg` for a comment about this.)
addTermInfo' stx mvar
addStructFieldAux fieldName mvar
loop
else
-- Default case: natural metavariable, register it for optParams
discard <| addStructFieldMVar fieldName fieldType
modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
loop
return ← loop
-- Default case: natural metavariable, register it for optParams
discard <| addStructFieldMVar fieldName fieldType
modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
loop
private partial def loop : StructInstM Expr := withViewRef do
let type := (← get).type
@ -1178,8 +1181,7 @@ private partial def addParentInstanceFields : StructInstM Unit := do
private def main : StructInstM Expr := do
initializeState
unless (← read).ellipsis && (← readThe Term.Context).inPattern do
-- Inside a pattern with ellipsis mode, users expect to match just the fields provided.
if (← read).useParentInstanceFields then
addParentInstanceFields
loop
@ -1198,7 +1200,17 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}"
let ellipsis := s.sources.implicit.isSome
let (val, _) ← main
|>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn, ellipsis }
|>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn
-- See the note in `ElabAppArgs.processExplicitArg`
-- For structure instances though, there's a sense in which app-style ellipsis mode is always enabled,
-- so we do not specifically check for it to disable defaults.
-- An effect of this is that if a user forgets `..` they'll be reminded with a "Fields missing" error.
useDefaults := !(← readThe Term.Context).inPattern
-- Similarly, for patterns we disable using parent instances to fill in fields
useParentInstanceFields := !(← readThe Term.Context).inPattern
-- In ellipsis mode, unsynthesized missing fields become metavariables, rather than being an error
unsynthesizedAsMVars := ellipsis
}
|>.run { type := ctorFnType }
return val

5
src/Lean/PrettyPrinter/Delaborator/Builtins.lean
View file

@ -619,8 +619,9 @@ private partial def collectStructFields
if s'.induct == parentName then
let (fieldValues, fields) ← collectStructFields structName levels params fields fieldValues s'
return (i + 1, fieldValues, fields)
/- Does this field have a default value? and if so, can we omit the field? -/
unless ← getPPOption getPPStructureInstancesDefaults do
/- Does this field have a default value? and if so, can we omit the field?
We cannot omit fields for patterns, since default values do not apply for them. -/
unless ← pure (← read).inPattern <||> getPPOption getPPStructureInstancesDefaults do
if let some defFn := getEffectiveDefaultFnForField? (← getEnv) structName fieldName then
-- Use `withNewMCtxDepth` to prevent delaborator from solving metavariables.
if let some (_, defValue) ← withNewMCtxDepth <| instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldValues.get?) then

46
tests/elab/10753.lean Normal file
View file

@ -0,0 +1,46 @@
/-!
# Structure instance notation should not use defaults in patterns
https://github.com/leanprover/lean4/issues/10753
-/
/-!
In the following, it used to be that the `{ b := bv }` pattern was matching
`{ b := bv, a := 0 }`, which was confusing.
-/
structure Test where
a : Nat := 0
b : Nat
/-- error: Fields missing: `a` -/
#guard_msgs in
def test1 (t : Test) : Nat :=
match t with
| { b := bv } => bv
def test2 (t : Test) : Nat :=
match t with
| { b := bv, .. } => bv
/-- info: 2 -/
#guard_msgs in #eval test2 { a := 1, b := 2 }
/-!
Check pretty printing: in a pattern, we can't assume we can omit default values.
We can of course omit them outside of patterns.
-/
def test3 (t : Test) : Test :=
match t with
| { b := bv, a := 0 } => { b := bv }
| _ => t
/--
info: def test3 : Test → Test :=
fun t =>
match t with
| { a := 0, b := bv } => { b := bv }
| x => t
-/
#guard_msgs in #print test3