feat: allow go-to-projection to look through reducible definitions (#12004)

This PR allows 'Go to Definition' to look through reducible definition
when looking for typeclass instance projections.

Specifically, this means that using 'Go to Definition' on uses of
`GT.gt` will now yield the corresponding `LT` instance as well.

src/Lean/Server/GoTo.lean

@@ -39,15 +39,24 @@ def GoToKind.determineTargetExprs (kind : GoToKind) (ti : TermInfo) : MetaM (Arr
   | _ =>
     return #[← instantiateMVars ti.expr]
 
-def getInstanceProjectionArg? (e : Expr) : MetaM (Option Expr) := do
-  let env ← getEnv
-  let .const n _ := e.getAppFn'
-    | return none
-  let some projInfo := env.getProjectionFnInfo? n
+partial def getInstanceProjectionArg? (e : Expr) : MetaM (Option Expr) := do
+  let some (e, projInfo) ← Meta.withReducible <| reduceToProjection? e
     | return none
   let instIdx := projInfo.numParams
   let appArgs := e.getAppArgs
   return appArgs[instIdx]?
+where
+  reduceToProjection? (e : Expr) : MetaM (Option (Expr × ProjectionFunctionInfo)) := do
+    let env ← getEnv
+    let .const n _ := e.getAppFn'
+      | return none
+    if let some projInfo := env.getProjectionFnInfo? n then
+      return some (e, projInfo)
+    -- Unfold reducible definitions when looking for a projection.
+    -- For example, this ensures that we get `LT.lt` instance projection entries on `GT.gt`.
+    let some e ← Meta.unfoldDefinition? e
+      | return none
+    reduceToProjection? e
 
 def isInstanceProjection (e : Expr) : MetaM Bool := do
   return (← getInstanceProjectionArg? e).isSome

tests/lean/interactive/goTo.lean

@@ -112,3 +112,15 @@ set_option pp.all true in
 -- duplicate definitions link to the original
 def mkFoo₁ := 1
      --^ textDocument/definition
+
+-- go-to-projection should be able to look through reducible definitions
+@[reducible] def foo'' (n : Nat) := Foo2.foo n
+
+#check foo'' 0
+      --^ textDocument/definition
+
+-- go-to-projection should not be able to look through semi-reducible definitions
+def foo''' (n : Nat) := Foo2.foo n
+
+#check foo''' 0
+      --^ textDocument/definition

tests/lean/interactive/goTo.lean.expected.out

@@ -301,3 +301,35 @@
   "originSelectionRange":
   {"start": {"line": 112, "character": 4},
    "end": {"line": 112, "character": 10}}}]
+{"textDocument": {"uri": "file:///goTo.lean"},
+ "position": {"line": 118, "character": 8}}
+[{"targetUri": "file:///goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "originSelectionRange":
+  {"start": {"line": 118, "character": 7},
+   "end": {"line": 118, "character": 14}}},
+ {"targetUri": "file:///goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 116, "character": 17},
+   "end": {"line": 116, "character": 22}},
+  "targetRange":
+  {"start": {"line": 116, "character": 17},
+   "end": {"line": 116, "character": 22}},
+  "originSelectionRange":
+  {"start": {"line": 118, "character": 7},
+   "end": {"line": 118, "character": 14}}}]
+{"textDocument": {"uri": "file:///goTo.lean"},
+ "position": {"line": 124, "character": 8}}
+[{"targetUri": "file:///goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 122, "character": 4},
+   "end": {"line": 122, "character": 10}},
+  "targetRange":
+  {"start": {"line": 122, "character": 4},
+   "end": {"line": 122, "character": 10}},
+  "originSelectionRange":
+  {"start": {"line": 124, "character": 7},
+   "end": {"line": 124, "character": 13}}}]