Type information lost for required function, when used at REPL

gistfile1.txt

Given these two files:

;; tr0.rkt
#lang typed/racket/base
(: f (Number -> Number))
(define (f n)
  n)
(provide f)

;; tr1.rkt
#lang typed/racket/base
(require "tr0.rkt")
(f 1)

Then:

$ racket
Welcome to Racket v6.0.1.4.
-> ,en tr1.rkt
1
"tr1.rkt"> (f 1)
; readline-input:2:0: Type Checker: missing type for identifier;
;  consider using `require/typed' to import it
;   identifier: idY6
;   from module: tr0.rkt
;   in: (f 1)
; [,bt for context]
"tr1.rkt"> ,bt
; readline-input:2:0: Type Checker: missing type for identifier;
;  consider using `require/typed' to import it
;   identifier: idY6
;   from module: tr0.rkt
;   in: (f 1)
;   context...:
;    /Users/greg/src/plt/racket/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:392:0: tc-toplevel-form
;    fail-to-succeed
;    /Users/greg/src/plt/racket/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:40:0: tc-setup
;    /Users/greg/src/plt/racket/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:25:4
;    /Users/greg/src/plt/racket/pkgs/xrepl-pkgs/xrepl-lib/xrepl/xrepl.rkt:1346:0
;    /Users/greg/src/plt/racket/racket/collects/racket/private/misc.rkt:87:7
"tr1.rkt"> 

In other words, `f` evaluates fine in the file, but at the racket REPL
`f` seems to lack type information. (Same problem in my Emacs
racket-mode REPL.)

However, in the DrRacket REPL ("interactions"), `f` evaluates just fine.

What is DrRacket doing differently? I want to do it in racket-mode REPL.

Note: Both normal Racket command-line and my racket-mode are using the
standard `read-eval-print-loop`, which IIRC does
`(eval (cons #%top-interaction form))`.

Note: `f` evaluates fine at the REPL when in the tr0.rkt namespace/module
in which it's defined. The issue seems to be related to provide-ing
and require-ing it.