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