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.
This commit is contained in:
jrr6
GitHub
parent
5c2ae7b414
commit
fa1da03d50
28 changed files with 451 additions and 239 deletions
|
|
@ -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? =>
|
||||
|
|
|
|||
|
|
@ -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. -/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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 } }
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 };
|
||||
|
|
|
|||
75
tests/lean/run/ctorFieldVisibilityHints.lean
Normal file
75
tests/lean/run/ctorFieldVisibilityHints.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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) ::
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 _`
|
||||
|
|
|
|||
|
|
@ -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"⟩
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue