diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index ba46e151c1..9c880cdfbb 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -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 diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean index 3d52b625ed..eb311ffc5b 100644 --- a/src/Lean/Elab/DeclUtil.lean +++ b/src/Lean/Elab/DeclUtil.lean @@ -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}'" diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 360eefda63..43cd332792 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -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 diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 30bde73b2b..f654645f60 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -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 diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 137e8c05c8..471ad586ea 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -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. diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 714c57a01c..d04bab8342 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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 diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 04feb92519..cf7abcf1fd 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -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 diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean index b7ed2378f3..c49bb0e455 100644 --- a/src/Lean/Util.lean +++ b/src/Lean/Util.lean @@ -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 diff --git a/src/Lean/Util/CollectLevelMVars.lean b/src/Lean/Util/CollectLevelMVars.lean new file mode 100644 index 0000000000..140e70b46e --- /dev/null +++ b/src/Lean/Util/CollectLevelMVars.lean @@ -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 diff --git a/tests/lean/interactive/2058.lean b/tests/lean/interactive/2058.lean new file mode 100644 index 0000000000..5d2194c20a --- /dev/null +++ b/tests/lean/interactive/2058.lean @@ -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 diff --git a/tests/lean/interactive/2058.lean.expected.out b/tests/lean/interactive/2058.lean.expected.out new file mode 100644 index 0000000000..a790588354 --- /dev/null +++ b/tests/lean/interactive/2058.lean.expected.out @@ -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}}}]} diff --git a/tests/lean/run/2058.lean b/tests/lean/run/2058.lean new file mode 100644 index 0000000000..c869980691 --- /dev/null +++ b/tests/lean/run/2058.lean @@ -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 diff --git a/tests/lean/run/2226.lean b/tests/lean/run/2226.lean index ca9a89905f..810f37c18e 100644 --- a/tests/lean/run/2226.lean +++ b/tests/lean/run/2226.lean @@ -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