From 1450a86c4dafab6be6f802fa731699d8285d6383 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 6 Mar 2022 07:26:31 -0800
Subject: [PATCH] feat: include types in the "ambiguous, possible
 interpretations" error message

---
 src/Lean/Elab/App.lean                  | 7 +++----
 src/Lean/MonadEnv.lean                  | 8 ++++++++
 tests/lean/641.lean.expected.out        | 4 ++--
 tests/lean/emptyc.lean.expected.out     | 4 ++--
 tests/lean/macroPrio.lean.expected.out  | 4 ++--
 tests/lean/parserPrio.lean.expected.out | 4 ++--
 6 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 6e77d15a4a..ed30e816b2 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 09d5b006e9..f2dbd49009 100644
--- a/src/Lean/MonadEnv.lean
+++ b/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
diff --git a/tests/lean/641.lean.expected.out b/tests/lean/641.lean.expected.out
index 121e2d76dc..b302a8efc1 100644
--- a/tests/lean/641.lean.expected.out
+++ b/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
diff --git a/tests/lean/emptyc.lean.expected.out b/tests/lean/emptyc.lean.expected.out
index 3a730562fc..f1e3c59f6e 100644
--- a/tests/lean/emptyc.lean.expected.out
+++ b/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
diff --git a/tests/lean/macroPrio.lean.expected.out b/tests/lean/macroPrio.lean.expected.out
index 3df230ae6d..35aa7f5964 100644
--- a/tests/lean/macroPrio.lean.expected.out
+++ b/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
diff --git a/tests/lean/parserPrio.lean.expected.out b/tests/lean/parserPrio.lean.expected.out
index 1c329a8c68..3087b41a9b 100644
--- a/tests/lean/parserPrio.lean.expected.out
+++ b/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]