From f75ce86f71ad4780d8cc0249ca85520da7b6108f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 8 Apr 2021 18:54:53 +0200
Subject: [PATCH] fix: server: go to type definition

---
 src/Lean/Server/FileWorker.lean                     | 5 ++++-
 tests/lean/interactive/definition.lean              | 6 ++++++
 tests/lean/interactive/definition.lean.expected.out | 9 +++++++++
 3 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/interactive/definition.lean
 create mode 100644 tests/lean/interactive/definition.lean.expected.out

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 8263fb2179..515c40e228 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -414,7 +414,10 @@ section RequestHandling
       (notFoundX := pure #[]) fun snap => do
         for t in snap.toCmdState.infoState.trees do
           if let some (ci, Info.ofTermInfo i) := t.hoverableInfoAt? hoverPos then
-            let expr ← if goToType? then ci.runMetaM i.lctx <| Meta.inferType i.expr else i.expr
+            let mut expr := i.expr
+            if goToType? then
+              expr ← ci.runMetaM i.lctx do
+                Meta.instantiateMVars (← Meta.inferType expr)
             if let some n := expr.constName? then
               let mod? ← ci.runMetaM i.lctx <| findModuleOf? n
               let modUri? ← match mod? with
diff --git a/tests/lean/interactive/definition.lean b/tests/lean/interactive/definition.lean
new file mode 100644
index 0000000000..f302e1fe66
--- /dev/null
+++ b/tests/lean/interactive/definition.lean
@@ -0,0 +1,6 @@
+inductive Foo where
+  | foo
+example : Foo :=
+  let c := Foo.foo
+  c
+--^ textDocument/typeDefinition
diff --git a/tests/lean/interactive/definition.lean.expected.out b/tests/lean/interactive/definition.lean.expected.out
new file mode 100644
index 0000000000..de7824b6d1
--- /dev/null
+++ b/tests/lean/interactive/definition.lean.expected.out
@@ -0,0 +1,9 @@
+{"textDocument": {"uri": "file://definition.lean"},
+ "position": {"line": 4, "character": 2}}
+[{"targetUri": "file://definition.lean",
+  "targetSelectionRange":
+  {"start": {"line": 0, "character": 10}, "end": {"line": 0, "character": 13}},
+  "targetRange":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 1, "character": 7}},
+  "originSelectionRange":
+  {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 3}}}]