Put a finer point on the only-raising-one-exception point

src/Lean/Elab/SyntheticMVars.lean

@@ -11,6 +11,7 @@ public import Lean.Util.ForEachExpr
 public import Lean.Util.OccursCheck
 public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.AbstractNestedProofs
+public import Init.Data.List.Sort.Basic
 
 public section
 
@@ -304,10 +305,9 @@ def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option M
 We use this method to report typeclass (and coercion) resolution problems that are "stuck".
 That is, there is nothing else to do, and we don't have enough information to synthesize them using TC resolution.
 -/
-def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermElabM Unit := do
-  let some mvarSyntheticDecl ← getSyntheticMVarDecl? mvarId | return ()
-  withRef mvarSyntheticDecl.stx do
-    match mvarSyntheticDecl.kind with
+def reportStuckSyntheticMVar (mvarId : MVarId) (mvarDecl : SyntheticMVarDecl) (ignoreStuckTC := false) : TermElabM Unit := do
+  withRef mvarDecl.stx do
+    match mvarDecl.kind with
     | .typeClass extraErrorMsg? =>
       let extraErrorMsg := extraMsgToMsg extraErrorMsg?
       unless ignoreStuckTC do
@@ -337,8 +337,45 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
 -/
 private def reportStuckSyntheticMVars (ignoreStuckTC := false) : TermElabM Unit := do
   let pendingMVars ← modifyGet fun s => (s.pendingMVars, { s with pendingMVars := [] })
-  for mvarId in pendingMVars do
-    reportStuckSyntheticMVar mvarId ignoreStuckTC
+  /-
+  Calling the singular reportStuckSyntheticMVar function will usually raise
+  an exception, meaning that we only expect to report one issue with
+  synthetic MVars. Given that, what's the best one to return?
+
+  If we have stuck typeclass instances associated with overlapping syntactic
+  ranges, we want to report a problem whose syntactic range *does not include
+  other unsolved typeclass problem ranges*. Here's a case where we want to
+  include the innermost range, if `x` has unknown type:
+
+      |--------------------| <- stuck typeclass problem is Decidable (x < x)
+      if x < x then 1 else 2
+         |---| <- stuck typeclass problem is LT _?
+
+  Reporting the `LT _` typeclass is more informative to the user.
+
+  A simple way to achieve this is prioritizing typeclass error messages with
+  smaller syntactic ranges.
+  -/
+  let pendingMVarsWithDecls ← pendingMVars.filterMapM (fun mvarId => do
+    let some decl ← getSyntheticMVarDecl? mvarId | return .none
+    return .some (mvarId, decl)
+  )
+  let prioritizedProblems := pendingMVarsWithDecls.mergeSort (fun (_, decl1) (_, decl2) =>
+    match (decl1.kind, decl2.kind) with
+     | (.typeClass _, .typeClass _) =>
+       match (decl1.stx.getRange?, decl2.stx.getRange?) with
+        | (.some r1, .some r2) => if r1.bsize != r2.bsize then
+            r1.bsize <= r2.bsize
+          else
+            r1.start <= r2.start
+        | (.none, _) => false
+        | _ => true
+     -- All non-typeclass problems are equivalent and come before typeclass problems
+     | (.typeClass _, _) => false
+     | _ => true
+  )
+  for (mvarId, mvarDecl) in prioritizedProblems do
+    reportStuckSyntheticMVar mvarId mvarDecl ignoreStuckTC
 
 private def getSomeSyntheticMVarsRef : TermElabM Syntax := do
   for mvarId in (← get).pendingMVars do

tests/lean/353.lean.expected.out

@@ -1,7 +1,7 @@
-353.lean:13:26-13:50: error: typeclass instance problem is stuck
-  Arr.{?u, ?u + 1} (@?m a₁ a₂) (Sort ?u)
+353.lean:13:27-13:35: error: typeclass instance problem is stuck
+  Arr.{1, ?u} Bool (@?m a₁ a₂)
 
-Note: Lean will not try to resolve this typeclass instance problem because the first type argument to `Arr.{u1,
+Note: Lean will not try to resolve this typeclass instance problem because the second type argument to `Arr.{u1,
   u2}` contains metavariables. This argument must be fully determined before Lean will try to resolve the typeclass.
 
 Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

tests/lean/run/due_to_metavariables.lean

@@ -67,6 +67,71 @@ Note: Lean will not try to resolve this typeclass instance problem because the f
 Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
 -/
 #guard_msgs in
-
-
 def f x := test x 3 x x x
+
+/-
+From Joseph's lean4-error-messages#41, this generates two stuck typeclass
+problems, `Decidable (x < y)` (unhelpfully the metavariables aren't even
+visible!) with a span of the entire ite, and `LT _?` with the span of just the
+scrutinee. The error message associated with the smaller range is better.
+-/
+/--
+error: typeclass instance problem is stuck
+  LT ?m.13
+
+Note: Lean will not try to resolve this typeclass instance problem because the type argument to `LT` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
+-/
+#guard_msgs in
+def min x y := if x < y then x else y
+
+def isDigitEven? [Monad m] [Alternative m] (n : Nat) : m Bool := do
+  guard (n < 10)
+  return n % 2 == 0
+
+/-
+From Joseph's lean4-error-messages#81, this is similar to the previous example
+and is addressed by preferring any synthetic MVar problem that isn't a
+stuck typeclass resolution instance. Preferring smaller ranges generically
+would also work here.
+-/
+/--
+error: Application type mismatch: The argument
+  isDigitEven? n
+has type
+  ?m.9 Bool
+but is expected to have type
+  Prop
+in the application
+  @ite (Option Nat) (isDigitEven? n)
+-/
+#guard_msgs in
+def myOption (s : String) : Option Nat := do
+  let n ← s.toNat?
+  if isDigitEven? n then
+    return n
+  else
+    return 2 * n
+
+instance {n} : Functor (Vector · n) where
+  map f v := v.map f
+
+/-
+From Joseph's lean4-error-messages#56, this is a case where we *might* want to
+tweak prioritization in the future. This creates a typeclass resolution
+problem over the whole expression `Functor ?m.2`, and higher-order unification
+can't solve that `?m.2 = Vector · 3`.
+-/
+/--
+error: Application type mismatch: The argument
+  #v[1, 2, 3]
+has type
+  Vector Nat 3
+but is expected to have type
+  ?m.2 ?m.6
+in the application
+  id <$> #v[1, 2, 3]
+-/
+#guard_msgs in
+#eval Functor.map id #v[1, 2, 3]