>Instead of run-time reflection on values, I think an IDE implementing 
jump to definition should use source location and binding information 
from syntax objects. That's how DrRacket does it.

>The attached DrRacket screenshot (of [1]), in which I've tacked a bunch 
of binding arrows, shows how local definitions and complex 
macro-introduced binding structures are supported. It also works across 
modules, even with renaming: in the program `#lang racket (define one 
1)`, right-clicking on `define` and choosing "Jump to Binding 
Occurrence" will highlight `racket`, because the initial import of the 
racket language establishes the applicable binding of define, whereas 
choosing "Open Defining File" will open the racket/private/kw module, 
and then choosing "Jump to Definition (in Other File)" will jump to the 
definition of `new-define` on line 1171 of kw.rkt, which is renamed 
elsewhere to become the `define` of `#lang racket`.

>Since syntax objects from the expander encode all the details of scope, 
this works mostly automatically. DrRacket makes this functionality 
available as a library, so navigation features can also be used from 
Emacs with racket-xp-mode [2] or other editors with the Language Server 
Protocol [3].

I suppose this could work, but it seems the wrong layer of abstraction and a bit round-about to me, it also only works on languages that use Scheme-style syntax. Instead, I’d propose compiling the relevant code to Tree-IL (without optimisations, should work with most languages).  (For Scheme, this is essentially macro expansion, but the resulting object won’t technically be a syntax object.)

In Tree-IL, all syntax has been expanded (in tree form), which eliminates a lot of complications. Yet, source location information remains available (albeit not documented ...)! And the original variable names remain available (together with an unshadow-ified version, so for local variables you can move upwards to find the corresponding definition and in particular its source location.

A large upside is that this should work for most languages (not only Scheme) and is relatively straightforward to implement, a small downside is that information on definitions like (let-syntax ((f [...])) ...) aren’t available – you only see the return of (f stuff), not ‘f’ itself.

(But this downside applies to the ‘syntax’ route as well, unless you are doing complicated (but possible!) DIY partial macro expansion shenanigans.)

Best regards,
Maxime Devos.