feat: include types in the "ambiguous, possible interpretations" error message

src/Lean/Elab/App.lean

@@ -911,10 +911,9 @@ private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array A
     if successes.size == 1 then
       applyResult successes[0]
     else if successes.size > 1 then
-      let lctx ← getLCtx
-      let opts ← getOptions
-      let msgs : Array MessageData := successes.map fun success => match success with
-        | EStateM.Result.ok e s => MessageData.withContext { env := s.meta.core.env, mctx := s.meta.meta.mctx, lctx := lctx, opts := opts } e
+      let msgs : Array MessageData ← successes.mapM fun success => do
+        match success with
+        | EStateM.Result.ok e s => withMCtx s.meta.meta.mctx <| withEnv s.meta.core.env do addMessageContext m!"{e} : {← inferType e}"
         | _                     => unreachable!
       throwErrorAt f "ambiguous, possible interpretations {toMessageList msgs}"
     else

src/Lean/MonadEnv.lean

@@ -14,6 +14,14 @@ namespace Lean
 def setEnv [MonadEnv m] (env : Environment) : m Unit :=
   modifyEnv fun _ => env
 
+def withEnv [Monad m] [MonadFinally m] [MonadEnv m] (env : Environment) (x : m α) : m α := do
+  let saved ← getEnv
+  try
+    setEnv env
+    x
+  finally
+    setEnv saved
+
 def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getEnv).find? declName with
   | some (ConstantInfo.inductInfo ..) => return true

tests/lean/641.lean.expected.out

@@ -1,8 +1,8 @@
 def y : Unit :=
 Foo.x
 641.lean:9:17-9:18: error: ambiguous, possible interpretations 
-  Bar.x
+  Bar.x : Unit
   
-  Foo.x
+  Foo.x : Unit
 def Rig.x : Nat :=
 _root_.x

tests/lean/emptyc.lean.expected.out

@@ -1,4 +1,4 @@
 emptyc.lean:19:0-19:2: error: ambiguous, possible interpretations 
-  ∅
+  ∅ : A
   
-  { x := 0 }
+  { x := 0 } : A

tests/lean/macroPrio.lean.expected.out

@@ -1,6 +1,6 @@
 0 + 1 : Nat
 macroPrio.lean:12:7-12:13: error: ambiguous, possible interpretations 
-  1 * 2
+  1 * 2 : ?m
   
-  1 + 1
+  1 + 1 : ?m
 2 - 2 : Nat

tests/lean/parserPrio.lean.expected.out

@@ -1,7 +1,7 @@
 [1, 2]
 6
 parserPrio.lean:28:7-28:10: error: ambiguous, possible interpretations 
-  2 * 1
+  2 * 1 : ?m
   
-  [1]
+  [1] : List ?m
 [1, 2, 3]