display constant with unverse levels at error

src/Lean/Elab/Level.lean

@@ -17,7 +17,7 @@ namespace Term
 There are two kinds of errors -/
 inductive LevelMVarErrorKind where
   /-- Metavariable for a universe level parameter of a constant that hasn't been given explicitly -/
-  | ofConst (constantName levelName : Name)
+  | ofConst (levelName : Name) (const : Expr)
   /-- Metavariable for an explicit hole provided by the user (`_`) -/
   | hole
 

src/Lean/Elab/Term.lean

@@ -646,8 +646,8 @@ def withMacroExpansion (beforeStx afterStx : Syntax) (x : TermElabM α) : TermEl
   withMacroExpansionInfo beforeStx afterStx do
     withPushMacroExpansionStack beforeStx afterStx x
 
-def registerLevelMVarOfConstErrorInfo (mvarId : LMVarId) (ref : Syntax) (constantName levelName : Name) : TermElabM Unit :=
-  modify fun s => { s with levelMVarErrorInfos := { mvarId, ref, kind := .ofConst constantName levelName } :: s.levelMVarErrorInfos }
+def registerLevelMVarOfConstErrorInfo (mvarId : LMVarId) (ref : Syntax) (levelName : Name) (const : Expr) : TermElabM Unit :=
+  modify fun s => { s with levelMVarErrorInfos := { mvarId, ref, kind := .ofConst levelName const } :: s.levelMVarErrorInfos }
 
 /--
   Add the given metavariable to the list of pending synthetic metavariables.
@@ -722,8 +722,8 @@ def LevelMVarErrorInfo.logError (levelMVarErrorInfo : LevelMVarErrorInfo) (extra
   | .hole =>
     let msg := m! "don't know how to synthesize universe level placeholder {Level.mvar levelMVarErrorInfo.mvarId}"
     logErrorAt levelMVarErrorInfo.ref (appendExtra msg)
-  | .ofConst constName levelName =>
-    let msg := m! "don't know how to synthesize universe level parameter {levelName} of '{constName}'"
+  | .ofConst levelName const =>
+    let msg := m! "don't know how to synthesize universe level parameter {levelName} of '{const.constName!}'{indentD const}"
     logErrorAt levelMVarErrorInfo.ref (appendExtra msg)
 where
   appendExtra (msg : MessageData) : MessageData :=
@@ -1840,11 +1840,11 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM E
     throwError "too many explicit universe levels for '{constName}'"
   else
     let missingLevels := cinfo.levelParams.drop explicitLevels.length
-    let us ← missingLevels.reverse.mapM fun levelName => do
-      let u ← mkFreshLevelMVar
-      registerLevelMVarOfConstErrorInfo u.mvarId! (← getRef) constName levelName
-      pure u
-    return Lean.mkConst constName (explicitLevels ++ us.reverse)
+    let us ← mkFreshLevelMVars missingLevels.length
+    let const := Lean.mkConst constName (explicitLevels ++ us)
+    for u in us, levelName in missingLevels do
+      registerLevelMVarOfConstErrorInfo u.mvarId! (← getRef) levelName const
+    return const
 
 private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do

tests/lean/univErrorMessages.lean.expected.out

@@ -0,0 +1,57 @@
+univErrorMessages.lean:7:6-7:7: error: failed to infer 'let' declaration type
+univErrorMessages.lean:6:11-6:14: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+⊢ Type ?u
+univErrorMessages.lean:7:11-7:13: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+x : Array ?m := #[]
+⊢ Type ?u
+univErrorMessages.lean:6:11-6:14: error: don't know how to synthesize implicit argument
+  @List.toArray ?m []
+context:
+⊢ Type ?u
+univErrorMessages.lean:6:6-6:7: error: failed to infer 'let' declaration type
+univErrorMessages.lean:7:11-7:13: error: don't know how to synthesize universe level parameter u of 'List.nil'
+univErrorMessages.lean:6:11-6:14: error: don't know how to synthesize universe level parameter u of 'List.nil'
+univErrorMessages.lean:6:11-6:14: error: don't know how to synthesize universe level parameter u_1 of 'List.toArray'
+univErrorMessages.lean:11:25-11:28: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+⊢ Type ?u
+univErrorMessages.lean:12:21-12:22: error: don't know how to synthesize placeholder for argument 'α'
+context:
+x : Array ?m := #[]
+⊢ Type (?u + 1)
+univErrorMessages.lean:12:26-12:28: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+x : Array ?m := #[]
+⊢ Type (?u + 1)
+univErrorMessages.lean:11:20-11:21: error: don't know how to synthesize placeholder for argument 'α'
+context:
+⊢ Type ?u
+univErrorMessages.lean:11:25-11:28: error: don't know how to synthesize implicit argument
+  @List.toArray ?m []
+context:
+⊢ Type ?u
+univErrorMessages.lean:12:26-12:28: error: don't know how to synthesize universe level parameter u of 'List.nil'
+univErrorMessages.lean:12:16-12:17: error: don't know how to synthesize universe level placeholder ?u
+univErrorMessages.lean:11:25-11:28: error: don't know how to synthesize universe level parameter u of 'List.nil'
+univErrorMessages.lean:11:25-11:28: error: don't know how to synthesize universe level parameter u_1 of 'List.toArray'
+univErrorMessages.lean:11:17-11:18: error: don't know how to synthesize universe level placeholder ?u
+univErrorMessages.lean:16:21-16:38: error: don't know how to synthesize implicit argument
+  @id (Array ?m) { data := [] }
+context:
+⊢ Type ?u
+univErrorMessages.lean:16:34-16:36: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+⊢ Type ?u
+univErrorMessages.lean:16:16-16:17: error: don't know how to synthesize placeholder for argument 'α'
+context:
+⊢ Type ?u
+univErrorMessages.lean:16:34-16:36: error: don't know how to synthesize universe level parameter u of 'List.nil'
+univErrorMessages.lean:16:21-16:23: error: don't know how to synthesize universe level parameter u of 'id'
+univErrorMessages.lean:16:10-16:15: error: don't know how to synthesize universe level parameter u of 'Array'