fix: fixes #456

src/Lean/Elab/Term.lean

@@ -1619,6 +1619,7 @@ unsafe def evalExpr (α) (typeName : Name) (value : Expr) : TermElabM α :=
     evalConst α name
 
 private def throwStuckAtUniverseCnstr : TermElabM Unit := do
+  -- This code assumes `entries` is not empty. Note that `processPostponed` uses `exceptionOnFailure` to guarantee this property
   let entries ← getPostponed
   let mut found : Std.HashSet (Level × Level) := {}
   let mut uniqueEntries := #[]
@@ -1631,35 +1632,14 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do
       found := found.insert (lhs, rhs)
       uniqueEntries := uniqueEntries.push entry
   for i in [1:uniqueEntries.size] do
-    logErrorAt uniqueEntries[i].ref (← mkMessage uniqueEntries[i])
-  throwErrorAt uniqueEntries[0].ref (← mkMessage uniqueEntries[0])
-where
-  /- Annotate any constant and sort in `e` that satisfies `p` with `pp.universes true` -/
-  exposeRelevantUniverses (e : Expr) (p : Level → Bool) : Expr :=
-    e.replace fun e =>
-      match e with
-      | Expr.const _ us _ => if us.any p then some (e.setPPUniverses true) else none
-      | Expr.sort u _     => if p u then some (e.setPPUniverses true) else none
-      | _                 => none
-
-  mkMessage (entry : PostponedEntry) : TermElabM MessageData := do
-    match entry.ctx? with
-    | none =>
-      return m!"stuck at solving universe constraints{indentD m!"{entry.lhs} =?= {entry.rhs}"}"
-    | some ctx =>
-      withLCtx ctx.lctx ctx.localInstances do
-        let s   := entry.lhs.collectMVars entry.rhs.collectMVars
-        /- `p u` is true if it contains a universe metavariable in `s` -/
-        let p (u : Level) := u.any fun | Level.mvar m _ => s.contains m | _ => false
-        let lhs := exposeRelevantUniverses (← instantiateMVars ctx.lhs) p
-        let rhs := exposeRelevantUniverses (← instantiateMVars ctx.rhs) p
-        addMessageContext m!"stuck at solving universe constraints{indentD m!"{entry.lhs} =?= {entry.rhs}"}\nwhile trying to unify{indentD m!"{lhs} : {← inferType lhs}"}\nwith{indentD m!"{rhs} : {← inferType rhs}"}"
+    logErrorAt uniqueEntries[i].ref (← mkLevelStuckErrorMessage uniqueEntries[i])
+  throwErrorAt uniqueEntries[0].ref (← mkLevelStuckErrorMessage uniqueEntries[0])
 
 @[specialize] def withoutPostponingUniverseConstraints (x : TermElabM α) : TermElabM α := do
   let postponed ← getResetPostponed
   try
     let a ← x
-    unless (← processPostponed (mayPostpone := false)) do
+    unless (← processPostponed (mayPostpone := false) (exceptionOnFailure := true)) do
       throwStuckAtUniverseCnstr
     setPostponed postponed
     return a

src/Lean/Meta/LevelDefEq.lean

@@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.CollectMVars
+import Lean.Util.ReplaceExpr
 import Lean.Meta.Basic
 import Lean.Meta.InferType
 
@@ -168,15 +170,47 @@ def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do
   setPostponed {}
   return ps
 
-private def processPostponedStep : MetaM Bool :=
+/-- Annotate any constant and sort in `e` that satisfies `p` with `pp.universes true` -/
+private def exposeRelevantUniverses (e : Expr) (p : Level → Bool) : Expr :=
+  e.replace fun
+    | Expr.const _ us _ => if us.any p then some (e.setPPUniverses true) else none
+    | Expr.sort u _     => if p u then some (e.setPPUniverses true) else none
+    | _                 => none
+
+private def mkLeveErrorMessageCore (header : String) (entry : PostponedEntry) : MetaM MessageData := do
+  match entry.ctx? with
+  | none =>
+    return m!"{header}{indentD m!"{entry.lhs} =?= {entry.rhs}"}"
+  | some ctx =>
+    withLCtx ctx.lctx ctx.localInstances do
+      let s   := entry.lhs.collectMVars entry.rhs.collectMVars
+      /- `p u` is true if it contains a universe metavariable in `s` -/
+      let p (u : Level) := u.any fun | Level.mvar m _ => s.contains m | _ => false
+      let lhs := exposeRelevantUniverses (← instantiateMVars ctx.lhs) p
+      let rhs := exposeRelevantUniverses (← instantiateMVars ctx.rhs) p
+      try
+        addMessageContext m!"{header}{indentD m!"{entry.lhs} =?= {entry.rhs}"}\nwhile trying to unify{indentD m!"{lhs} : {← inferType lhs}"}\nwith{indentD m!"{rhs} : {← inferType rhs}"}"
+      catch _ =>
+        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
+
+def mkLevelErrorMessage (entry : PostponedEntry) : MetaM MessageData := do
+  mkLeveErrorMessageCore "failed to solve universe constraint" entry
+
+private def processPostponedStep (exceptionOnFailure : Bool) : MetaM Bool :=
   traceCtx `Meta.isLevelDefEq.postponed.step do
     let ps ← getResetPostponed
     for p in ps do
       unless (← withReader (fun ctx => { ctx with defEqCtx? := p.ctx? }) <| isLevelDefEqAux p.lhs p.rhs) do
-        return false
+        if exceptionOnFailure then
+          throwError (← mkLevelErrorMessage p)
+        else
+          return false
     return true
 
-partial def processPostponed (mayPostpone : Bool := true) : MetaM Bool := do
+partial def processPostponed (mayPostpone : Bool := true) (exceptionOnFailure := false) : MetaM Bool := do
   if (← getNumPostponed) == 0 then
     return true
   else
@@ -187,7 +221,7 @@ partial def processPostponed (mayPostpone : Bool := true) : MetaM Bool := do
           return true
         else
           trace[Meta.isLevelDefEq.postponed] "processing #{numPostponed} postponed is-def-eq level constraints"
-          if !(← processPostponedStep) then
+          if !(← processPostponedStep exceptionOnFailure) then
             return false
           else
             let numPostponed' ← getNumPostponed

tests/lean/343.lean.expected.out

@@ -1,11 +1,7 @@
 343.lean:27:11-27:16: warning: declaration uses 'sorry'
-343.lean:30:24-30:54: error: stuck at solving universe constraints
+343.lean:30:24-30:54: error: stuck at solving universe constraint
   max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
 while trying to unify
-  CatIsh.Obj.{max (max (?u + 1) (?u + 1)) ?u ?u,
-      max ((max (?u + 1) (?u + 1)) + 1) ((max ?u ?u) + 1)}
-    Catish.{max ?u ?u,
-      max (?u + 1) (?u + 1)} : Type (max ((max (?u + 1) (?u + 1)) + 1) ((max ?u ?u) + 1))
+  Catish.Obj Catish.Obj
 with
-  CatIsh.{max ?u ?u,
-    max (?u + 1) (?u + 1)} : Type (max ((max ?u ?u) + 1) ((max (?u + 1) (?u + 1)) + 1))
+  CatIsh.{max ?u ?u, max (?u + 1) (?u + 1)}

tests/lean/456.lean

@@ -0,0 +1 @@
+def A : Sort u := { s : Prop // _ }

tests/lean/456.lean.expected.out

@@ -0,0 +1,6 @@
+456.lean:1:18-1:35: error: failed to solve universe constraint
+  u =?= max 1 ?u
+while trying to unify
+  Sort u : Type u
+with
+  Type : Type 1