The original paper (I was just reading parts of it) suggests the first interpretation is (or was) correct, that the type-checker is looking at expanded programs

oh yes, it’s looking at the expanded programs. My comment was about how using macro probably won’t make things easier.

There is a section of the typed racket guide that describes this limitation https://docs.racket-lang.org/ts-guide/caveats.html#%28part._.Macros_and_compile-time_computation%29