This all looks good, but I'm concerned about the potential performance implications of reset-table, since that table is quite large. Is there something different we can do to create a more stable table, or just to modify fewer entries?

It's possible that a different kind of table would work better (e.g., keyed on syntax-e results instead of identifier-binding-symbol results), but that might speed up the top-level at the expense of module checking. It's hard to know how far to push on the (hopeless) top level.

The problem with a free-id table is shifting identifier bindings, and those create other problems, such as in

(define-syntax-rule (m)
  (define x "hi"))
(define x 5)
(m)

In that example, the macro-introduced x definition as a string will be confused with the original x definition as a number.

Possibly, a better approach to rebuilding the table is to detect top-level definitions in the local-expanded form and force the corresponding bindings by evaluating (define-syntaxes (id ...) (values)). There's an expand-syntax-top-level-with-compile-time-evals function that tries to do that more generally; I'm not sure whether that function would be better or even workable for TR, though.

It looks like the changes to colon.rkt regress the bug in #160. I bet that fixing the top-level is a higher priority, but this seems worth bringing up given the lack of a test-case for that bug.

It looks like this solution still doesn't quite work as expected, as this REPL interaction demonstrates:

-> (begin (require/typed racket/base [values (-> String String)]) values)
- : (All (a b ...)
      (case-> (-> (values)) (-> a a) (-> a b ... b (values a b ... b))))
#<procedure:values>

It gets the original type for values rather than the new one because the environment is only reset after each interaction. It does seem that we need the trampolining macro approach.

I'm now working on an alternative approach using trampolining macros. I think it fixes PR13747 and also eliminates some other hacks for the top-level.

The branch is here: master...takikawa:toplevel-trampoline

I just merged #175, which repairs this using the define-syntaxes technique. Thanks Matthew for suggesting that approach.