diff --git a/typed-racket-lib/typed-racket/core.rkt b/typed-racket-lib/typed-racket/core.rkt
index 25c41e21..dfa8f696 100644
--- a/typed-racket-lib/typed-racket/core.rkt
+++ b/typed-racket-lib/typed-racket/core.rkt
@@ -54,8 +54,6 @@
                      #,(if (unbox include-extra-requires?) extra-requires #'(begin))
                      before-code ... optimized-body ... after-code ... check-syntax-help)))))))]))
 
-(define did-I-suggest-:print-type-already? #f)
-(define :print-type-message " ... [Use (:print-type <expr>) to see more.]")
 (define (ti-core stx )
   (current-type-names (init-current-type-names))
   (syntax-parse stx
@@ -69,67 +67,4 @@
      ;; TODO(endobson): Remove the call to do-standard-inits when it is no longer necessary
      ;; Cast at the top-level still needs this for some reason
      (do-standard-inits)
-     (tc-toplevel/full stx #'form
-       (λ (body2 type)
-         (with-syntax*
-          ([(optimized-body ...) (maybe-optimize #`(#,body2))]
-           ;; Transform after optimization for top-level because the flattening will
-           ;; change syntax object identity (via syntax-track-origin) which doesn't work
-           ;; for looking up types in the optimizer.
-           [(transformed-body ...)
-            (change-contract-fixups (flatten-all-begins #'(begin optimized-body ...)))])
-          (define ty-str
-            (match type
-              ;; 'no-type means the form is not an expression and
-              ;; has no meaningful type to print
-              ['no-type #f]
-              ;; don't print results of type void
-              [(tc-result1: (== -Void type-equal?)) #f]
-              ;; don't print results of unknown type
-              [(tc-any-results: f) #f]
-              [(tc-result1: t f o)
-               ;; Don't display the whole types at the REPL. Some case-lambda types
-               ;; are just too large to print.
-               ;; Also, to avoid showing too precise types, we generalize types
-               ;; before printing them.
-               (define tc (cleanup-type t))
-               (define tg (generalize tc))
-               (format "- : ~a~a~a\n"
-                       (pretty-format-type tg #:indent 4)
-                       (cond [(equal? tc tg) ""]
-                             [else (format " [more precisely: ~a]" tc)])
-                       (cond [(equal? tc t) ""]
-                             [did-I-suggest-:print-type-already? " ..."]
-                             [else (set! did-I-suggest-:print-type-already? #t)
-                                   :print-type-message]))]
-              [(tc-results: t)
-               (define tcs (map cleanup-type t))
-               (define tgs (map generalize tcs))
-               (define tgs-val (make-Values (map -result tgs)))
-               (define formatted (pretty-format-type tgs-val #:indent 4))
-               (define indented? (regexp-match? #rx"\n" formatted))
-               (format "- : ~a~a~a\n"
-                       formatted
-                       (cond [(andmap equal? tgs tcs) ""]
-                             [indented?
-                              (format "\n[more precisely: ~a]"
-                                      (pretty-format-type (make-Values (map -result tcs))
-                                                          #:indent 17))]
-                             [else (format " [more precisely: ~a]" (cons 'Values tcs))])
-                       ;; did any get pruned?
-                       (cond [(andmap equal? t tcs) ""]
-                             [did-I-suggest-:print-type-already? " ..."]
-                             [else (set! did-I-suggest-:print-type-already? #t)
-                                   :print-type-message]))]
-              [x (int-err "bad type result: ~a" x)]))
-          (if (and ty-str
-                   (not (null? (syntax-e #'(transformed-body ...)))))
-              (with-syntax ([(transformed-body ... transformed-last)
-                             #'(transformed-body ...)])
-                #`(begin #,(if (unbox include-extra-requires?)
-                               extra-requires
-                               #'(begin))
-                         #,(arm #'(begin transformed-body ...))
-                         (begin0 #,(arm #'transformed-last)
-                           (display '#,ty-str))))
-              (arm #'(begin transformed-body ...))))))]))
+     (tc-toplevel/full stx #'form)]))
diff --git a/typed-racket-lib/typed-racket/tc-setup.rkt b/typed-racket-lib/typed-racket/tc-setup.rkt
index f99e0bee..1c2cebfe 100644
--- a/typed-racket-lib/typed-racket/tc-setup.rkt
+++ b/typed-racket-lib/typed-racket/tc-setup.rkt
@@ -1,6 +1,7 @@
 #lang racket/base
 
 (require "utils/utils.rkt"
+         syntax/kerncase
          syntax/stx
          racket/pretty racket/promise racket/lazy-require
          (env type-name-env type-alias-env mvar-env)
@@ -9,7 +10,8 @@
          (for-syntax racket/base)
          (for-template racket/base))
 (lazy-require [typed-racket/optimizer/optimizer (optimize-top)])
-(lazy-require [typed-racket/typecheck/tc-toplevel (tc-toplevel-form tc-module)])
+(lazy-require [typed-racket/typecheck/tc-toplevel (tc-module)])
+(lazy-require [typed-racket/typecheck/toplevel-trampoline (tc-toplevel-start)])
 
 (provide maybe-optimize init-current-type-names
          tc-module/full
@@ -36,7 +38,7 @@
 
 (define-logger online-check-syntax)
 
-(define (tc-setup orig-stx stx expand-ctxt do-expand checker k)
+(define (tc-setup orig-stx stx expand-ctxt do-expand stop-forms k)
   (set-box! typed-context? #t)
   ;(start-timing (syntax-property stx 'enclosing-module-name))
   (with-handlers
@@ -52,11 +54,11 @@
                    ;; reinitialize disappeared uses
                    [disappeared-use-todo      null]
                    [disappeared-bindings-todo null])
-      (define fully-expanded-stx (disarm* (do-expand stx expand-ctxt (list #'module*))))
+      (define expanded-stx (disarm* (do-expand stx expand-ctxt stop-forms)))
       (when (print-syntax?)
-        (pretty-print (syntax->datum fully-expanded-stx)))
+        (pretty-print (syntax->datum expanded-stx)))
       (do-time "Local Expand Done")
-      (let ([exprs (syntax->list (syntax-local-introduce fully-expanded-stx))])
+      (let ([exprs (syntax->list (syntax-local-introduce expanded-stx))])
         (when (pair? exprs)
           (log-message online-check-syntax-logger
                        'info
@@ -66,17 +68,25 @@
       ;; expansion errors to happen with out paying that cost
       (do-standard-inits)
       (do-time "Initialized Envs")
-      (find-mutated-vars fully-expanded-stx mvar-env)
-      (parameterize ([orig-module-stx (or (orig-module-stx) orig-stx)]
-                     [expanded-module-stx fully-expanded-stx])
-        (do-time "Starting `checker'")
-        (call-with-values (λ () (checker fully-expanded-stx))
-          (λ results
-            (do-time "Typechecking Done")
-            (apply k fully-expanded-stx results)))))))
+      (find-mutated-vars expanded-stx mvar-env)
+      (k expanded-stx))))
 
-(define (tc-toplevel/full orig-stx stx k)
-  (tc-setup orig-stx stx 'top-level local-expand/capture* tc-toplevel-form k))
+;; for top-level use
+(define (tc-toplevel/full orig-stx stx)
+  (tc-setup orig-stx stx 'top-level
+            local-expand/capture* (kernel-form-identifier-list)
+            (λ (head-expanded-stx)
+              (parameterize ([orig-module-stx (or (orig-module-stx) orig-stx)])
+                (do-time "Trampoline the top-level checker")
+                (tc-toplevel-start head-expanded-stx)))))
 
 (define (tc-module/full orig-stx stx k)
-  (tc-setup orig-stx stx 'module-begin local-expand tc-module k))
+  (tc-setup orig-stx stx 'module-begin local-expand (list #'module*)
+            (λ (fully-expanded-stx)
+              (do-time "Starting `checker'")
+              (parameterize ([orig-module-stx (or (orig-module-stx) orig-stx)]
+                             [expanded-module-stx fully-expanded-stx])
+                (call-with-values (λ () (tc-module fully-expanded-stx))
+                  (λ results
+                    (do-time "Typechecking Done")
+                    (apply k fully-expanded-stx results)))))))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
index d69447bf..aa6db55b 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
@@ -523,41 +523,30 @@
   (syntax-parse stx
     [(pmb . forms) (begin0 (type-check #'forms) (do-time "finished type checking"))]))
 
-;; typecheck a top-level form
+;; typecheck a top-level form that does not have any
+;; top-level `begin`s
 ;; used only from #%top-interaction
 ;; syntax -> (or/c 'no-type tc-results/c)
 (define (tc-toplevel-form form)
-  (syntax-parse form
-    ;; Don't open up `begin`s that are supposed to be ignored
-    [(~and ((~literal begin) e ...)
-           (~not (~or _:ignore^ _:ignore-some^)))
-     (begin0
-       (or (for/last ([form (in-syntax #'(e ...))])
-             (tc-toplevel-form form))
-           'no-type)
-       (report-all-errors))]
-    [_
-     ;; Handle type aliases
-     (when (type-alias? form)
-       (define-values (alias-names alias-map)
-         (get-type-alias-info (list form)))
-       (register-all-type-aliases alias-names alias-map))
-     ;; Handle struct definitions
-     (when (typed-struct? form)
-       (define name (name-of-struct form))
-       (define tvars (type-vars-of-struct form))
-       (register-type-name name)
-       (add-constant-variance! name tvars)
-       (define parsed (parse-typed-struct form))
-       (register-parsed-struct-sty! parsed)
-       (refine-struct-variance! (list parsed))
-       (register-parsed-struct-bindings! parsed))
-     (tc-toplevel/pass1 form)
-     (tc-toplevel/pass1.5 form)
-     (begin0 (tc-toplevel/pass2 form #f)
-             (report-all-errors))]))
-
-
+  ;; Handle type aliases
+  (when (type-alias? form)
+    (define-values (alias-names alias-map)
+      (get-type-alias-info (list form)))
+    (register-all-type-aliases alias-names alias-map))
+  ;; Handle struct definitions
+  (when (typed-struct? form)
+    (define name (name-of-struct form))
+    (define tvars (type-vars-of-struct form))
+    (register-type-name name)
+    (add-constant-variance! name tvars)
+    (define parsed (parse-typed-struct form))
+    (register-parsed-struct-sty! parsed)
+    (refine-struct-variance! (list parsed))
+    (register-parsed-struct-bindings! parsed))
+  (tc-toplevel/pass1 form)
+  (tc-toplevel/pass1.5 form)
+  (begin0 (tc-toplevel/pass2 form #f)
+          (report-all-errors)))
 
 ;; handle-define-new-subtype : Syntax -> Void
 (define (handle-define-new-subtype form)
diff --git a/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
new file mode 100644
index 00000000..06898ae0
--- /dev/null
+++ b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
@@ -0,0 +1,173 @@
+#lang racket/base
+
+;; This module implements Typed Racket's trampolining top-level
+;; typechecking. The entrypoint is the function provided below, which
+;; sets up the trampoline.
+;;
+;; Subsequently, the macros forms defined in the submodule at the bottom
+;; take over and keep head local-expanding until `begin` forms are exhausted,
+;; at which point the syntax can be fully-expanded and checked normally.
+
+(require "../utils/utils.rkt"
+         syntax/parse
+         (private syntax-properties)
+         (for-template racket/base))
+
+(provide tc-toplevel-start)
+
+;; entrypoint for typechecking a top-level interaction
+;; this is defined in this module (instead of tc-top-level.rkt) in
+;; order to avoid cyclic dependency issues
+;; syntax -> syntax
+(define (tc-toplevel-start stx)
+  (syntax-parse stx
+    #:literal-sets (kernel-literals)
+    ;; Don't open up `begin`s that are supposed to be ignored
+    [(~and (begin e ... e-last)
+           (~not (~or _:ignore^ _:ignore-some^)))
+     #'(begin (tc-toplevel-trampoline e) ...
+              (tc-toplevel-trampoline/report e-last))]))
+
+(module trampolines racket/base
+  (require "../utils/utils.rkt"
+           (for-syntax racket/base
+                       racket/match
+                       syntax/kerncase
+                       syntax/parse
+                       syntax/stx
+                       (rep type-rep)
+                       (optimizer optimizer)
+                       (types utils abbrev printer generalize)
+                       (typecheck tc-toplevel tc-app-helper)
+                       (private type-contract syntax-properties)
+                       (utils disarm lift utils timing tc-utils arm)))
+
+  (provide tc-toplevel-trampoline
+           tc-toplevel-trampoline/report)
+
+  (define-for-syntax (maybe-optimize body)
+    ;; do we optimize?
+    (if (optimize?)
+        (begin
+          (do-time "Starting optimizer")
+          (begin0 (stx-map optimize-top body)
+            (do-time "Optimized")))
+        body))
+
+  (define-for-syntax (trampoline-core stx report? kont)
+    (syntax-parse stx
+      [(_ e)
+       (define head-expanded
+         (disarm*
+          (local-expand/capture* #'e 'top-level (kernel-form-identifier-list))))
+       (syntax-parse head-expanded
+         #:literal-sets (kernel-literals)
+         [(begin (define-values (n) _) ... (~or _:ignore^ _:ignore-some^))
+          #'e]
+         ;; keep trampolining on begins
+         [(begin (define-values (n) e-rhs) ... (begin e ... e-last))
+          #`(begin (tc-toplevel-trampoline (define-values (n) e-rhs)) ...
+                   (tc-toplevel-trampoline e) ...
+                   #,(if report?
+                         #'(tc-toplevel-trampoline/report e-last)
+                         #'(tc-toplevel-trampoline e-last)))]
+         [_
+          (define fully-expanded
+            ;; a non-begin form can still cause lifts, so still have to catch them
+            (disarm* (local-expand/capture* #'e 'top-level (list #'module*))))
+          ;; Unlike the `begin` cases, we probably don't need to trampoline back
+          ;; to the top-level because we're not catching lifts from macros at the
+          ;; top-level context but instead from expression context.
+          (parameterize ([expanded-module-stx fully-expanded])
+            (syntax-parse fully-expanded
+              #:literal-sets (kernel-literals)
+              [(begin form ...)
+               (define forms (syntax->list #'(form ...)))
+               (define result
+                 (for/last ([form (in-list forms)])
+                   (tc-toplevel-form form)))
+               ;; Transform after optimization for top-level because the flattening
+               ;; will change syntax object identity (via syntax-track-origin) which
+               ;; doesn't work for looking up types in the optimizer.
+               (define new-stx
+                 (apply append
+                        (for/list ([form (in-list forms)])
+                          (change-contract-fixups (maybe-optimize (list form))))))
+               (kont new-stx result)]))])]))
+
+  ;; Trampoline that continues the typechecking process.
+  (define-syntax (tc-toplevel-trampoline stx)
+    (trampoline-core
+     stx #f
+     (λ (new-stx result)
+       (arm
+        (if (unbox include-extra-requires?)
+            #`(begin #,extra-requires #,@new-stx)
+            #`(begin #,@new-stx))))))
+
+  (begin-for-syntax
+    (define did-I-suggest-:print-type-already? #f)
+    (define :print-type-message " ... [Use (:print-type <expr>) to see more.]"))
+
+  ;; Trampoline that continues the typechecking process and reports the type
+  ;; information to the user.
+  (define-syntax (tc-toplevel-trampoline/report stx)
+    (trampoline-core
+     stx #t
+     (λ (new-stx result)
+       (define ty-str
+         (match result
+           ;; 'no-type means the form is not an expression and
+           ;; has no meaningful type to print
+           ['no-type #f]
+           ;; don't print results of type void
+           [(tc-result1: (== -Void type-equal?)) #f]
+           ;; don't print results of unknown type
+           [(tc-any-results: f) #f]
+           [(tc-result1: t f o)
+            ;; Don't display the whole types at the REPL. Some case-lambda types
+            ;; are just too large to print.
+            ;; Also, to avoid showing too precise types, we generalize types
+            ;; before printing them.
+            (define tc (cleanup-type t))
+            (define tg (generalize tc))
+            (format "- : ~a~a~a\n"
+                    (pretty-format-type tg #:indent 4)
+                    (cond [(equal? tc tg) ""]
+                          [else (format " [more precisely: ~a]" tc)])
+                    (cond [(equal? tc t) ""]
+                          [did-I-suggest-:print-type-already? " ..."]
+                          [else (set! did-I-suggest-:print-type-already? #t)
+                                :print-type-message]))]
+           [(tc-results: t)
+            (define tcs (map cleanup-type t))
+            (define tgs (map generalize tcs))
+            (define tgs-val (make-Values (map -result tgs)))
+            (define formatted (pretty-format-type tgs-val #:indent 4))
+            (define indented? (regexp-match? #rx"\n" formatted))
+            (format "- : ~a~a~a\n"
+                    formatted
+                    (cond [(andmap equal? tgs tcs) ""]
+                          [indented?
+                           (format "\n[more precisely: ~a]"
+                                   (pretty-format-type (make-Values (map -result tcs))
+                                                       #:indent 17))]
+                          [else (format " [more precisely: ~a]" (cons 'Values tcs))])
+                    ;; did any get pruned?
+                    (cond [(andmap equal? t tcs) ""]
+                          [did-I-suggest-:print-type-already? " ..."]
+                          [else (set! did-I-suggest-:print-type-already? #t)
+                                :print-type-message]))]
+           [x (int-err "bad type result: ~a" x)]))
+       (define with-printing
+        (with-syntax ([(e ... e-last) new-stx])
+          (if ty-str
+              #`(begin e ...
+                       (begin0 e-last (display '#,ty-str)))
+              #'(begin e ... e-last))))
+       (arm
+        (if (unbox include-extra-requires?)
+            #`(begin #,extra-requires #,with-printing)
+            with-printing))))))
+
+(require (for-template (submod "." trampolines)))
diff --git a/typed-racket-lib/typed-racket/utils/lift.rkt b/typed-racket-lib/typed-racket/utils/lift.rkt
index ec348858..02372af6 100644
--- a/typed-racket-lib/typed-racket/utils/lift.rkt
+++ b/typed-racket-lib/typed-racket/utils/lift.rkt
@@ -15,7 +15,7 @@
     (let loop ([stx stx])
       (define stx* (local-expand/capture-lifts stx ctx stop-ids))
       (syntax-parse stx*
-        #:literals (begin define-values)
+        #:literal-sets (kernel-literals)
         [(begin (define-values (n) e) ... e*)
          (define-values (sub-defss defs)
            (for/lists (_1 _2) ([e (in-list (syntax->list #'(e ...)))]