From fa1da03d50a697fece646327902a90073c4a7938 Mon Sep 17 00:00:00 2001 From: jrr6 <7482866+jrr6@users.noreply.github.com> Date: Tue, 29 Jul 2025 17:27:30 -0400 Subject: [PATCH] feat: update structure/inductive error messages (#9592) This PR updates the styling and wording of error messages produced in inductive type declarations and anonymous constructor notation, including hints for inferable constructor visibility updates. --- src/Lean/Elab/BuiltinNotation.lean | 28 ++- src/Lean/Elab/DeclUtil.lean | 8 +- src/Lean/Elab/Inductive.lean | 23 ++- src/Lean/Elab/MutualInductive.lean | 95 +++++---- src/Lean/Elab/Structure.lean | 194 +++++++++++------- tests/lean/1021.lean.expected.out | 4 +- tests/lean/277b.lean.expected.out | 5 +- tests/lean/ctorUnivTooBig.lean.expected.out | 12 +- tests/lean/diamond1.lean.expected.out | 4 +- tests/lean/inductive1.lean.expected.out | 44 ++-- .../inductiveUnivErrorMsg.lean.expected.out | 12 +- tests/lean/invalidFieldName.lean.expected.out | 2 +- .../lean/mvarAtDefaultValue.lean.expected.out | 2 +- .../lean/nonAtomicFieldName.lean.expected.out | 2 +- tests/lean/run/3467.lean | 4 +- tests/lean/run/4310.lean | 6 +- tests/lean/run/5236.lean | 6 +- tests/lean/run/6694.lean | 20 +- tests/lean/run/anonymous_ctor_error_msg.lean | 3 +- tests/lean/run/ctorFieldVisibilityHints.lean | 75 +++++++ tests/lean/run/inductive_univ.lean | 13 +- tests/lean/run/structBinderUpdates.lean | 12 +- tests/lean/run/structNamedParentProj.lean | 42 ++-- tests/lean/run/structureElab.lean | 12 +- tests/lean/struct1.lean.expected.out | 31 +-- .../structDefValueOverride.lean.expected.out | 2 +- tests/lean/univInference.lean.expected.out | 27 +-- tests/pkg/prv/Prv.lean | 2 +- 28 files changed, 451 insertions(+), 239 deletions(-) create mode 100644 tests/lean/run/ctorFieldVisibilityHints.lean diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 006ce5e78c..f365a2866d 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -47,16 +47,22 @@ open Meta match stx with | `(⟨$args,*⟩) => do tryPostponeIfNoneOrMVar expectedType? + let throwExpTypeUnknown {α} : TermElabM α := + throwError "Invalid `⟨...⟩` notation: The expected type of this term could not be determined" + let usageNote := .note m!"\ + This notation can only be used when the expected type is an inductive type with a single constructor" match expectedType? with | some expectedType => let expectedType ← whnf expectedType + if expectedType.getAppFn.isMVar then throwExpTypeUnknown matchConstInduct expectedType.getAppFn - (fun _ => throwError "invalid constructor ⟨...⟩, expected type must be an inductive type {indentExpr expectedType}") + (fun _ => throwError m!"Invalid `⟨...⟩` notation: The expected type{inlineExpr expectedType}is not an inductive type" + ++ usageNote) (fun ival _ => do match ival.ctors with | [ctor] => if isInaccessiblePrivateName (← getEnv) ctor then - throwError "invalid ⟨...⟩ notation, constructor for `{ival.name}` is marked as private" + throwError "Invalid `⟨...⟩` notation: Constructor for `{ival.name}` is marked as private" let cinfo ← getConstInfoCtor ctor let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do let mut n := 0 @@ -66,19 +72,29 @@ open Meta return n let args := args.getElems if args.size < numExplicitFields then - throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' has #{numExplicitFields} explicit fields, but only #{args.size} provided" + let fieldsStr := if numExplicitFields == 1 then "fields" else "field" + let providedStr := + if args.size == 0 then "none were" + else if args.size == 1 then "only 1 was" + else s!"only {args.size} were" + throwError "Insufficient number of fields for `⟨...⟩` constructor: Constructor \ + `{ctor}` has {numExplicitFields} explicit {fieldsStr}, but {providedStr} provided" let newStx ← if args.size == numExplicitFields then `($(mkCIdentFrom stx ctor (canonical := true)) $(args)*) else if numExplicitFields == 0 then - throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' does not have explicit fields, but #{args.size} provided" + throwError "Insufficient number of fields for `⟨...⟩` constructor: Constructor \ + `{ctor}` does not have explicit fields, but {args.size} + {if args.size == 1 then "was" else "were"} provided" else let extra := args[(numExplicitFields-1)...args.size] let newLast ← `(⟨$[$extra],*⟩) let newArgs := args[*...(numExplicitFields-1)].toArray.push newLast `($(mkCIdentFrom stx ctor (canonical := true)) $(newArgs)*) withMacroExpansion stx newStx $ elabTerm newStx expectedType? - | _ => throwError "invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor {indentExpr expectedType}") - | none => throwError "invalid constructor ⟨...⟩, expected type must be known" + | [] => throwError "Invalid `⟨...⟩` notation: The expected type{inlineExpr expectedType}has no constructors" + | _ => throwError m!"Invalid `⟨...⟩` notation: The expected type{inlineExpr expectedType}has more than one constructor" + ++ usageNote) + | none => throwExpTypeUnknown | _ => throwUnsupportedSyntax @[builtin_term_elab borrowed] def elabBorrowed : TermElab := fun stx expectedType? => diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean index 822f98be35..de7236517e 100644 --- a/src/Lean/Elab/DeclUtil.lean +++ b/src/Lean/Elab/DeclUtil.lean @@ -22,21 +22,21 @@ def forallTelescopeCompatibleAux (k : Array Expr → Expr → Expr → MetaM α) | .forallE n₁ d₁ b₁ c₁, .forallE n₂ d₂ b₂ c₂ => -- Remark: we use `mkIdent` to ensure macroscopes do not leak into error messages unless c₁ == c₂ do - throwError "binder annotation mismatch at parameter '{mkIdent n₁}'" + throwError "Binder annotations for parameter `{mkIdent n₁}` must match" /- Remark: recall that users may suppress parameter names for instance implicit arguments. A fresh name (with macro scopes) is generated in this case. Thus, we allow the names to be different in this case. See issue #4310. -/ unless n₁ == n₂ || (c₁.isInstImplicit && n₁.hasMacroScopes && n₂.hasMacroScopes) do - throwError "parameter name mismatch '{mkIdent n₁}', expected '{mkIdent n₂}'" + throwError "Parameter names `{mkIdent n₁}` and `{mkIdent n₂}` differ but were expected to match" unless (← isDefEq d₁ d₂) do - throwError "parameter '{mkIdent n₁}' {← mkHasTypeButIsExpectedMsg d₁ d₂}" + throwError "Parameter `{mkIdent n₁}` {← mkHasTypeButIsExpectedMsg d₁ d₂}" withLocalDecl n₁ c₁ d₁ fun x => let type₁ := b₁.instantiate1 x let type₂ := b₂.instantiate1 x forallTelescopeCompatibleAux k i type₁ type₂ (xs.push x) - | _, _ => throwError "unexpected number of parameters" + | _, _ => throwError "Internal error: Mismatched number of parameters when checking type compatibility" /-- Given two forall-expressions `type₁` and `type₂`, ensure the first `numParams` parameters are compatible, and then execute `k` with the parameters and remaining types. -/ diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 5493a968e9..a2ff71dc52 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -35,15 +35,28 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig ``` -/ - let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩ + let modifiersStx := ctor[2] + let mut ctorModifiers ← elabModifiers ⟨modifiersStx⟩ if let some leadingDocComment := ctor[0].getOptional? then if ctorModifiers.docString?.isSome then - logErrorAt leadingDocComment "duplicate doc string" + logErrorAt leadingDocComment "Duplicate doc string" ctorModifiers := { ctorModifiers with docString? := some ⟨leadingDocComment⟩ } if ctorModifiers.isPrivate && modifiers.isPrivate then - throwError "invalid 'private' constructor in a 'private' inductive datatype" + let hint ← do + let .original .. := modifiersStx.getHeadInfo | pure .nil + let some range := modifiersStx[2].getRangeWithTrailing? | pure .nil + -- Drop the doc comment from both the `declModifiers` and outer `ctor`, as well as + -- everything after the constructor name (yielding invalid syntax with the desired range) + let previewSpan? := ctor.modifyArgs (·[2...4].toArray.modify 0 (·.modifyArgs (·[1...*]))) + MessageData.hint "Remove `private` modifier from constructor" #[{ + suggestion := "" + span? := Syntax.ofRange range + previewSpan? + toCodeActionTitle? := some fun _ => "Delete `private` modifier" + }] + throwError m!"Constructor cannot be marked `private` because it is already in a `private` inductive datatype" ++ hint if ctorModifiers.isProtected && modifiers.isPrivate then - throwError "invalid 'protected' constructor in a 'private' inductive datatype" + throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype" checkValidCtorModifier ctorModifiers let ctorName := ctor.getIdAt 3 let ctorName := declName ++ ctorName @@ -58,7 +71,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term if decl[3][0].isToken ":=" then -- https://github.com/leanprover/lean4/issues/5236 withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3] - "'inductive ... :=' has been deprecated in favor of 'inductive ... where'." + "`inductive ... :=` has been deprecated in favor of `inductive ... where`" return { ref := decl shortDeclName := name diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 45f80258a6..996498b376 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -207,42 +207,48 @@ Initializes the elaborator associated to the given syntax. def mkInductiveView (modifiers : Modifiers) (stx : Syntax) : TermElabM InductiveElabStep1 := do let handlers := inductiveElabAttr.getValues (← getEnv) stx.getKind if handlers.isEmpty then - throwErrorAt stx "no '@[inductive_elab]' for '{.ofConstName stx.getKind}'" + throwErrorAt stx "Failed to elaborate inductive type declaration: There is no `@[inductive_elab]` \ + handler for `{.ofConstName stx.getKind}` syntax" handlers[0]!.mkInductiveView modifiers stx def checkValidInductiveModifier [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit := do if modifiers.isNoncomputable then - throwError "invalid use of 'noncomputable' in inductive declaration" + throwError "Invalid modifier: Inductive declarations cannot be marked as `noncomputable`" if modifiers.isPartial then - throwError "invalid use of 'partial' in inductive declaration" + throwError "Invalid modifier: Inductive declarations cannot be marked as `partial`" def checkValidCtorModifier [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit := do if modifiers.isNoncomputable then - throwError "invalid use of 'noncomputable' in constructor declaration" + throwError "Invalid modifier: Constructors cannot be marked as `noncomputable`" if modifiers.isPartial then - throwError "invalid use of 'partial' in constructor declaration" + throwError "Invalid modifier: Constructors cannot be marked as `partial`" if modifiers.isUnsafe then - throwError "invalid use of 'unsafe' in constructor declaration" + throwError "Invalid modifier: Constructors cannot be marked as `unsafe`" if modifiers.attrs.size != 0 then - throwError "invalid use of attributes in constructor declaration" + throwError "Invalid attribute: Attributes cannot be added to constructors" private def checkUnsafe (rs : Array PreElabHeaderResult) : TermElabM Unit := do let isUnsafe := rs[0]!.view.modifiers.isUnsafe for r in rs do unless r.view.modifiers.isUnsafe == isUnsafe do - throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in mutually inductive datatypes" + let unsafeStr (b : Bool) := if b then "unsafe" else "safe" + throwErrorAt r.view.ref m!"Invalid mutually inductive types: `{r.view.declName}` is {unsafeStr (!isUnsafe)}, \ + but `{rs[0]!.view.declName}` is {unsafeStr isUnsafe}" + ++ .note m!"Safe and unsafe inductive declarations cannot both occur in the same `mutual` block" private def checkClass (rs : Array PreElabHeaderResult) : TermElabM Unit := do if rs.size > 1 then for r in rs do if r.view.isClass then - throwErrorAt r.view.ref "invalid inductive type, mutual classes are not supported" + throwErrorAt r.view.ref "Invalid mutually inductive type: Mutually inductive classes are not supported" private def checkNumParams (rs : Array PreElabHeaderResult) : TermElabM Nat := do let numParams := rs[0]!.numParams for r in rs do unless r.numParams == numParams do - throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes" + throwErrorAt r.view.ref m!"Invalid mutually inductive types: `{r.view.shortDeclName}` has {r.numParams} \ + parameter(s), but the preceding type `{rs[0]!.view.shortDeclName}` has {numParams}" + ++ .note m!"All inductive types declared in the same `mutual` block must have the same parameters" return numParams /-- @@ -267,13 +273,15 @@ private def checkParamsAndResultType (type firstType : Expr) (numParams : Nat) : match type with | .sort .. => unless (← isDefEq firstType type) do - throwError "resulting universe mismatch, given{indentExpr type}\nexpected type{indentExpr firstType}" + throwError m!"The resulting type of this declaration{indentExpr type}\ndiffers from a preceding one{indentExpr firstType}" + ++ .note "All inductive types declared in the same `mutual` block must belong to the same type universe" | _ => - throwError "unexpected inductive resulting type" + throwError "The specified resulting type{inlineExpr type}is not a type" catch - | Exception.error ref msg => throw (Exception.error ref m!"invalid mutually inductive types, {msg}") + | Exception.error ref msg => throw (Exception.error ref m!"Invalid mutually inductive types: {msg}") | ex => throw ex + /-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible. -/ @@ -305,10 +313,12 @@ private def elabHeadersAux (views : Array InductiveView) (i : Nat) (acc : Array let type ← mkForallFVars indices type if view.allowIndices then unless (← isTypeFormerType type) do - throwErrorAt typeStx "invalid resulting type, expecting 'Sort _' or an indexed family of sorts" + throwErrorAt typeStx m!"Invalid resulting type: Expected a sort or an indexed family of sorts" + ++ .hint' m!"Examples of valid sorts include `Type _`, `Sort _`, and `Prop`" else unless (← whnfD type).isSort do - throwErrorAt typeStx "invalid resulting type, expecting 'Type _' or 'Prop'" + throwErrorAt typeStx m!"Invalid resulting type: Expected a sort" + ++ .hint' m!"Examples of valid sorts include `Type _`, `Sort _`, and `Prop`" return (type, indices.size) let params ← Term.addAutoBoundImplicits params (view.declId.getTailPos? (canonicalOnly := true)) trace[Elab.inductive] "header params: {params}, type: {type}" @@ -353,19 +363,27 @@ private def withInductiveLocalDecls (rs : Array PreElabHeaderResult) (x : Array x params indFVars loop 0 #[] +private def throwLevelNameMismatch [Monad m] [MonadError m] + (curNames prevNames : List Name) (curDeclName prevDeclName : Name) : m α := + let listNames (names : List Name) := MessageData.joinSep (names.map (m!"`{·}`")) ", " + throwError m!"Universe parameter mismatch in mutually inductive types: `{curDeclName}` \ + has universe parameters{indentD (listNames curNames)}\nbut the preceding declaration \ + `{prevDeclName}` has{indentD (listNames prevNames)}" + ++ .note m!"All inductive declarations in the same `mutual` block must have the same universe level parameters" + private def InductiveElabStep1.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do if h : views.size > 1 then let levelNames := views[0].levelNames for view in views do unless view.levelNames == levelNames do - throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes" + withRef view.ref <| throwLevelNameMismatch view.levelNames levelNames view.shortDeclName views[0].shortDeclName private def ElabHeaderResult.checkLevelNames (rs : Array PreElabHeaderResult) : TermElabM Unit := do if h : rs.size > 1 then let levelNames := rs[0].levelNames for r in rs do unless r.levelNames == levelNames do - throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes" + throwLevelNameMismatch r.levelNames levelNames r.view.declName rs[0].view.shortDeclName private def getArity (indType : InductiveType) : MetaM Nat := forallTelescopeReducing indType.type fun xs _ => return xs.size @@ -473,12 +491,12 @@ private def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveTy go numParams type typesToCheck private def getResultingUniverse : List InductiveType → TermElabM Level - | [] => throwError "unexpected empty inductive declaration" + | [] => throwError "Unexpected empty inductive declaration" | indType :: _ => forallTelescopeReducing indType.type fun _ r => do let r ← whnfD r match r with | Expr.sort u => return u - | _ => throwError "unexpected inductive type resulting type{indentExpr r}" + | _ => throwError "Unexpected inductive type resulting type{indentExpr r}" /-- Returns `some ?m` if `u` is of the form `?m + k`. @@ -491,10 +509,10 @@ def shouldInferResultUniverse (u : Level) : TermElabM (Option LMVarId) := do match u.getLevelOffset with | Level.mvar mvarId => return some mvarId | _ => - throwError "\ - cannot infer resulting universe level of inductive datatype, \ - given resulting type contains metavariables{indentExpr <| mkSort u}\n\ - provide universe explicitly" + throwError m!"\ + Cannot infer resulting universe level of inductive datatype: \ + The given resulting type contains metavariables{indentExpr <| mkSort u}" + ++ .hint' "Provide the uninferred universe(s) explicitly" else return none @@ -554,7 +572,7 @@ where pure () else if r.occurs u then /- `f(?r) = ?r + k`. -/ - throw m!"in the constraint {u} ≤ {Level.addOffset r rOffset}, the level metavariable {r} appears in both sides" + throw m!"In the constraint `{u} ≤ {Level.addOffset r rOffset}`, the level metavariable `{r}` appears in both sides" else modify fun acc => acc.push u rOffset @@ -567,7 +585,7 @@ def accLevelAtCtor (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateT AccLe match (← modifyGet fun s => accLevel u r rOffset |>.run |>.run s) with | .ok _ => pure () | .error msg => - throwError "failed to infer universe level for resulting type due to the constructor argument '{ctorParam}', {msg}" + throwError "Failed to infer universe level for resulting type due to the constructor argument `{ctorParam}`: {msg}" /-- Executes `k` using the `Syntax` reference associated with constructor `ctorName`. @@ -603,17 +621,17 @@ private def collectUniverses (views : Array InductiveView) (r : Level) (rOffset let badPart := Level.mkNaryMax (acc.badLevels.toList.map fun (u, k) => Level.max (Level.ofNat rOffset) (Level.addOffset u (rOffset - k))) let inferred := (Level.max goodPart badPart).normalize let badConstraints := acc.badLevels.map fun (u, k) => indentD m!"{u} ≤ {Level.addOffset r k}" - throwError "resulting type is of the form{indentD <| mkSort (Level.addOffset r rOffset)}\n\ + throwError "Resulting type is of the form{indentD <| mkSort (Level.addOffset r rOffset)}\n\ but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. \ Explicitly providing a resulting type will silence this error. \ Universe inference suggests using{indentD <| mkSort inferred}\n\ if the resulting universe level should be at the above universe level or higher.\n\n\ Explanation: At this point in elaboration, universe level unification has committed to using a \ - resulting universe level of the form '{Level.addOffset r rOffset}'. \ + resulting universe level of the form `{Level.addOffset r rOffset}`. \ Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s):\ {MessageData.joinSep badConstraints.toList ""}\n\ However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. \ - For example, if the resulting type is of the form 'Sort (_ + 1)' and a constructor argument is in universe `Sort u`, \ + For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, \ then universe inference would yield `Sort (u + 1)`, \ but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary." return acc.levels @@ -675,7 +693,8 @@ private def updateResultingUniverse (views : Array InductiveView) (numParams : N let rOffset : Nat := r₀.getOffset let r : Level := r₀.getLevelOffset unless r.isMVar do - throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly: {r₀}" + throwError m!"Failed to compute resulting universe level of inductive datatype: {r₀}" + ++ .hint' "Provide this universe explicitly" let us ← collectUniverses views r rOffset numParams indTypes trace[Elab.inductive] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}" let rNew := mkResultUniverse us rOffset (← isPropCandidate numParams indTypes) @@ -693,9 +712,9 @@ unless one of the inductive commands requires it (for instance `structure` due t private def checkResultingUniversePolymorphism (views : Array InductiveView) (u : Level) (_numParams : Nat) (_indTypes : List InductiveType) : TermElabM Unit := do let doErrFor := fun view => view.withTypeRef do - throwError "\ - invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values:{indentD (mkSort u)}\n\ - Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'." + throwError m!"\ + Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:{indentD (mkSort u)}" + ++ .hint' m!"A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`" unless u.isZero || u.isNeverZero do for view in views do if !view.allowSortPolymorphism then @@ -733,7 +752,7 @@ where propagateConstraint (v : Level) (r : Level) (k : Nat) : MetaM Unit := do match v, k with | .zero, _ => pure () - | .succ _, 0 => throwError "(for debug) {v} ≤ 0 is impossible" + | .succ _, 0 => throwError "Internal error: Generated an impossible universe constraint `{v} ≤ 0`" | .succ u, k+1 => propagateConstraint u r k | .max u v, k => propagateConstraint u r k; propagateConstraint v r k /- @@ -776,9 +795,9 @@ private def checkResultingUniverses (views : Array InductiveView) (elabs' : Arra let type ← inferType ctorArg let v := (← instantiateLevelMVars (← getLevel type)).normalize unless u.geq v do - let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter" + let mut msg := m!"Invalid universe level in constructor `{ctor.name}`: Parameter" unless (← ctorArg.fvarId!.getUserName).hasMacroScopes do - msg := msg ++ m!" '{ctorArg}'" + msg := msg ++ m!" `{ctorArg}`" msg := msg ++ m!" has type{indentExpr type}\n\ at universe level{indentD v}\n\ which is not less than or equal to the inductive type's resulting universe level{indentD u}" @@ -984,13 +1003,13 @@ private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) : T let typeDeclName := privateToUserName view.declName if let some (prevNameIsType, prevRef) := uniqueNames[typeDeclName]? then let declKinds := if prevNameIsType then "multiple inductive types" else "an inductive type and a constructor" - throwErrorsAt prevRef view.declId m!"cannot define {declKinds} with the same name '{typeDeclName}'" + throwErrorsAt prevRef view.declId m!"Cannot define {declKinds} with the same name `{typeDeclName}`" uniqueNames := uniqueNames.insert typeDeclName (true, view.declId) for ctor in view.ctors do let ctorName := privateToUserName ctor.declName if let some (prevNameIsType, prevRef) := uniqueNames[ctorName]? then let declKinds := if prevNameIsType then "an inductive type and a constructor" else "multiple constructors" - throwErrorsAt prevRef ctor.declId m!"cannot define {declKinds} with the same name '{ctorName}'" + throwErrorsAt prevRef ctor.declId m!"Cannot define {declKinds} with the same name `{ctorName}`" uniqueNames := uniqueNames.insert ctorName (false, ctor.declId) private def applyComputedFields (indViews : Array InductiveView) : CommandElabM Unit := do @@ -1005,7 +1024,7 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM | `(Lean.Parser.Command.declModifiersT| $[$doc:docComment]? $[$attrs:attributes]? $[$vis]? $[noncomputable]?) => `(Lean.Parser.Command.declModifiersT| $[$doc]? $[$attrs]? $[$vis]? noncomputable) | _ => do - withRef modifiers do logError "unsupported modifiers for computed field" + withRef modifiers do logError "Unsupported modifiers for computed field" `(Parser.Command.declModifiersT| noncomputable) `($(⟨modifiers⟩):declModifiers def%$ref $(mkIdent <| `_root_ ++ declName ++ fieldId):ident : $type $matchAlts:matchAlts) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 6470fbf944..37ba3179b9 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -198,6 +198,29 @@ structure StructFieldInfo where private def defaultCtorName := `mk +/-- +Drops the docstring from structure constructor or binder syntax (i.e., syntax with leading +`declModifiers`), preserving source information. Used for generating error message hint spans. +-/ +private def dropLeadingDeclModifiersDocstring (stx : Syntax) : Syntax := + stx.modifyArgs (·.modify 0 (·.setArg 0 mkNullNode)) + +/-- +Creates a hint to delete a `private` modifier from the decl modifiers `stx` of either a field or a +constructor (indicated by the value of `fieldKindDescr`) if such a modifier exists. `fullSpan` +should be the full field or constructor syntax, whose first argument is a doc comment. +-/ +private def mkDeletePrivateFieldHint (stx : TSyntax ``Parser.Command.declModifiers) (fullSpan : Syntax) (fieldKindDescr : String) := do + let previewSpan? := dropLeadingDeclModifiersDocstring fullSpan + let .original .. := stx.raw.getHeadInfo | pure .nil + let some range := stx.raw[2].getRangeWithTrailing? | pure .nil + MessageData.hint m!"Remove `private` modifier from {fieldKindDescr}" #[{ + suggestion := "" + span? := Syntax.ofRange range + toCodeActionTitle? := some fun _ => "Delete `private` modifier" + previewSpan? + }] + /- The structure constructor syntax is ``` @@ -224,14 +247,30 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc else let ctor := optCtor[0] withRef ctor do - let ctorModifiers ← elabModifiers ctor[0] + let modifiersStx := ctor[0] + let ctorModifiers ← elabModifiers modifiersStx checkValidCtorModifier ctorModifiers if ctorModifiers.isPrivate && structModifiers.isPrivate then - throwError "invalid 'private' constructor in a 'private' structure" + let hint ← mkDeletePrivateFieldHint modifiersStx ctor "constructor" + throwError m!"Constructor cannot be marked `private` because it is already in a `private` structure" ++ hint if ctorModifiers.isProtected && structModifiers.isPrivate then - throwError "invalid 'protected' constructor in a 'private' structure" + throwError "Constructor cannot be `protected` because this structure is `private`" if !ctorModifiers.isPrivate && forcePrivate then - throwError "invalid constructor visibility, must be private in presence of private fields" + let hint ← do + let .original .. := ctor.getHeadInfo | pure .nil + let spanSuggestion? := + if modifiersStx[2].getRange?.isSome then + some (modifiersStx[2], "private") + -- Place `private` after the doc comment, or else before other modifiers, or else before the identifier + else if let some pos := modifiersStx[0].getTrailingTailPos? <|> modifiersStx.getPos? <|> ctor[1].getPos? then + some (Syntax.ofRange ⟨pos, pos⟩, "private ") + else none + let some (span?, suggestion) := spanSuggestion? | pure .nil + let previewSpan? := dropLeadingDeclModifiersDocstring ctor + MessageData.hint m!"Mark constructor as `private`" #[{ + suggestion, span?, previewSpan?, toCodeActionTitle? := some fun _ => "Mark constructor private" + }] + throwError m!"Constructor must be `private` because one or more of this structure's fields are `private`" ++ hint let name := ctor[1].getId let declName := structDeclName ++ name let declName ← applyVisibility ctorModifiers.visibility declName @@ -258,7 +297,7 @@ private def expandParents (optExtendsStx : Syntax) : TermElabM (Array StructPare let rawName := ident.getId let name := rawName.eraseMacroScopes unless name.isAtomic do - throwErrorAt ident "invalid parent projection name '{name}', names must be atomic" + throwErrorAt ident "Invalid parent projection name `{name}`: Name must be atomic" projRef := ident rawName? := rawName name? := name @@ -273,13 +312,13 @@ private def expandParents (optExtendsStx : Syntax) : TermElabM (Array StructPare def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do if modifiers.isNoncomputable then - throwError "invalid use of 'noncomputable' in field declaration" + throwError "Invalid modifier: Fields cannot be marked as `noncomputable`" if modifiers.isPartial then - throwError "invalid use of 'partial' in field declaration" + throwError "Invalid modifier: Fields cannot be marked as `partial`" if modifiers.isUnsafe then - throwError "invalid use of 'unsafe' in field declaration" + throwError "Invalid modifier: Fields cannot be marked as `unsafe`" if modifiers.attrs.size != 0 then - throwError "invalid use of attributes in field declaration" + throwError "Invalid attribute: Attributes cannot be added to fields" /- ``` @@ -295,7 +334,7 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str -- https://github.com/leanprover/lean4/issues/5236 let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure" withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[4][0] - s!"{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'." + s!"`{cmd} ... :=` has been deprecated in favor of `{cmd} ... where`." let fieldBinders := if structStx[4].isNone then #[] else structStx[4][2][0].getArgs fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do let mut fieldBinder := fieldBinder @@ -307,13 +346,14 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str if k == ``Parser.Command.structExplicitBinder then pure BinderInfo.default else if k == ``Parser.Command.structImplicitBinder then pure BinderInfo.implicit else if k == ``Parser.Command.structInstBinder then pure BinderInfo.instImplicit - else throwError "unexpected kind of structure field" + else throwError "Found an unexpected binder type for field{indentD fieldBinder}" let fieldModifiers ← elabModifiers fieldBinder[0] checkValidFieldModifier fieldModifiers if fieldModifiers.isPrivate && structModifiers.isPrivate then - throwError "invalid 'private' field in a 'private' structure" + let hint ← mkDeletePrivateFieldHint fieldBinder[0] fieldBinder "field" + throwError m!"Field cannot be marked `private` because it is already in a `private` structure" ++ hint if fieldModifiers.isProtected && structModifiers.isPrivate then - throwError "invalid 'protected' field in a 'private' structure" + throwError "Field cannot be marked `protected` because this structure is `private`" let (binders, type?, default?) ← if binfo == BinderInfo.default then let (binders, type?) := expandOptDeclSig fieldBinder[3] @@ -337,7 +377,7 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str let rawName := ident.getId let name := rawName.eraseMacroScopes unless name.isAtomic do - throwErrorAt ident "invalid field name '{name.eraseMacroScopes}', field names must be atomic" + throwErrorAt ident "Invalid field name `{name.eraseMacroScopes}`: Field names must be atomic" let declName := structDeclName ++ name let declName ← applyVisibility fieldModifiers.visibility declName addDocString' declName fieldModifiers.docString? @@ -377,16 +417,16 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str let type? ← -- Compatibility mode for `structure S extends P : Type` syntax if type?.isNone && !exts.isNone && !exts[0][2].isNone then - logWarningAt exts[0][2][0] "\ - The syntax is now 'structure S : Type extends P' rather than 'structure S extends P : Type'.\n\n\ - The purpose of this change is to accommodate 'structure S extends toP : P' syntax for naming parent projections." + logWarningAt exts[0][2][0] <| "\ + The syntax is now `structure S : Type extends P` rather than `structure S extends P : Type`" + ++ .note "The purpose of this change is to accommodate `structure S extends toP : P` syntax for naming parent projections." pure (some exts[0][2][0][1]) else if !exts.isNone && !exts[0][2].isNone then - logErrorAt exts[0][2][0] "\ - Unexpected additional resulting type. \ - The syntax is now 'structure S : Type extends P' rather than 'structure S extends P : Type'.\n\n\ - The purpose of this change is to accommodate 'structure S extends toP : P' syntax for naming parent projections." + logErrorAt exts[0][2][0] <| "\ + Unexpected additional resulting type. \ + The syntax is now `structure S : Type extends P` rather than `structure S extends P : Type`." + ++ .note "The purpose of this change is to accommodate `structure S extends toP : P` syntax for naming parent projections." pure type? let parents ← expandParents exts let derivingClasses ← getOptDerivingClasses stx[5] @@ -397,7 +437,7 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str stx modifiers declName fields.forM fun field => do if field.declName == ctor.declName then - throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name" + throwErrorAt field.ref "Invalid field name `{field.name}`: This is the name of the structure constructor" addDeclarationRangesFromSyntax field.declName field.ref return { ref := stx @@ -466,7 +506,7 @@ Throws an error if there is already a field with that name. -/ private def addFieldInfo (info : StructFieldInfo) : StructElabM Unit := do if ← hasFieldName info.name then - throwError "(in addFieldInfo) structure field '{info.name}' already exists" + throwError "Internal error in addFieldInfo: Structure field `{info.name}` already exists" else modify fun s => let idx := s.fields.size @@ -494,11 +534,11 @@ private def replaceFieldInfo (info : StructFieldInfo) : StructElabM Unit := do if let some idx := (← get).fieldIdx.find? info.name then modify fun s => { s with fields := s.fields.set! idx info } else - throwError "(in replaceFieldInfo) structure field '{info.name}' does not already exist" + throwError "Internal error in replaceFieldInfo: Structure field `{info.name}` does not already exist" private def addFieldInheritedDefault (fieldName : Name) (structName : Name) (d : StructFieldDefault) : StructElabM Unit := do let some info ← findFieldInfo? fieldName - | throwError "(in addFieldInheritedDefault) structure field '{fieldName}' does not already exist" + | throwError "Internal error in addFieldInheritedDefault: Structure field `{fieldName}` does not already exist" replaceFieldInfo { info with inheritedDefaults := info.inheritedDefaults.push (structName, d) } /-- @@ -538,9 +578,9 @@ private def fieldNormalizeExpr (e : Expr) (zetaDelta : Bool := true) : StructEla private def fieldFromMsg (info : StructFieldInfo) : MessageData := if let some sourceStructName := info.sourceStructNames.head? then - m!"field '{info.name}' from '{.ofConstName sourceStructName}'" + m!"field `{info.name}` from `{.ofConstName sourceStructName}`" else - m!"field '{info.name}'" + m!"field `{info.name}`" /-- Instantiates default value for field `fieldName` set at structure `structName`, using the field fvars in the `StructFieldInfo`s. @@ -555,7 +595,7 @@ private partial def getFieldDefaultValue? (structName : Name) (params : Array Ex let some info ← findFieldInfo? n | return none return info.fvar let some (_, val) ← instantiateStructDefaultValueFn? defFn none params fieldVal? - | logWarning m!"default value for field '{fieldName}' of structure '{.ofConstName structName}' could not be instantiated, ignoring" + | logWarning m!"Default value for field `{fieldName}` of structure `{.ofConstName structName}` could not be instantiated; ignoring" return none return val @@ -593,7 +633,7 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis let fieldType := fieldType.consumeTypeAnnotations -- remove autoParam from constructor field let env ← getEnv let some fieldInfo := getFieldInfo? env structName fieldName - | throwError "(withStructField internal error) no such field '{fieldName}' of '{.ofConstName structName}'" + | throwError "Internal error in withStructField: No such field `{fieldName}` of `{.ofConstName structName}`" if let some _ := fieldInfo.subobject? then -- It's a subobject field, add it and its fields withStruct view (structName :: sourceStructNames) (binfo := fieldInfo.binderInfo) @@ -601,10 +641,10 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis else if let some existingField ← findFieldInfo? fieldName then -- It's a pre-existing field, make sure it is compatible (unless diamonds are not allowed) if structureDiamondWarning.get (← getOptions) then - logWarning m!"field '{fieldName}' from '{.ofConstName structName}' has already been declared" + logWarning m!"Field `{fieldName}` from `{.ofConstName structName}` has already been declared" let existingFieldType ← inferType existingField.fvar unless (← isDefEq fieldType existingFieldType) do - throwError "field type mismatch, field '{fieldName}' from parent '{.ofConstName structName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" + throwError "Field type mismatch: Field `{fieldName}` from parent `{.ofConstName structName}` {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" if let some d ← getFieldDefault? structName params fieldName then addFieldInheritedDefault fieldName structName d k existingField.fvar @@ -715,15 +755,15 @@ private partial def withStruct (view : StructView) (sourceStructNames : List Nam if ← isDefEq infoType structType then k info else - throwError "parent type mismatch, {← mkHasTypeButIsExpectedMsg structType infoType}" + throwError "Parent type mismatch: {← mkHasTypeButIsExpectedMsg structType infoType}" else - throwErrorAt projRef "{fieldFromMsg info} has a name conflict with parent projection for '{.ofConstName structName}'\n\n\ - The 'toParent : P' syntax can be used to adjust the name for the parent projection" + throwErrorAt projRef m!"{fieldFromMsg info} has a name conflict with parent projection for `{.ofConstName structName}`" + ++ .hint' "The `toParent : P` syntax can be used to adjust the name for the parent projection" else if let some info ← findParentFieldInfo? structName then -- The field name is different. Error. assert! structFieldName != info.name - throwErrorAt projRef "expecting '{structFieldName}' to match {fieldFromMsg info} for parent '{.ofConstName structName}'\n\n\ - The 'toParent : P' syntax can be used to adjust the name for the parent projection" + throwErrorAt projRef m!"Expected `{structFieldName}` to match {fieldFromMsg info} for parent `{.ofConstName structName}`" + ++ .hint' "The `toParent : P` syntax can be used to adjust the name for the parent projection" else -- Main case: there is no field named `structFieldName` and there is no field for the structure `structName` yet. @@ -734,8 +774,8 @@ private partial def withStruct (view : StructView) (sourceStructNames : List Nam let withStructFields' (kind : StructFieldKind) (inSubobject? : Option Expr) (k : StructFieldInfo → StructElabM α) : StructElabM α := do withStructFields view sourceStructNames structType inSubobject? fun structVal => do if let some _ ← findFieldInfo? structFieldName then - throwErrorAt projRef "field '{structFieldName}' has already been declared\n\n\ - The 'toParent : P' syntax can be used to adjust the name for the parent projection" + throwErrorAt projRef m!"Field `{structFieldName}` has already been declared" + ++ .hint' "The `toParent : P` syntax can be used to adjust the name for the parent projection" -- Add default values. -- We've added some default values so far, but we want all overridden default values, -- which for inherited fields might not have been seen yet. @@ -825,24 +865,24 @@ where Term.synthesizeSyntheticMVarsNoPostponing let parentType ← whnf parentType if parentType.getAppFn == indFVar then - logWarning "structure extends itself, skipping" + logWarning "Structure extends itself; skipping" return ← go (i + 1) if rs.any (fun r => r.indFVar == parentType.getAppFn) then - throwError "structure cannot extend types defined in the same mutual block" + throwError "Structure cannot extend types defined in the same mutual block" let parentStructName ← try getStructureName parentType catch ex => - throwErrorAt parentView.type "{ex.toMessageData}\n\n\ - This error is possibly due to a change in the 'structure' syntax. \ - Now the syntax is 'structure S : Type extends P' rather than 'structure S extends P' : Type'.\n\n\ - The purpose of the change is to accommodate 'structure S extends toP : P' syntax for naming parent projections." + throwErrorAt parentView.type ex.toMessageData + ++ .hint' "This error is possibly due to a change in the `structure` syntax. \ + Now the syntax is `structure S : Type extends P` rather than `structure S extends P : Type`.\n\n\ + The purpose of the change is to accommodate `structure S extends toP : P` syntax for naming parent projections." let (rawToParentName, toParentName) := parentView.mkToParentNames parentStructName if (← get).parents.any (·.structName == parentStructName) then - logWarning m!"duplicate parent structure '{.ofConstName parentStructName}', skipping" + logWarning m!"Duplicate parent structure `{.ofConstName parentStructName}`; skipping" go (i + 1) else if (← get).parents.any (·.name == toParentName) then - throwError "field '{toParentName}' has already been declared\n\n\ - The 'toParent : P' syntax can be used to adjust the name for the parent projection" + throwError m!"Field `{toParentName}` has already been declared" + ++ .hint' "The `toParent : P` syntax can be used to adjust the name for the parent projection" else withParent view parentView.projRef rawToParentName toParentName parentType fun parentFieldInfo => do addParentInfo { @@ -859,11 +899,11 @@ where k private def registerFailedToInferFieldType (fieldName : Name) (e : Expr) (ref : Syntax) : TermElabM Unit := do - Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"failed to infer type of field '{.ofConstName fieldName}'" + Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"Failed to infer type of field `{.ofConstName fieldName}`" private def registerFailedToInferDefaultValue (fieldName : Name) (e : Expr) (ref : Syntax) : TermElabM Unit := do - Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"failed to infer default value for field '{.ofConstName fieldName}'" - Term.registerLevelMVarErrorExprInfo e ref m!"failed to infer universe levels in default value for field '{.ofConstName fieldName}'" + Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"Failed to infer default value for field `{.ofConstName fieldName}`" + Term.registerLevelMVarErrorExprInfo e ref m!"Failed to infer universe levels in default value for field `{.ofConstName fieldName}`" /-- Goes through all the natural mvars appearing in `e`, assigning any whose type is one of the inherited parents. @@ -939,8 +979,8 @@ private def elabParamInfoUpdates (structParams : Array Expr) (binders : Array Sy for decl in decls, id in ids do Term.addTermInfo' id decl.toExpr unless structParams.contains decl.toExpr do - throwErrorAt id m!"only parameters appearing in the declaration header may have their binders kinds be overridden\n\n\ - If this is not intended to be an override, use a binder with a type, for example '(x : _)'." + throwErrorAt id m!"Only parameters appearing in the declaration header may have their binders kinds be overridden" + ++ .hint' "If this is not intended to be an override, use a binder with a type: for example, `(x : _)`" overrides := overrides.insert decl.toExpr (id, bi) return (#[], overrides) @@ -966,7 +1006,7 @@ private def elabFieldTypeValue (structParams : Array Expr) (view : StructFieldVi let value ← mkLambdaFVars params value return (none, paramInfoOverrides, StructFieldDefault.optParam value) | some (.autoParam tacticStx) => - throwErrorAt tacticStx "invalid field declaration, type must be provided when auto-param tactic is used" + throwErrorAt tacticStx "Invalid field declaration: Type must be provided when auto-param tactic is used" | some typeStx => let type ← Term.elabType typeStx let type ← runStructElabM (init := state) <| solveParentMVars type @@ -1000,12 +1040,12 @@ where let view := views[i] withRef view.ref do if let some parent := (← get).parents.find? (·.name == view.name) then - throwError "field '{view.name}' has already been declared as a projection for parent '{.ofConstName parent.structName}'" + throwError "Field `{view.name}` has already been declared as a projection for parent `{.ofConstName parent.structName}`" match ← findFieldInfo? view.name with | none => let (type?, paramInfoOverrides, default?) ← elabFieldTypeValue structParams view match type?, default? with - | none, none => throwError "invalid field, type expected" + | none, none => throwError "Invalid field: Type expected" | some type, _ => withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do addFieldInfo { ref := view.nameId, sourceStructNames := [], @@ -1022,22 +1062,22 @@ where kind := StructFieldKind.newField } go (i+1) | none, some (.autoParam _) => - throwError "field '{view.name}' has an autoparam but no type" + throwError "Field `{view.name}` has an auto-param but no type" | some info => let updateDefaultValue : StructElabM α := do match view.default? with - | none => throwError "field '{view.name}' has been declared in parent structure" + | none => throwError "Field `{view.name}` has already been declared in a parent structure" | some (.optParam valStx) => if let some type := view.type? then - throwErrorAt type "omit field '{view.name}' type to set default value" + throwErrorAt type "Omit the type of field `{view.name}` to set its default value" else if info.default?.isSome then - throwError "field '{view.name}' new default value has already been set" + throwError "A new default value for field `{view.name}` has already been set in this structure" let mut valStx := valStx let (binders, paramInfoOverrides) ← elabParamInfoUpdates structParams view.binders.getArgs unless paramInfoOverrides.isEmpty do let params := MessageData.joinSep (paramInfoOverrides.toList.map (m!"{·.1}")) ", " - throwError "cannot override structure parameter binder kinds when overriding the default value: {params}" + throwError "Cannot override structure parameter binder kinds when overriding the default value: {params}" if binders.size > 0 then valStx ← `(fun $binders* => $valStx:term) let fvarType ← inferType info.fvar @@ -1049,12 +1089,12 @@ where go (i+1) | some (.autoParam tacticStx) => if let some type := view.type? then - throwErrorAt type "omit field '{view.name}' type to set auto-param tactic" + throwErrorAt type "Omit the type of field `{view.name}` to set its auto-param tactic" else if info.default?.isSome then - throwError "field '{view.name}' new default value has already been set" + throwError "A new default value for field `{view.name}` has already been set in this structure" if view.binders.getArgs.size > 0 then - throwErrorAt view.binders "invalid field, unexpected binders when setting auto-param tactic for inherited field" + throwErrorAt view.binders "Invalid field: Unexpected binders when setting auto-param tactic for inherited field" let name := mkAutoParamFnOfProjFn view.declName discard <| Term.declareTacticSyntax tacticStx name replaceFieldInfo { info with ref := view.nameId, default? := StructFieldDefault.autoParam (.const name []) } @@ -1062,9 +1102,17 @@ where if let some projFn := info.projFn? then Term.addTermInfo' view.ref (← mkConstWithLevelParams projFn) go (i+1) match info.kind with - | StructFieldKind.newField => throwError "field '{view.name}' has already been declared" + | StructFieldKind.newField => throwError "Field `{view.name}` has already been declared" | StructFieldKind.subobject n - | StructFieldKind.otherParent n => throwError "unexpected reference to parent field '{n}'" -- improve error message + | StructFieldKind.otherParent n => + -- If this were a parent projection, we'd have caught it in the initial check, so it must be a transitive parent + let parentMsgs := (← get).parents.map (m!"`{.ofConstName ·.structName}`") |>.toList + let inheritanceMsg := if let [parent] := parentMsgs then + m!"this structure's immediate parent {parent}" + else + m!"one of this structure's immediate parents {.orList parentMsgs}" + throwError m!"Field `{view.name}` has already been declared as a projection for an indirect parent structure `{.ofConstName n}`" + ++ .note m!"This projection was inherited from {inheritanceMsg}" | StructFieldKind.copiedField | StructFieldKind.fromSubobject => updateDefaultValue else @@ -1102,7 +1150,7 @@ private def mkCtorLCtx : StructElabM LocalContext := do if !field.kind.isInCtor then lctx := lctx.erase fvarId let some e ← pure field.projExpr? <||> fvarId.getValue? - | throwError "(mkCtorLCtx internal error) non-constructor field has no value" + | throwError "Internal error in mkCtorLCtx: Non-constructor field has no value" fvarMap ← insert fvarMap field e else -- Do replacements. @@ -1190,7 +1238,7 @@ private partial def checkResultingUniversesForFields (fieldInfos : Array StructF let type ← inferType info.fvar let v := (← instantiateLevelMVars (← getLevel type)).normalize unless u.geq v do - let msg := m!"invalid universe level for field '{info.name}', has type{indentExpr type}\n\ + let msg := m!"Invalid universe level for field `{info.name}`: Field has type{indentExpr type}\n\ at universe level{indentD v}\n\ which is not less than or equal to the structure's resulting universe level{indentD u}" throwErrorAt info.ref msg @@ -1202,7 +1250,7 @@ private def addProjections (params : Array Expr) (r : ElabHeaderResult) (fieldIn |>.mapM (fun info => do info.paramInfoOverrides.forM fun p (ref, _) => do unless params.contains p do - throwErrorAt ref "invalid parameter binder update, not a parameter" + throwErrorAt ref "Invalid parameter binder update: Not a parameter:{indentExpr p}" let paramInfoOverrides := params |>.map (fun param => info.paramInfoOverrides[param]?.map Prod.snd) |>.toList return { ref := info.ref, projName := info.declName, paramInfoOverrides }) mkProjections r.view.declName projDecls r.view.isClass @@ -1305,7 +1353,7 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace let value ← fieldNormalizeExpr value let value ← replaceIndFVars value withLCtx {} {} do trace[Elab.structure] "default value after abstraction:{indentExpr value}" - if value.hasFVar then withLCtx {} {} <| logError m!"(internal error) default value contains fvars{indentD value}" + if value.hasFVar then withLCtx {} {} <| logError m!"Internal error: Default value contains fvars{indentD value}" let type ← inferType value -- No need to compile the definition, since it is only used during elaboration. addDecl <| Declaration.defnDecl @@ -1395,7 +1443,7 @@ private def mkRemainingProjections (levelParams : List Name) (params : Array Exp -- TODO(kmill): if it is a direct parent, try adding the coercion function from the environment and use that instead of `val`. -- (This should be evaluated to see if it is a good idea.) else - throwError m!"(mkRemainingProjections internal error) {field.name} has no value" + throwError m!"Internal error in mkRemainingProjections: `{field.name}` has no value" let mut parentInfos := #[] for parent in (← get).parents do @@ -1422,10 +1470,10 @@ private def checkResolutionOrder (structName : Name) : TermElabM Unit := do for conflict in resolutionOrderResult.conflicts do let parentKind direct := if direct then "parent" else "indirect parent" let conflicts := conflict.conflicts.map fun (isDirect, name) => - m!"{parentKind isDirect} '{MessageData.ofConstName name}'" - defects := m!"- {parentKind conflict.isDirectParent} '{MessageData.ofConstName conflict.badParent}' \ + m!"{parentKind isDirect} `{MessageData.ofConstName name}`" + defects := m!"- {parentKind conflict.isDirectParent} `{MessageData.ofConstName conflict.badParent}` \ must come after {MessageData.andList conflicts.toList}" :: defects - logWarning m!"failed to compute strict resolution order:\n{MessageData.joinSep defects.reverse "\n"}" + logWarning m!"Failed to compute strict resolution order:\n{MessageData.joinSep defects.reverse "\n"}" /-- Adds each direct parent projection to a class as an instance, so long as the parent isn't an ancestor of the others. diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out index 49c6d6b856..5dc8748974 100644 --- a/tests/lean/1021.lean.expected.out +++ b/tests/lean/1021.lean.expected.out @@ -1,8 +1,8 @@ some { range := - { pos := { line := 194, column := 0 }, charUtf16 := 0, endPos := { line := 199, column := 31 }, + { pos := { line := 210, column := 0 }, charUtf16 := 0, endPos := { line := 215, column := 31 }, endCharUtf16 := 31 }, selectionRange := - { pos := { line := 194, column := 46 }, charUtf16 := 46, endPos := { line := 194, column := 58 }, + { pos := { line := 210, column := 46 }, charUtf16 := 46, endPos := { line := 210, column := 58 }, endCharUtf16 := 58 } } diff --git a/tests/lean/277b.lean.expected.out b/tests/lean/277b.lean.expected.out index c3aa9d6792..09e5a5904e 100644 --- a/tests/lean/277b.lean.expected.out +++ b/tests/lean/277b.lean.expected.out @@ -1,2 +1,3 @@ -277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor - List Point +277b.lean:8:10-8:16: error: Invalid `⟨...⟩` notation: The expected type `List Point` has more than one constructor + +Note: This notation can only be used when the expected type is an inductive type with a single constructor diff --git a/tests/lean/ctorUnivTooBig.lean.expected.out b/tests/lean/ctorUnivTooBig.lean.expected.out index 6fefc9febd..02a7607c59 100644 --- a/tests/lean/ctorUnivTooBig.lean.expected.out +++ b/tests/lean/ctorUnivTooBig.lean.expected.out @@ -1,35 +1,35 @@ -ctorUnivTooBig.lean:3:2-3:45: error: invalid universe level in constructor 'Bla.cons', parameter 'α' has type +ctorUnivTooBig.lean:3:2-3:45: error: Invalid universe level in constructor `Bla.cons`: Parameter `α` has type Type u at universe level u+2 which is not less than or equal to the inductive type's resulting universe level u+1 -ctorUnivTooBig.lean:7:2-7:25: error: invalid universe level in constructor 'Foo.mk', parameter 'α' has type +ctorUnivTooBig.lean:7:2-7:25: error: Invalid universe level in constructor `Foo.mk`: Parameter `α` has type Type at universe level 2 which is not less than or equal to the inductive type's resulting universe level 1 -ctorUnivTooBig.lean:12:2-12:34: error: invalid universe level in constructor 'Foo'.mk', parameter has type +ctorUnivTooBig.lean:12:2-12:34: error: Invalid universe level in constructor `Foo'.mk`: Parameter has type Sort (max u v) at universe level max (u+1) (v+1) which is not less than or equal to the inductive type's resulting universe level u+1 Ex1.Member.head.{u} {α : Type u} {a : α} {as : List α} : Member a (a :: as) -ctorUnivTooBig.lean:35:2-35:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'as' has type +ctorUnivTooBig.lean:35:2-35:27: error: Invalid universe level in constructor `Ex3.Member.head`: Parameter `as` has type List α at universe level u_1+1 which is not less than or equal to the inductive type's resulting universe level max (u+1) (v+1) -ctorUnivTooBig.lean:41:2-41:27: error: invalid universe level in constructor 'Ex4.Member.head', parameter 'as' has type +ctorUnivTooBig.lean:41:2-41:27: error: Invalid universe level in constructor `Ex4.Member.head`: Parameter `as` has type List α at universe level u_1+1 which is not less than or equal to the inductive type's resulting universe level u+2 -ctorUnivTooBig.lean:47:2-47:27: error: invalid universe level in constructor 'Ex5.Member.head', parameter 'as' has type +ctorUnivTooBig.lean:47:2-47:27: error: Invalid universe level in constructor `Ex5.Member.head`: Parameter `as` has type List α at universe level u_1+1 diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out index e4f5da1028..3370757350 100644 --- a/tests/lean/diamond1.lean.expected.out +++ b/tests/lean/diamond1.lean.expected.out @@ -1,4 +1,4 @@ -diamond1.lean:11:40-11:45: error: field type mismatch, field 'a' from parent 'Baz' has type +diamond1.lean:11:40-11:45: error: Field type mismatch: Field `a` from parent `Baz` has type α → α but is expected to have type α @@ -18,4 +18,4 @@ field notation resolution order: Foo, Bar, Baz def f : Nat → Foo Nat := fun x => { a := fun y => x + y, b := fun x1 x2 => x1 + x2, c := fun x_1 => x, d := x } -diamond1.lean:27:47-27:52: warning: field 'a' from 'Baz' has already been declared +diamond1.lean:27:47-27:52: warning: Field `a` from `Baz` has already been declared diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index 5b561e2db1..8e891babf1 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/tests/lean/inductive1.lean.expected.out @@ -1,26 +1,44 @@ -inductive1.lean:4:15-4:18: error: invalid resulting type, expecting 'Sort _' or an indexed family of sorts -inductive1.lean:12:0-12:19: error: invalid mutually inductive types, resulting universe mismatch, given +inductive1.lean:4:15-4:18: error: Invalid resulting type: Expected a sort or an indexed family of sorts + +Hint: Examples of valid sorts include `Type _`, `Sort _`, and `Prop` +inductive1.lean:12:0-12:19: error: Invalid mutually inductive types: The resulting type of this declaration Type -expected type +differs from a preceding one Prop -inductive1.lean:22:0-22:37: error: invalid mutually inductive types, resulting universe mismatch, given + +Note: All inductive types declared in the same `mutual` block must belong to the same type universe +inductive1.lean:22:0-22:37: error: Invalid mutually inductive types: The resulting type of this declaration Type v -expected type +differs from a preceding one Type u -inductive1.lean:31:0-31:41: error: invalid mutually inductive types, parameter 'x' has type + +Note: All inductive types declared in the same `mutual` block must belong to the same type universe +inductive1.lean:31:0-31:41: error: Invalid mutually inductive types: Parameter `x` has type Bool but is expected to have type Nat -inductive1.lean:40:0-40:30: error: invalid inductive type, number of parameters mismatch in mutually inductive datatypes -inductive1.lean:49:0-49:40: error: invalid mutually inductive types, binder annotation mismatch at parameter 'x' -inductive1.lean:59:0-59:45: error: invalid inductive type, universe parameters mismatch in mutually inductive datatypes +inductive1.lean:40:0-40:30: error: Invalid mutually inductive types: `T2` has 1 parameter(s), but the preceding type `T1` has 2 + +Note: All inductive types declared in the same `mutual` block must have the same parameters +inductive1.lean:49:0-49:40: error: Invalid mutually inductive types: Binder annotations for parameter `x` must match +inductive1.lean:59:0-59:45: error: Universe parameter mismatch in mutually inductive types: `T2` has universe parameters + `w2`, `v`, `u` +but the preceding declaration `T1` has + `w1`, `v`, `u` + +Note: All inductive declarations in the same `mutual` block must have the same universe level parameters inductive1.lean:69:2-69:5: error: 'Boo.T1.bla' has already been declared inductive1.lean:73:10-73:12: error: 'Boo.T1' has already been declared -inductive1.lean:80:0-80:27: error: invalid use of 'partial' in inductive declaration -inductive1.lean:81:0-81:33: error: invalid use of 'noncomputable' in inductive declaration +inductive1.lean:80:0-80:27: error: Invalid modifier: Inductive declarations cannot be marked as `partial` +inductive1.lean:81:0-81:33: error: Invalid modifier: Inductive declarations cannot be marked as `noncomputable` inductive1.lean:82:2-82:8: error: Cannot add attribute `[inline]`: Declaration `T1'` is not a definition -inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype -inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in mutually inductive datatypes +inductive1.lean:85:0-85:17: error: Constructor cannot be marked `private` because it is already in a `private` inductive datatype + +Hint: Remove `private` modifier from constructor + p̵r̵i̵v̵a̵t̵e̵ ̵mk +inductive1.lean:93:7-93:26: error: Invalid mutually inductive types: `T2` is unsafe, but `T1` is safe + +Note: Safe and unsafe inductive declarations cannot both occur in the same `mutual` block inductive1.lean:100:0-100:4: error: Missing resulting type for constructor 'T1.z2': Its resulting type must be specified because it is part of an inductive family declaration inductive1.lean:105:7-105:9: error: type expected, got (T1 : Nat → Type) diff --git a/tests/lean/inductiveUnivErrorMsg.lean.expected.out b/tests/lean/inductiveUnivErrorMsg.lean.expected.out index d72825661a..a743508cc3 100644 --- a/tests/lean/inductiveUnivErrorMsg.lean.expected.out +++ b/tests/lean/inductiveUnivErrorMsg.lean.expected.out @@ -1,18 +1,18 @@ -inductiveUnivErrorMsg.lean:1:0-3:27: error: resulting type is of the form +inductiveUnivErrorMsg.lean:1:0-3:27: error: Resulting type is of the form Type ?u but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using Type u_1 if the resulting universe level should be at the above universe level or higher. -Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form '?u+1'. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): +Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): u_1 ≤ ?u+1 -However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form 'Sort (_ + 1)' and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. -inductiveUnivErrorMsg.lean:5:0-7:29: error: resulting type is of the form +However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. +inductiveUnivErrorMsg.lean:5:0-7:29: error: Resulting type is of the form Type ?u but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using Type u_1 if the resulting universe level should be at the above universe level or higher. -Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form '?u+1'. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): +Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): u_1 ≤ ?u+1 -However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form 'Sort (_ + 1)' and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. +However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. diff --git a/tests/lean/invalidFieldName.lean.expected.out b/tests/lean/invalidFieldName.lean.expected.out index 482f01ab51..6d829c2c9b 100644 --- a/tests/lean/invalidFieldName.lean.expected.out +++ b/tests/lean/invalidFieldName.lean.expected.out @@ -1 +1 @@ -invalidFieldName.lean:3:2-3:4: error: invalid field name 'mk', it is equal to structure constructor name +invalidFieldName.lean:3:2-3:4: error: Invalid field name `mk`: This is the name of the structure constructor diff --git a/tests/lean/mvarAtDefaultValue.lean.expected.out b/tests/lean/mvarAtDefaultValue.lean.expected.out index be647d71bf..8a312701e0 100644 --- a/tests/lean/mvarAtDefaultValue.lean.expected.out +++ b/tests/lean/mvarAtDefaultValue.lean.expected.out @@ -1,4 +1,4 @@ -mvarAtDefaultValue.lean:5:7-5:8: error: failed to infer default value for field 'x' +mvarAtDefaultValue.lean:5:7-5:8: error: Failed to infer default value for field `x` mvarAtDefaultValue.lean:8:7-8:8: error: don't know how to synthesize placeholder context: x : Nat diff --git a/tests/lean/nonAtomicFieldName.lean.expected.out b/tests/lean/nonAtomicFieldName.lean.expected.out index 872b554274..b329cc2eaf 100644 --- a/tests/lean/nonAtomicFieldName.lean.expected.out +++ b/tests/lean/nonAtomicFieldName.lean.expected.out @@ -1 +1 @@ -nonAtomicFieldName.lean:2:2-2:5: error: invalid field name 'a.b', field names must be atomic +nonAtomicFieldName.lean:2:2-2:5: error: Invalid field name `a.b`: Field names must be atomic diff --git a/tests/lean/run/3467.lean b/tests/lean/run/3467.lean index d240bd4575..26a3726c5d 100644 --- a/tests/lean/run/3467.lean +++ b/tests/lean/run/3467.lean @@ -52,8 +52,8 @@ Example resolution order failure -/ /-- -warning: failed to compute strict resolution order: -- parent 'B' must come after parent 'D' +warning: Failed to compute strict resolution order: +- parent `B` must come after parent `D` --- trace: [Elab.structure.resolutionOrder] computed resolution order: [D', B, D, C, A] -/ diff --git a/tests/lean/run/4310.lean b/tests/lean/run/4310.lean index bfb2340d8b..4329b7a341 100644 --- a/tests/lean/run/4310.lean +++ b/tests/lean/run/4310.lean @@ -6,7 +6,7 @@ mutual end /-- -error: invalid mutually inductive types, parameter name mismatch 'x', expected 'inst✝' +error: Invalid mutually inductive types: Parameter names `x` and `inst✝` differ but were expected to match -/ #guard_msgs in mutual @@ -16,7 +16,7 @@ end /-- -error: invalid mutually inductive types, parameter name mismatch 'β', expected 'α' +error: Invalid mutually inductive types: Parameter names `β` and `α` differ but were expected to match -/ #guard_msgs in mutual @@ -35,7 +35,7 @@ error: unknown universe level 'u✝' --- error: unknown universe level 'u✝' --- -error: invalid mutually inductive types, parameter name mismatch 'β✝', expected 'α✝' +error: Invalid mutually inductive types: Parameter names `β✝` and `α✝` differ but were expected to match -/ #guard_msgs in gen_mutual diff --git a/tests/lean/run/5236.lean b/tests/lean/run/5236.lean index 764ef429a2..1765500cb3 100644 --- a/tests/lean/run/5236.lean +++ b/tests/lean/run/5236.lean @@ -5,7 +5,7 @@ set_option linter.deprecated true /-- -warning: 'inductive ... :=' has been deprecated in favor of 'inductive ... where'. +warning: `inductive ... :=` has been deprecated in favor of `inductive ... where` Note: This linter can be disabled with `set_option linter.deprecated false` -/ @@ -15,7 +15,7 @@ inductive DogSound' := | grr /-- -warning: structure ... :=' has been deprecated in favor of 'structure ... where'. +warning: `structure ... :=` has been deprecated in favor of `structure ... where`. Note: This linter can be disabled with `set_option linter.deprecated false` -/ @@ -24,7 +24,7 @@ structure S := (n : Nat) /-- -warning: class ... :=' has been deprecated in favor of 'class ... where'. +warning: `class ... :=` has been deprecated in favor of `class ... where`. Note: This linter can be disabled with `set_option linter.deprecated false` -/ diff --git a/tests/lean/run/6694.lean b/tests/lean/run/6694.lean index 029a5175db..c375ed12f1 100644 --- a/tests/lean/run/6694.lean +++ b/tests/lean/run/6694.lean @@ -72,9 +72,9 @@ end #guard_msgs in #check a.b /-- -error: cannot define an inductive type and a constructor with the same name 'Bar.foo' +error: Cannot define an inductive type and a constructor with the same name `Bar.foo` --- -error: cannot define an inductive type and a constructor with the same name 'Bar.foo' +error: Cannot define an inductive type and a constructor with the same name `Bar.foo` -/ #guard_msgs in mutual @@ -92,9 +92,9 @@ end #guard_msgs in #check Bar.foo.mk /-- -error: cannot define multiple inductive types with the same name 'Private' +error: Cannot define multiple inductive types with the same name `Private` --- -error: cannot define multiple inductive types with the same name 'Private' +error: Cannot define multiple inductive types with the same name `Private` -/ #guard_msgs in mutual @@ -110,9 +110,9 @@ end #guard_msgs in #check Private.mk /-- -error: cannot define an inductive type and a constructor with the same name 'PrivateConstructor.priv' +error: Cannot define an inductive type and a constructor with the same name `PrivateConstructor.priv` --- -error: cannot define an inductive type and a constructor with the same name 'PrivateConstructor.priv' +error: Cannot define an inductive type and a constructor with the same name `PrivateConstructor.priv` -/ #guard_msgs in mutual @@ -128,9 +128,9 @@ end #guard_msgs in #check PrivateConstructor.priv /-- -error: cannot define multiple constructors with the same name 'Baz.foo.mk' +error: Cannot define multiple constructors with the same name `Baz.foo.mk` --- -error: cannot define multiple constructors with the same name 'Baz.foo.mk' +error: Cannot define multiple constructors with the same name `Baz.foo.mk` -/ #guard_msgs in mutual @@ -148,9 +148,9 @@ end #guard_msgs in #check Baz.foo.mk /-- -error: cannot define multiple inductive types with the same name 'Foo' +error: Cannot define multiple inductive types with the same name `Foo` --- -error: cannot define multiple inductive types with the same name 'Foo' +error: Cannot define multiple inductive types with the same name `Foo` -/ #guard_msgs in mutual diff --git a/tests/lean/run/anonymous_ctor_error_msg.lean b/tests/lean/run/anonymous_ctor_error_msg.lean index a19e797a60..398876c8b5 100644 --- a/tests/lean/run/anonymous_ctor_error_msg.lean +++ b/tests/lean/run/anonymous_ctor_error_msg.lean @@ -24,8 +24,7 @@ let x6 := ⟨6⟩ Foo.sum [x1, x2, x3, x5, x6] /-- -error: invalid constructor ⟨...⟩, expected type must be an inductive type ⏎ - ?_ +error: Invalid `⟨...⟩` notation: The expected type of this term could not be determined --- info: let x1 := { n := 1 }; let x2 := { n := 2 }; diff --git a/tests/lean/run/ctorFieldVisibilityHints.lean b/tests/lean/run/ctorFieldVisibilityHints.lean new file mode 100644 index 0000000000..7061b13661 --- /dev/null +++ b/tests/lean/run/ctorFieldVisibilityHints.lean @@ -0,0 +1,75 @@ +module +/-! +# Visibility hints for fields and constructors + +This test assess error message hints for fields and constructors with invalid visibilities where the +necessary correction is reasonably unambiguous. +-/ + +/-- +error: Constructor must be `private` because one or more of this structure's fields are `private` + +Hint: Mark constructor as `private` + p̵r̵o̵t̵e̵c̵t̵e̵d̵p̲r̲i̲v̲a̲t̲e̲ mk :: +-/ +#guard_msgs in +structure Foo where + protected mk :: + private foo : Nat + +/-- +error: Constructor must be `private` because one or more of this structure's fields are `private` + +Hint: Mark constructor as `private` + p̲r̲i̲v̲a̲t̲e̲ ̲mk :: +-/ +#guard_msgs in +structure Foo where + /-- doc -/ + mk :: + private foo : Nat + +/-- +error: Constructor must be `private` because one or more of this structure's fields are `private` + +Hint: Mark constructor as `private` + p̲r̲i̲v̲a̲t̲e̲ ̲mk :: +-/ +#guard_msgs in +structure Foo where + mk :: + private foo : Nat + +/-- +error: Field cannot be marked `private` because it is already in a `private` structure + +Hint: Remove `private` modifier from field + p̵r̵i̵v̵a̵t̵e̵ ̵bar : Nat +-/ +#guard_msgs in +private structure Bar where + private bar : Nat + +/-- +error: Constructor cannot be marked `private` because it is already in a `private` structure + +Hint: Remove `private` modifier from constructor + p̵r̵i̵v̵a̵t̵e̵ ̵mk :: +-/ +#guard_msgs in +private structure Bar' where + /-- doc -/ + private mk :: + bar' : Nat + +/-- +error: Duplicate doc string +--- +error: Constructor cannot be marked `private` because it is already in a `private` inductive datatype + +Hint: Remove `private` modifier from constructor + p̵r̵i̵v̵a̵t̵e̵ ̵baz +-/ +#guard_msgs in +private inductive Baz where + /-- doc -/ | /-- doc -/ private baz (x : Nat) : Baz diff --git a/tests/lean/run/inductive_univ.lean b/tests/lean/run/inductive_univ.lean index d46849a839..3279943b28 100644 --- a/tests/lean/run/inductive_univ.lean +++ b/tests/lean/run/inductive_univ.lean @@ -33,7 +33,7 @@ inductive T3 : Prop where Given the resultant type, fail to infer a level for `PUnit` if there's not a unique solution. -/ /-- -error: invalid universe level in constructor 'E0.mk', parameter 'x' has type +error: Invalid universe level in constructor `E0.mk`: Parameter `x` has type PUnit.{u_1} at universe level u_1 @@ -48,7 +48,7 @@ inductive E0 : Type where Given the resultant type, fail to infer a level for `PUnit` if there's not a unique solution. -/ /-- -error: invalid universe level in constructor 'E1.mk', parameter 'x' has type +error: Invalid universe level in constructor `E1.mk`: Parameter `x` has type Prod.{u_1, u_2} PUnit.{u_1 + 1} PUnit.{u_2 + 1} at universe level max (u_1+1) (u_2+1) @@ -63,9 +63,10 @@ inductive E1 : Type 1 where `Sort` polymorphism is not allowed. -/ /-- -error: invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values: +error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values: Sort u -Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'. + +Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _` -/ #guard_msgs in inductive P (α : Sort u) : Sort u where @@ -75,7 +76,7 @@ inductive P (α : Sort u) : Sort u where Errors for `structure` are specialized to talking about fields. -/ /-- -error: invalid universe level for field 'α', has type +error: Invalid universe level for field `α`: Field has type Type at universe level 2 @@ -93,7 +94,7 @@ Errors for `structure` talk about parent projection fields too. structure A' where α : Type /-- -error: invalid universe level for field 'α', has type +error: Invalid universe level for field `α`: Field has type Type at universe level 2 diff --git a/tests/lean/run/structBinderUpdates.lean b/tests/lean/run/structBinderUpdates.lean index 3e3f8a2a43..00a6774274 100644 --- a/tests/lean/run/structBinderUpdates.lean +++ b/tests/lean/run/structBinderUpdates.lean @@ -104,9 +104,9 @@ namespace Ex4 variable (α : Type) /-- -error: only parameters appearing in the declaration header may have their binders kinds be overridden +error: Only parameters appearing in the declaration header may have their binders kinds be overridden -If this is not intended to be an override, use a binder with a type, for example '(x : _)'. +Hint: If this is not intended to be an override, use a binder with a type: for example, `(x : _)` -/ #guard_msgs in class Inhabited where @@ -170,9 +170,9 @@ structure WithLp (p : Nat) (V : Type) where toLp (p : _) :: variable (n : Nat) /-- -error: only parameters appearing in the declaration header may have their binders kinds be overridden +error: Only parameters appearing in the declaration header may have their binders kinds be overridden -If this is not intended to be an override, use a binder with a type, for example '(x : _)'. +Hint: If this is not intended to be an override, use a binder with a type: for example, `(x : _)` -/ #guard_msgs in structure WithLp (p : Nat) (V : Type) where toLp (n) :: @@ -185,9 +185,9 @@ Motivation 2: we should be able to tell whether the param binder update is legit Motivation 3: the constructor type is constructed before we know which `variable`s will be included. That would take participation of MutualInductive. -/ /-- -error: only parameters appearing in the declaration header may have their binders kinds be overridden +error: Only parameters appearing in the declaration header may have their binders kinds be overridden -If this is not intended to be an override, use a binder with a type, for example '(x : _)'. +Hint: If this is not intended to be an override, use a binder with a type: for example, `(x : _)` -/ #guard_msgs in structure WithLp (p : Nat) (V : Type) where toLp (n) :: diff --git a/tests/lean/run/structNamedParentProj.lean b/tests/lean/run/structNamedParentProj.lean index b3d1883af0..d3528e6642 100644 --- a/tests/lean/run/structNamedParentProj.lean +++ b/tests/lean/run/structNamedParentProj.lean @@ -12,16 +12,16 @@ structure U where /-! Non-atomic parent projections are not allowed. -/ -/-- error: invalid parent projection name 'non.atomic', names must be atomic -/ +/-- error: Invalid parent projection name `non.atomic`: Name must be atomic -/ #guard_msgs in structure S' extends non.atomic : S /-! Shadowing other fields is not allowed. -/ /-- -error: field 'x' has already been declared +error: Field `x` has already been declared -The 'toParent : P' syntax can be used to adjust the name for the parent projection +Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends x : S @@ -29,9 +29,9 @@ The 'toParent : P' syntax can be used to adjust the name for the parent projecti Duplicate parent projections -/ /-- -error: field 'toP' has already been declared +error: Field `toP` has already been declared -The 'toParent : P' syntax can be used to adjust the name for the parent projection +Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends toP : S, toP : T @@ -41,9 +41,9 @@ Duplicate parent projections because from different namespaces structure NS1.S structure NS2.S /-- -error: field 'toS' has already been declared +error: Field `toS` has already been declared -The 'toParent : P' syntax can be used to adjust the name for the parent projection +Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends NS1.S, NS2.S @@ -51,15 +51,15 @@ The 'toParent : P' syntax can be used to adjust the name for the parent projecti Duplicate parent projections, when there are overlapping fields -/ /-- -error: field 'toS' has already been declared +error: Field `toS` has already been declared -The 'toParent : P' syntax can be used to adjust the name for the parent projection +Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends S, toS : U /-- -error: field 'toP' has already been declared +error: Field `toP` has already been declared -The 'toParent : P' syntax can be used to adjust the name for the parent projection +Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends toP : S, toP : T @@ -69,19 +69,33 @@ Duplicate parent projections because from different namespaces, when there are d structure NS1.S' where x : Nat structure NS2.S' where x : Nat /-- -error: field 'toS'' has already been declared +error: Field `toS'` has already been declared -The 'toParent : P' syntax can be used to adjust the name for the parent projection +Hint: The `toParent : P` syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends NS1.S', NS2.S' /-! Field conflicts with projection -/ -/-- error: field 'toS' has already been declared as a projection for parent 'S' -/ +/-- error: Field `toS` has already been declared as a projection for parent `S` -/ #guard_msgs in structure S' extends S where toS : Nat +/-! +Field conflicts with indirect parent projection +-/ +structure GP where +structure P extends toGP : GP where +/-- +error: Field `toGP` has already been declared as a projection for an indirect parent structure `GP` + +Note: This projection was inherited from this structure's immediate parent `P` +-/ +#guard_msgs in +structure C extends P where + toGP : Unit + /-! Checking that the projection name is honored. -/ diff --git a/tests/lean/run/structureElab.lean b/tests/lean/run/structureElab.lean index 10b4140049..0a49f85cc3 100644 --- a/tests/lean/run/structureElab.lean +++ b/tests/lean/run/structureElab.lean @@ -454,36 +454,36 @@ Some failures from unsupported autoparams -/ namespace TestFail1 -/-- error: invalid field declaration, type must be provided when auto-param tactic is used -/ +/-- error: Invalid field declaration: Type must be provided when auto-param tactic is used -/ #guard_msgs in structure F1 where x := by exact 0 structure F2 where x (n : Nat) : Nat -/-- error: omit field 'x' type to set auto-param tactic -/ +/-- error: Omit the type of field `x` to set its auto-param tactic -/ #guard_msgs in structure F3 extends F2 where x : Nat → Nat := by exact 0 -/-- error: invalid field, unexpected binders when setting auto-param tactic for inherited field -/ +/-- error: Invalid field: Unexpected binders when setting auto-param tactic for inherited field -/ #guard_msgs in structure F4 extends F2 where x (n : Nat) := by exact 0 -/-- error: field 'x' new default value has already been set -/ +/-- error: A new default value for field `x` has already been set in this structure -/ #guard_msgs in structure F5 extends F2 where x := by exact 0 x := by exact 0 -/-- error: field 'x' new default value has already been set -/ +/-- error: A new default value for field `x` has already been set in this structure -/ #guard_msgs in structure F6 extends F2 where x := id x := by exact 0 -/-- error: field 'x' new default value has already been set -/ +/-- error: A new default value for field `x` has already been set in this structure -/ #guard_msgs in structure F7 extends F2 where x := by exact 0 diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index 5fd3cd75f0..48d69c7e51 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -1,33 +1,38 @@ -struct1.lean:9:14-9:17: error: invalid resulting type, expecting 'Type _' or 'Prop' +struct1.lean:9:14-9:17: error: Invalid resulting type: Expected a sort + +Hint: Examples of valid sorts include `Type _`, `Sort _`, and `Prop` struct1.lean:12:20-12:29: error: expected structure -This error is possibly due to a change in the 'structure' syntax. Now the syntax is 'structure S : Type extends P' rather than 'structure S extends P' : Type'. +Hint: This error is possibly due to a change in the `structure` syntax. Now the syntax is `structure S : Type extends P` rather than `structure S extends P : Type`. -The purpose of the change is to accommodate 'structure S extends toP : P' syntax for naming parent projections. -struct1.lean:15:28-15:33: warning: field 'x' from 'B' has already been declared -struct1.lean:16:1-16:2: error: field 'x' has been declared in parent structure -struct1.lean:17:30-17:35: warning: duplicate parent structure 'A', skipping -struct1.lean:19:27-19:33: error: field type mismatch, field 'x' from parent 'B' has type +The purpose of the change is to accommodate `structure S extends toP : P` syntax for naming parent projections. +struct1.lean:15:28-15:33: warning: Field `x` from `B` has already been declared +struct1.lean:16:1-16:2: error: Field `x` has already been declared in a parent structure +struct1.lean:17:30-17:35: warning: Duplicate parent structure `A`; skipping +struct1.lean:19:27-19:33: error: Field type mismatch: Field `x` from parent `B` has type Bool but is expected to have type Nat -struct1.lean:30:1-30:2: error: field 'x' has already been declared -struct1.lean:33:1-33:2: error: field 'x' has been declared in parent structure +struct1.lean:30:1-30:2: error: Field `x` has already been declared +struct1.lean:33:1-33:2: error: Field `x` has already been declared in a parent structure struct1.lean:36:6-36:10: error: type mismatch true has type Bool but is expected to have type Nat -struct1.lean:39:5-39:9: error: omit field 'x' type to set default value +struct1.lean:39:5-39:9: error: Omit the type of field `x` to set its default value struct1.lean:42:12-42:16: error: type mismatch true has type Bool but is expected to have type Nat -struct1.lean:45:0-45:13: error: invalid 'private' constructor in a 'private' structure -struct1.lean:48:0-48:15: error: invalid 'protected' constructor in a 'private' structure -struct1.lean:51:0-51:19: error: invalid 'protected' field in a 'private' structure +struct1.lean:45:0-45:13: error: Constructor cannot be marked `private` because it is already in a `private` structure + +Hint: Remove `private` modifier from constructor + p̵r̵i̵v̵a̵t̵e̵ ̵mk :: +struct1.lean:48:0-48:15: error: Constructor cannot be `protected` because this structure is `private` +struct1.lean:51:0-51:19: error: Field cannot be marked `protected` because this structure is `private` S : Type S.mk2 (x : Nat) : S diff --git a/tests/lean/structDefValueOverride.lean.expected.out b/tests/lean/structDefValueOverride.lean.expected.out index 2ad385abde..ef2bd4f2ff 100644 --- a/tests/lean/structDefValueOverride.lean.expected.out +++ b/tests/lean/structDefValueOverride.lean.expected.out @@ -1 +1 @@ -structDefValueOverride.lean:6:2-6:3: error: field 'x' new default value has already been set +structDefValueOverride.lean:6:2-6:3: error: A new default value for field `x` has already been set in this structure diff --git a/tests/lean/univInference.lean.expected.out b/tests/lean/univInference.lean.expected.out index 7600593dc2..7e6a36532b 100644 --- a/tests/lean/univInference.lean.expected.out +++ b/tests/lean/univInference.lean.expected.out @@ -1,30 +1,33 @@ -univInference.lean:25:48-25:54: error: resulting type is of the form +univInference.lean:25:48-25:54: error: Resulting type is of the form Type ?u but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using Sort (max (max 1 u) v) if the resulting universe level should be at the above universe level or higher. -Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form '?u+1'. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): +Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): u ≤ ?u+1 v ≤ ?u+1 -However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form 'Sort (_ + 1)' and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. +However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1)) -univInference.lean:45:48-45:62: error: invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values: +univInference.lean:45:48-45:62: error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values: Sort (max u v) -Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'. -univInference.lean:64:48-64:54: error: resulting type is of the form + +Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _` +univInference.lean:64:48-64:54: error: Resulting type is of the form Type ?u but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using Sort (max (max 1 u) v) if the resulting universe level should be at the above universe level or higher. -Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form '?u+1'. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): +Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): u ≤ ?u+1 v ≤ ?u+1 -However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form 'Sort (_ + 1)' and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. -univInference.lean:73:48-73:62: error: invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values: +However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. +univInference.lean:73:48-73:62: error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values: Sort (max u v) -Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'. -univInference.lean:81:48-81:62: error: invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values: + +Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _` +univInference.lean:81:48-81:62: error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values: Sort (max u v) -Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'. + +Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _` diff --git a/tests/pkg/prv/Prv.lean b/tests/pkg/prv/Prv.lean index 995b87e8e8..c85038b692 100644 --- a/tests/pkg/prv/Prv.lean +++ b/tests/pkg/prv/Prv.lean @@ -22,7 +22,7 @@ error: overloaded, errors ⏎ #guard_msgs in def m1 : Name "hello" := {} -/-- error: invalid ⟨...⟩ notation, constructor for `Name` is marked as private -/ +/-- error: Invalid `⟨...⟩` notation: Constructor for `Name` is marked as private -/ #guard_msgs in def m2 : Name "hello" := ⟨"hello"⟩