feat: make go-to-definition on a typeclass projection application go …

…to the instance(s)

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -122,6 +122,23 @@ def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info
     | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
     | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
     | _ => pure ()
+    expr ← ci.runMetaM i.lctx do instantiateMVars expr
+    -- go-to-definition on a projection application of a typeclass
+    -- should return all instances generated by TC
+    match expr.getAppFn with
+    | .const n _ => if let some info := ci.env.getProjectionFnInfo? n then
+      let instIdx := info.numParams + info.i
+      let appArgs := expr.getAppArgs
+      let rec extractInstances : Expr → RequestM (Array Name)
+        | .const declName _ => do
+          if ← ci.runMetaM i.lctx do Lean.Meta.isInstance declName then pure #[declName] else pure #[]
+        | .app fn arg => do pure $ (← extractInstances fn).append (← extractInstances arg)
+        | _ => pure #[]
+      if appArgs.size > instIdx then
+        let instArg := appArgs.get! instIdx
+        return ← (← extractInstances instArg).foldlM (init := #[]) fun acc n => do
+          pure $ acc.append (← ci.runMetaM i.lctx <| locationLinksFromDecl i n)
+    | _ => pure ()
   if let Info.ofFieldInfo fi := i then
     if kind == type then
       let expr ← ci.runMetaM i.lctx do