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

feat: localize universe metavariable errors at let bindings and fun binders (#5402)

Browse source 
Modifies how the declaration command elaborator reports when there are
unassigned metavariables. The visible effects are that (1) now errors
like "don't know how to synthesize implicit argument" and "failed to
infer 'let' declaration type" take precedence over universe level
issues, (2) universe level metavariables are reported as metavariables
(rather than as `u_1`, `u_2`, etc.), and (3) if the universe level
metavariables appear in `let` binding types or `fun` binder types, the
error is localized there.

Motivation: Reporting unsolved expression metavariables is more
important than universe level issues (typically universe issues are from
unsolved expression metavariables). Furthermore, `let` and `fun` binders
can't introduce universe polymorphism, so we can "blame" such bindings
for universe metavariables, if possible.

Example 1: Now the errors are on `x` and `none` (reporting expression
metavariables) rather than on `example` (which reported universe level
metavariables).
```lean
example : IO Unit := do
  let x := none
  pure ()
```

Example 2: Now there is a "failed to infer universe levels in 'let'
declaration type" error on `PUnit`.
```lean
def foo : IO Unit := do
  let x : PUnit := PUnit.unit
  pure ()
```


In more detail:
* `elabMutualDef` used to turn all level mvars into fresh level
parameters before doing an analysis for "hidden levels". This analysis
turns out to be exactly the same as instead creating fresh parameters
for level mvars in only pre-definitions' types and then looking for
level metavariables in their bodies. With this PR, error messages refer
to the same level metavariables in the Infoview, rather than obscure
generated `u_1`, `u_2`, ... level parameters.
* This PR made it possible to push the "hidden levels" check into
`addPreDefinitions`, after the checks for unassigned expression mvars.
It used to be that if the "hidden levels" check produced an "invalid
occurrence of universe level" error it would suppress errors for
unassigned expression mvars, and now it is the other way around.
* There is now a list of `LevelMVarErrorInfo` objects in the `TermElabM`
state. These record expressions that should receive a localized error if
they still contain level metavariables. Currently `let` expressions and
binder types in general register such info. Error messages make use of a
new `exposeLevelMVars` function that adds pretty printer annotations
that try to expose all universe level metavariables.
* When there are universe level metavariables, for error recovery the
definition is still added to the environment after assigning each
metavariable to level 0.
* There's a new `Lean.Util.CollectLevelMVars` module for collecting
level metavariables from expressions.

Closes #2058
This commit is contained in:
Kyle Miller 2024-09-23 22:30:42 -07:00 • committed by GitHub
parent b612403980
commit 8cc62940e0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
13 changed files with 373 additions and 59 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/Binders.lean
View file

@ -170,8 +170,9 @@ private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
else
throwUnsupportedSyntax
private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit := do
registerCustomErrorIfMVar type ref "failed to infer binder type"
registerLevelMVarErrorExprInfo type ref m!"failed to infer universe levels in binder type"
def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit :=
addTermInfo' (isBinder := true) stx fvar
@ -639,7 +640,7 @@ open Lean.Elab.Term.Quotation in
| _ => throwUnsupportedSyntax
/-- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
Otherwise, we create a term of the form `(fun (x : type) => body) val`
Otherwise, we create a term of the form `letFun val (fun (x : type) => body)`
The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`.
If `elabBodyFirst == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`. -/
@ -670,7 +671,9 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
Recall that TC resolution does **not** produce synthetic opaque metavariables.
-/
let type ← withSynthesize (postpone := .partial) <| elabType typeStx
registerCustomErrorIfMVar type typeStx "failed to infer 'let' declaration type"
let letMsg := if useLetExpr then "let" else "have"
registerCustomErrorIfMVar type typeStx m!"failed to infer '{letMsg}' declaration type"
registerLevelMVarErrorExprInfo type typeStx m!"failed to infer universe levels in '{letMsg}' declaration type"
if elabBodyFirst then
let type ← mkForallFVars fvars type
let val ← mkFreshExprMVar type

15
src/Lean/Elab/DeclUtil.lean
View file

@ -61,16 +61,17 @@ def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
(binders, typeSpec[1])
/--
Sort the given list of `usedParams` using the following order:
- If it is an explicit level `allUserParams`, then use user given order.
- Otherwise, use lexicographical.
Sort the given list of `usedParams` using the following order:
- If it is an explicit level in `allUserParams`, then use user-given order.
- All other levels come in lexicographic order after these.
Remark: `scopeParams` are the universe params introduced using the `universe` command. `allUserParams` contains
the universe params introduced using the `universe` command *and* the `.{...}` notation.
Remark: `scopeParams` are the universe params introduced using the `universe` command. `allUserParams` contains
the universe params introduced using the `universe` command *and* the `.{...}` notation.
Remark: this function return an exception if there is an `u` not in `usedParams`, that is in `allUserParams` but not in `scopeParams`.
Remark: this function return an exception if there is an `u` not in `usedParams`, that is in `allUserParams` but not in `scopeParams`.
Remark: `explicitParams` are in reverse declaration order. That is, the head is the last declared parameter. -/
Remark: `scopeParams` and `allUserParams` are in reverse declaration order. That is, the head is the last declared parameter.
-/
def sortDeclLevelParams (scopeParams : List Name) (allUserParams : List Name) (usedParams : Array Name) : Except String (List Name) :=
match allUserParams.find? fun u => !usedParams.contains u && !scopeParams.elem u with
| some u => throw s!"unused universe parameter '{u}'"

46
src/Lean/Elab/MutualDef.lean
View file

@ -98,7 +98,7 @@ private def isMultiConstant? (views : Array DefView) : Option (List Name) :=
else
none
private def getPendindMVarErrorMessage (views : Array DefView) : String :=
private def getPendingMVarErrorMessage (views : Array DefView) : String :=
match isMultiConstant? views with
| some ids =>
let idsStr := ", ".intercalate <| ids.map fun id => s!"`{id}`"
@ -196,7 +196,7 @@ private def elabHeaders (views : Array DefView)
if view.type?.isSome then
let pendingMVarIds ← getMVars type
discard <| logUnassignedUsingErrorInfos pendingMVarIds <|
getPendindMVarErrorMessage views
getPendingMVarErrorMessage views
let newHeader : DefViewElabHeaderData := {
declName, shortDeclName, type, levelNames, binderIds
numParams := xs.size
@ -947,45 +947,6 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
let newHeaders ← (process).run' 1
newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs : Array PreDefinition) : TermElabM Unit :=
unless (← MonadLog.hasErrors) do
-- We do not report this kind of error if the declaration already contains errors
let mut sTypes : CollectLevelParams.State := {}
let mut sValues : CollectLevelParams.State := {}
for preDef in preDefs do
sTypes := collectLevelParams sTypes preDef.type
sValues := collectLevelParams sValues preDef.value
if sValues.params.all fun u => sTypes.params.contains u || allUserLevelNames.contains u then
-- If all universe level occurring in values also occur in types or explicitly provided universes, then everything is fine
-- and we just return
return ()
let checkPreDef (preDef : PreDefinition) : TermElabM Unit :=
-- Otherwise, we try to produce an error message containing the expression with the offending universe
let rec visitLevel (u : Level) : ReaderT Expr TermElabM Unit := do
match u with
| .succ u => visitLevel u
| .imax u v | .max u v => visitLevel u; visitLevel v
| .param n =>
unless sTypes.visitedLevel.contains u || allUserLevelNames.contains n do
let parent ← withOptions (fun o => pp.universes.set o true) do addMessageContext m!"{indentExpr (← read)}"
let body ← withOptions (fun o => pp.letVarTypes.setIfNotSet (pp.funBinderTypes.setIfNotSet o true) true) do addMessageContext m!"{indentExpr preDef.value}"
throwError "invalid occurrence of universe level '{u}' at '{preDef.declName}', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression{parent}\nat declaration body{body}"
| _ => pure ()
let rec visit (e : Expr) : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit := do
checkCache { val := e : ExprStructEq } fun _ => do
match e with
| .forallE n d b c | .lam n d b c => visit d e; withLocalDecl n c d fun x => visit (b.instantiate1 x) e
| .letE n t v b _ => visit t e; visit v e; withLetDecl n t v fun x => visit (b.instantiate1 x) e
| .app .. => e.withApp fun f args => do visit f e; args.forM fun arg => visit arg e
| .mdata _ b => visit b e
| .proj _ _ b => visit b e
| .sort u => visitLevel u (← read)
| .const _ us => us.forM (visitLevel · (← read))
| _ => pure ()
visit preDef.value preDef.value |>.run {}
for preDef in preDefs do
checkPreDef preDef
def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
if isExample views then
withoutModifyingEnv do
@ -1021,13 +982,12 @@ where
let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
for preDef in preDefs do
trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs
let preDefs ← instantiateMVarsAtPreDecls preDefs
let preDefs ← shareCommonPreDefs preDefs
let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
for preDef in preDefs do
trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
checkForHiddenUnivLevels allUserLevelNames preDefs
addPreDefinitions preDefs
processDeriving headers
for view in views, header in headers do

16
src/Lean/Elab/PreDefinition/Basic.lean
View file

@ -39,14 +39,26 @@ structure PreDefinition where
def PreDefinition.filterAttrs (preDef : PreDefinition) (p : Attribute → Bool) : PreDefinition :=
{ preDef with modifiers := preDef.modifiers.filterAttrs p }
/--
Applies `Lean.instantiateMVars` to the types of values of each predefinition.
-/
def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
preDefs.mapM fun preDef => do
pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }
def levelMVarToParamPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
/--
Applies `Lean.Elab.Term.levelMVarToParam` to the types of each predefinition.
-/
def levelMVarToParamTypesPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
preDefs.mapM fun preDef => do
pure { preDef with type := (← levelMVarToParam preDef.type), value := (← levelMVarToParam preDef.value) }
pure { preDef with type := (← levelMVarToParam preDef.type) }
/--
Collects all the level parameters in sorted order from the types and values of each predefinition.
Throws an "unused universe parameter" error if there is an unused `.{...}` parameter.
See `Lean.collectLevelParams`.
-/
private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (List Name) := do
let mut s : CollectLevelParams.State := {}
for preDef in preDefs do

60
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -53,6 +53,64 @@ private def getMVarsAtPreDef (preDef : PreDefinition) : MetaM (Array MVarId) :=
let (_, s) ← (collectMVarsAtPreDef preDef).run {}
pure s.result
/--
Set any lingering level mvars to `.zero`, for error recovery.
-/
private def setLevelMVarsAtPreDef (preDef : PreDefinition) : PreDefinition :=
if preDef.value.hasLevelMVar then
let value' :=
preDef.value.replaceLevel fun l =>
match l with
| .mvar _ => levelZero
| _ => none
{ preDef with value := value' }
else
preDef
private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition) : TermElabM PreDefinition := do
if !preDef.value.hasLevelMVar then
return preDef
else
let pendingLevelMVars := (collectLevelMVars {} (← instantiateMVars preDef.value)).result
if (← logUnassignedLevelMVarsUsingErrorInfos pendingLevelMVars) then
return setLevelMVarsAtPreDef preDef
else if !(← MonadLog.hasErrors) then
-- This is a fallback in case we don't have an error info available for the universe level metavariables.
-- We try to produce an error message containing an expression with one of the universe level metavariables.
let rec visitLevel (u : Level) (e : Expr) : TermElabM Unit := do
if u.hasMVar then
let e' ← exposeLevelMVars e
throwError "\
declaration '{preDef.declName}' contains universe level metavariables at the expression\
{indentExpr e'}\n\
in the declaration body{indentExpr <| ← exposeLevelMVars preDef.value}"
let withExpr (e : Expr) (m : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit) :=
withReader (fun _ => e) m
let rec visit (e : Expr) (head := false) : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit := do
if e.hasLevelMVar then
checkCache { val := e : ExprStructEq } fun _ => do
match e with
| .forallE n d b c | .lam n d b c => withExpr e do visit d; withLocalDecl n c d fun x => visit (b.instantiate1 x)
| .letE n t v b _ => withExpr e do visit t; visit v; withLetDecl n t v fun x => visit (b.instantiate1 x)
| .mdata _ b => withExpr e do visit b
| .proj _ _ b => withExpr e do visit b
| .sort u => visitLevel u (← read)
| .const _ us => (if head then id else withExpr e) <| us.forM (visitLevel · (← read))
| .app .. => withExpr e do
if let some (args, n, t, v, b) := e.letFunAppArgs? then
visit t; visit v; withLocalDeclD n t fun x => visit (b.instantiate1 x); args.forM visit
else
e.withApp fun f args => do visit f true; args.forM visit
| _ => pure ()
try
visit preDef.value |>.run preDef.value |>.run {}
catch e =>
logException e
return setLevelMVarsAtPreDef preDef
throwAbortCommand
else
return setLevelMVarsAtPreDef preDef
private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM PreDefinition := do
let pendingMVarIds ← getMVarsAtPreDef preDef
if (← logUnassignedUsingErrorInfos pendingMVarIds) then
@ -62,7 +120,7 @@ private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM
else
throwAbortCommand
else
return preDef
ensureNoUnassignedLevelMVarsAtPreDef preDef
/--
Letrec declarations produce terms of the form `(fun .. => ..) d` where `d` is a (partial) application of an auxiliary declaration for a letrec declaration.

63
src/Lean/Elab/Term.lean
View file

@ -8,6 +8,7 @@ import Lean.ReservedNameAction
import Lean.Meta.AppBuilder
import Lean.Meta.CollectMVars
import Lean.Meta.Coe
import Lean.Util.CollectLevelMVars
import Lean.Linter.Deprecated
import Lean.Elab.Config
import Lean.Elab.Level
@ -93,6 +94,18 @@ structure MVarErrorInfo where
kind : MVarErrorKind
deriving Inhabited
/--
When reporting unexpected universe level metavariables, it is useful to localize the errors
to particular terms, especially at `let` bindings and function binders,
where universe polymorphism is not permitted.
-/
structure LevelMVarErrorInfo where
lctx : LocalContext
expr : Expr
ref : Syntax
msgData? : Option MessageData := none
deriving Inhabited
/--
Nested `let rec` expressions are eagerly lifted by the elaborator.
We store the information necessary for performing the lifting here.
@ -120,6 +133,8 @@ structure State where
pendingMVars : List MVarId := {}
/-- List of errors associated to a metavariable that are shown to the user if the metavariable could not be fully instantiated -/
mvarErrorInfos : List MVarErrorInfo := []
/-- List of data to be able to localize universe level metavariable errors to particular expressions. -/
levelMVarErrorInfos : List LevelMVarErrorInfo := []
/--
`mvarArgNames` stores the argument names associated to metavariables.
These are used in combination with `mvarErrorInfos` for throwing errors about metavariables that could not be fully instantiated.
@ -794,6 +809,54 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Op
error.logError extraMsg?
return hasNewErrors
def registerLevelMVarErrorInfo (levelMVarErrorInfo : LevelMVarErrorInfo) : TermElabM Unit :=
modify fun s => { s with levelMVarErrorInfos := levelMVarErrorInfo :: s.levelMVarErrorInfos }
def registerLevelMVarErrorExprInfo (expr : Expr) (ref : Syntax) (msgData? : Option MessageData := none) : TermElabM Unit := do
registerLevelMVarErrorInfo { lctx := (← getLCtx), expr, ref, msgData? }
def exposeLevelMVars (e : Expr) : MetaM Expr :=
Core.transform e
(post := fun e => do
match e with
| .const _ us => return .done <| if us.any (·.isMVar) then e.setPPUniverses true else e
| .sort u => return .done <| if u.isMVar then e.setPPUniverses true else e
| .lam _ t _ _ => return .done <| if t.hasLevelMVar then e.setOption `pp.funBinderTypes true else e
| .letE _ t _ _ _ => return .done <| if t.hasLevelMVar then e.setOption `pp.letVarTypes true else e
| _ => return .done e)
def LevelMVarErrorInfo.logError (levelMVarErrorInfo : LevelMVarErrorInfo) : TermElabM Unit :=
Meta.withLCtx levelMVarErrorInfo.lctx {} do
let e' ← exposeLevelMVars (← instantiateMVars levelMVarErrorInfo.expr)
let msg := levelMVarErrorInfo.msgData?.getD m!"don't know how to synthesize universe level metavariables"
let msg := m!"{msg}{indentExpr e'}"
logErrorAt levelMVarErrorInfo.ref msg
/--
Try to log errors for unassigned level metavariables `pendingLevelMVarIds`.
Returns `true` if there are any relevant `LevelMVarErrorInfo`s and we should "abort" the declaration.
Remark: we only log unassigned level metavariables as new errors if no error has been logged so far.
-/
def logUnassignedLevelMVarsUsingErrorInfos (pendingLevelMVarIds : Array LMVarId) : TermElabM Bool := do
if pendingLevelMVarIds.isEmpty then
return false
else
let hasOtherErrors ← MonadLog.hasErrors
let mut hasNewErrors := false
let mut errors : Array LevelMVarErrorInfo := #[]
for levelMVarErrorInfo in (← get).levelMVarErrorInfos do
let e ← instantiateMVars levelMVarErrorInfo.expr
let lmvars := (collectLevelMVars {} e).result
if lmvars.any pendingLevelMVarIds.contains then do
unless hasOtherErrors do
errors := errors.push levelMVarErrorInfo
hasNewErrors := true
for error in errors do
error.logError
return hasNewErrors
/-- Ensure metavariables registered using `registerMVarErrorInfos` (and used in the given declaration) have been assigned. -/
def ensureNoUnassignedMVars (decl : Declaration) : TermElabM Unit := do
let pendingMVarIds ← getMVarsAtDecl decl

6
src/Lean/Meta/Basic.lean
View file

@ -1766,7 +1766,7 @@ private def exposeRelevantUniverses (e : Expr) (p : Level → Bool) : Expr :=
| .sort u => if p u then some (e.setPPUniverses true) else none
| _ => none
private def mkLeveErrorMessageCore (header : String) (entry : PostponedEntry) : MetaM MessageData := do
private def mkLevelErrorMessageCore (header : String) (entry : PostponedEntry) : MetaM MessageData := do
match entry.ctx? with
| none =>
return m!"{header}{indentD m!"{entry.lhs} =?= {entry.rhs}"}"
@ -1783,10 +1783,10 @@ private def mkLeveErrorMessageCore (header : String) (entry : PostponedEntry) :
addMessageContext m!"{header}{indentD m!"{entry.lhs} =?= {entry.rhs}"}\nwhile trying to unify{indentD lhs}\nwith{indentD rhs}"
def mkLevelStuckErrorMessage (entry : PostponedEntry) : MetaM MessageData := do
mkLeveErrorMessageCore "stuck at solving universe constraint" entry
mkLevelErrorMessageCore "stuck at solving universe constraint" entry
def mkLevelErrorMessage (entry : PostponedEntry) : MetaM MessageData := do
mkLeveErrorMessageCore "failed to solve universe constraint" entry
mkLevelErrorMessageCore "failed to solve universe constraint" entry
private def processPostponedStep (exceptionOnFailure : Bool) : MetaM Bool := do
let ps ← getResetPostponed

1
src/Lean/Util.lean
View file

@ -7,6 +7,7 @@ prelude
import Lean.Util.CollectFVars
import Lean.Util.CollectLevelParams
import Lean.Util.CollectMVars
import Lean.Util.CollectLevelMVars
import Lean.Util.FindMVar
import Lean.Util.FindLevelMVar
import Lean.Util.MonadCache

62
src/Lean/Util/CollectLevelMVars.lean Normal file
View file

@ -0,0 +1,62 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
prelude
import Lean.Expr
namespace Lean
namespace CollectLevelMVars
structure State where
visitedLevel : LevelSet := {}
visitedExpr : ExprSet := {}
result : Array LMVarId := {}
instance : Inhabited State := ⟨{}⟩
abbrev Visitor := State → State
mutual
partial def visitLevel (u : Level) : Visitor := fun s =>
if !u.hasMVar || s.visitedLevel.contains u then s
else collect u { s with visitedLevel := s.visitedLevel.insert u }
partial def collect : Level → Visitor
| .succ v => visitLevel v
| .max u v => visitLevel v ∘ visitLevel u
| .imax u v => visitLevel v ∘ visitLevel u
| .mvar m => fun s => { s with result := s.result.push m }
| _ => id
end
mutual
partial def visitExpr (e : Expr) : Visitor := fun s =>
if !e.hasMVar then s
else if s.visitedExpr.contains e then s
else main e { s with visitedExpr := s.visitedExpr.insert e }
partial def main : Expr → Visitor
| .proj _ _ s => visitExpr s
| .forallE _ d b _ => visitExpr b ∘ visitExpr d
| .lam _ d b _ => visitExpr b ∘ visitExpr d
| .letE _ t v b _ => visitExpr b ∘ visitExpr v ∘ visitExpr t
| .app f a => visitExpr a ∘ visitExpr f
| .mdata _ b => visitExpr b
| .const _ us => us.foldl (fun s u => visitLevel u s)
| .sort u => visitLevel u
| _ => id
end
end CollectLevelMVars
/--
Collects all universe level metavariables present in `e`.
Result is in `Lean.CollectLevelMVars.State.result`.
-/
def collectLevelMVars (s : CollectLevelMVars.State) (e : Expr) : CollectLevelMVars.State :=
CollectLevelMVars.main e s
end Lean

31
tests/lean/interactive/2058.lean Normal file
View file

@ -0,0 +1,31 @@
/-!
# Localized error messages with unassigned metavariables
-/
set_option pp.mvars false
/-!
Test: now reports that the universe levels are not assigned at the 'let' rather than an error on the `example` command.
-/
def foo : IO Unit := do
let x : PUnit := PUnit.unit
--^ collectDiagnostics
pure ()
/-!
Test: Works for `fun` binders too.
-/
example : Nat := (fun x : PUnit => 2) PUnit.unit
--^ collectDiagnostics
/-!
Test: A failure not in a binder, right now reports an error on `example` since there's no other location information.
-/
example : Nat := Function.const _ 2 @id
--^ collectDiagnostics

32
tests/lean/interactive/2058.lean.expected.out Normal file
View file

@ -0,0 +1,32 @@
{"version": 1,
"uri": "file:///2058.lean",
"diagnostics":
[{"source": "Lean 4",
"severity": 1,
"range":
{"start": {"line": 12, "character": 10},
"end": {"line": 12, "character": 15}},
"message":
"failed to infer universe levels in 'let' declaration type\n PUnit.{_}",
"fullRange":
{"start": {"line": 12, "character": 10},
"end": {"line": 12, "character": 15}}},
{"source": "Lean 4",
"severity": 1,
"range":
{"start": {"line": 21, "character": 26},
"end": {"line": 21, "character": 31}},
"message": "failed to infer universe levels in binder type\n PUnit.{_}",
"fullRange":
{"start": {"line": 21, "character": 26},
"end": {"line": 21, "character": 31}}},
{"source": "Lean 4",
"severity": 1,
"range":
{"start": {"line": 29, "character": 0},
"end": {"line": 29, "character": 39}},
"message":
"declaration '_example' contains universe level metavariables at the expression\n Function.const ({α : Sort _} → α → α) 2 @id.{_}\nin the declaration body\n Function.const ({α : Sort _} → α → α) 2 @id.{_}",
"fullRange":
{"start": {"line": 29, "character": 0},
"end": {"line": 29, "character": 39}}}]}

87
tests/lean/run/2058.lean Normal file
View file

@ -0,0 +1,87 @@
/-!
# Localized error messages with unassigned metavariables
-/
set_option pp.mvars false
/-!
Test: now reports "don't know how to synthesize implicit argument" rather than an error on the `example` command.
-/
/--
error: don't know how to synthesize implicit argument 'α'
@none ?_
context:
⊢ Type _
---
error: failed to infer 'let' declaration type
-/
#guard_msgs in
example : IO Unit := do
let x := none
pure ()
/-!
Test: now reports that the universe levels are not assigned at the 'let' rather than an error on the `example` command.
-/
/--
error: failed to infer universe levels in 'let' declaration type
PUnit.{_}
-/
#guard_msgs in
def foo : IO Unit := do
let x : PUnit := PUnit.unit
pure ()
-- specializes to 0 on error
/--
info: def foo : IO Unit :=
let x := PUnit.unit.{0};
pure.{0, 0} Unit.unit
-/
#guard_msgs in set_option pp.universes true in #print foo
/-!
Test: Works for `have` too.
-/
/--
error: failed to infer universe levels in 'have' declaration type
PUnit.{_}
-/
#guard_msgs in
def foo' : IO Unit := do
have x : PUnit := PUnit.unit
pure ()
/-!
Test: Works for `fun` binders.
-/
/--
error: failed to infer universe levels in binder type
PUnit.{_}
-/
#guard_msgs in
example : Nat := (fun x : PUnit => 2) PUnit.unit
/-!
Test: A failure not in a binder, right now reports an error on `example`.
A change is that before the error was about level parameters rather than metavariables since
the def elaborator would turn all metavariables into parameters before this analysis.
-/
/--
error: declaration '_example' contains universe level metavariables at the expression
Function.const ({α : Sort _} → α → α) 2 @id.{_}
in the declaration body
Function.const ({α : Sort _} → α → α) 2 @id.{_}
-/
#guard_msgs in
example : Nat := Function.const _ 2 @id

4
tests/lean/run/2226.lean
View file

@ -6,8 +6,12 @@ A : Nat
#guard_msgs in
variable (A : Nat) (B : by skip)
/-- error: failed to infer definition type -/
#guard_msgs in
def foo :=
A = B
/-- warning: declaration uses 'sorry' -/
#guard_msgs in
def boo :=
B