feat: localize universe metavariable errors at let bindings and `fu…

…n` binders (#5402)

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

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

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}'"

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

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

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.

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

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

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