diff --git a/collects/tests/typed-racket/succeed/pr13747.rkt b/collects/tests/typed-racket/succeed/pr13747.rkt
new file mode 100644
index 0000000000..abd9aa1216
--- /dev/null
+++ b/collects/tests/typed-racket/succeed/pr13747.rkt
@@ -0,0 +1,13 @@
+#lang racket
+
+;; Test that `require/typed` works at the top-level
+
+(require racket/sandbox)
+
+(define evaluator
+  (call-with-trusted-sandbox-configuration
+   (λ () (make-evaluator 'typed/racket))))
+
+(evaluator '(require/typed racket/base [values (Integer -> Integer)]))
+(evaluator '(values 1))
+
diff --git a/collects/typed-racket/base-env/prims.rkt b/collects/typed-racket/base-env/prims.rkt
index b5cf6bb31b..39889bd0eb 100644
--- a/collects/typed-racket/base-env/prims.rkt
+++ b/collects/typed-racket/base-env/prims.rkt
@@ -133,7 +133,21 @@ This file defines two sorts of primitives. All of them are provided into any mod
          (raise-syntax-error #f "at least one specification is required" stx))
        #`(begin c.spec ...)]
       [(_ #:internal nm:opt-rename ty lib (~optional [~seq #:struct-maker parent]) ...)
-       (with-syntax ([cnt* (generate-temporary #'nm.nm)]
+       (with-syntax ([cnt* (if (eq? (syntax-local-context) 'top-level)
+                               ;; if we're at the top-level, we can generate the contract
+                               ;; immediately, but otherwise the contract will be fixed up
+                               ;; by the module type-checking pass later
+                               (let ([typ (parse-type #'ty)])
+                                 (ignore
+                                  (type->contract
+                                   typ
+                                   ;; this is for a `require/typed', so the value is not from the typed side
+                                   #:typed-side #f
+                                   (lambda ()
+                                     (tc-error/stx #'ty "Type ~a could not be converted to a contract." typ)))))
+                               ;; in the fix-up case, the contract is just an identifier
+                               ;; that is defined below
+                               (generate-temporary #'nm.nm))]
                      [hidden (generate-temporary #'nm.nm)]
                      [sm (if (attribute parent)
                              #'(#:struct-maker parent)
@@ -143,20 +157,14 @@ This file defines two sorts of primitives. All of them are provided into any mod
                               'typechecker:contract-def)])
            (quasisyntax/loc stx
              (begin
-               #,(syntax-property (if (eq? (syntax-local-context) 'top-level)
-                                      (let ([typ (parse-type #'ty)])
-                                        #`(define cnt*
-                                            #,(type->contract
-                                               typ
-                                               ;; this is for a `require/typed', so the value is not from the typed side
-                                               #:typed-side #f
-                                               (lambda () (tc-error/stx #'ty "Type ~a could not be converted to a contract." typ)))))
-                                      (syntax-property #'(define cnt* #f)
-                                                   prop-name #'ty))
-                                  'typechecker:ignore #t)
+               ;; define `cnt*` to be fixed up later by the module
+               ;; type-checking (not defined at top-level since it
+               ;; doesn't work with local expansion)
+               #,@(ignore (if (eq? (syntax-local-context) 'top-level)
+                              #'()
+                              #`(#,(syntax-property #'(define cnt* #f) prop-name #'ty))))
                #,(internal #'(require/typed-internal hidden ty . sm))
-               #,(syntax-property #'(require/contract nm.spec hidden cnt* lib)
-                                  'typechecker:ignore #t)))))]))
+               #,(ignore #'(require/contract nm.spec hidden cnt* lib))))))]))
   (values (r/t-maker #t) (r/t-maker #f))))
 
 (define-syntax-rule (require/typed/provide lib [nm t] ...)
diff --git a/collects/typed-racket/utils/require-contract.rkt b/collects/typed-racket/utils/require-contract.rkt
index f9685ded81..2ab535518e 100644
--- a/collects/typed-racket/utils/require-contract.rkt
+++ b/collects/typed-racket/utils/require-contract.rkt
@@ -48,16 +48,21 @@
 
   (syntax-parse stx
     [(require/contract nm:renameable hidden:id cnt lib)
-     #`(begin (require (only-in lib [nm.orig-nm nm.orig-nm-r]))
-              (define-syntax nm.nm
+     #`(begin (define-syntax nm.nm
                 (make-rename-transformer
                  (syntax-property (syntax-property (quote-syntax hidden)
                                                    'not-free-identifier=? #t)
                                   'not-provide-all-defined #t)))
               (define-ignored hidden
-                (contract cnt
-                          (get-alternate nm.orig-nm-r)
-                          '(interface for #,(syntax->datum #'nm.nm))
-                          (current-contract-region)
-                          (quote nm.nm)
-                          (quote-srcloc nm.nm))))]))
+                (let ()
+                  ;; Use `local-require` in order to use this internal
+                  ;; definition context instead of defining at the top-level.
+                  ;; This avoids top-level hopelessness to do with
+                  ;; `local-expand` and definitions.
+                  (local-require (only-in lib [nm.orig-nm nm.orig-nm-r]))
+                  (contract cnt
+                            (get-alternate nm.orig-nm-r)
+                            '(interface for #,(syntax->datum #'nm.nm))
+                            (current-contract-region)
+                            (quote nm.nm)
+                            (quote-srcloc nm.nm)))))]))