From f5f9be191bd8968fc34cd179640aba047d74e6bd Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 31 May 2021 19:29:49 +0200
Subject: [PATCH] fix: show expected type in term goal

---
 src/Lean/Server/FileWorker.lean                        | 2 +-
 tests/lean/interactive/plainTermGoal.lean.expected.out | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 8ed904250d..fdfb2d945f 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -479,7 +479,7 @@ section RequestHandling
         for t in snap.cmdState.infoState.trees do
           if let some (ci, Info.ofTermInfo i) := t.termGoalAt? hoverPos then
             let goal ← ci.runMetaM i.lctx <| open Meta in do
-              let ty ← instantiateMVars <|<- inferType i.expr
+              let ty ← instantiateMVars <| i.expectedType?.getD (← inferType i.expr)
               withPPInaccessibleNames <| Meta.ppGoal (← mkFreshExprMVar ty).mvarId!
             let range := if hasRange i.stx then rangeOfSyntax! text i.stx else ⟨p.position, p.position⟩
             return some { goal := toString goal, range }
diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out
index fd31106641..810a9271b9 100644
--- a/tests/lean/interactive/plainTermGoal.lean.expected.out
+++ b/tests/lean/interactive/plainTermGoal.lean.expected.out
@@ -17,7 +17,7 @@
  "position": {"line": 2, "character": 29}}
 {"range":
  {"start": {"line": 2, "character": 28}, "end": {"line": 2, "character": 46}},
- "goal": "⊢ 1 < Nat.succ 1"}
+ "goal": "⊢ 1 < 2"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 2, "character": 44}}
 {"range":
@@ -27,7 +27,7 @@
  "position": {"line": 11, "character": 10}}
 {"range":
  {"start": {"line": 11, "character": 10}, "end": {"line": 11, "character": 18}},
- "goal": "y : Int\n⊢ Nat"}
+ "goal": "y : Int\n⊢ OptionM Nat"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 16, "character": 16}}
 {"range":
@@ -57,4 +57,4 @@
  "position": {"line": 31, "character": 8}}
 {"range":
  {"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 24}},
- "goal": "n : Nat\n⊢ n < Nat.succ n"}
+ "goal": "n : Nat\n⊢ n < n + 1"}