From acae2b44fd8bb0c0009b4428529da9da6212df08 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 2 Apr 2026 20:25:23 -0700 Subject: [PATCH] feat: no default values for structure instance notation patterns (#13243) 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 --- src/Lean/Elab/PatternVar.lean | 2 +- src/Lean/Elab/StructInst.lean | 124 ++++++++++-------- .../PrettyPrinter/Delaborator/Builtins.lean | 5 +- tests/elab/10753.lean | 46 +++++++ 4 files changed, 118 insertions(+), 59 deletions(-) create mode 100644 tests/elab/10753.lean diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 22f4ac4c42..c30af3e5ab 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -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 diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 73f980fa24..1fd5354332 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -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 diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 006603b98b..51584aa29d 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -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 diff --git a/tests/elab/10753.lean b/tests/elab/10753.lean new file mode 100644 index 0000000000..b21393c83e --- /dev/null +++ b/tests/elab/10753.lean @@ -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