Unexpected sensitivity to order of `require`d typed modules in untyped code

[jessealama]

What version of Racket are you using?

8.0 (problem occurs in both the CS and BC variants)

What program did you run?

raco exe src/c.rkt, with the following setup:

Three programs, a.rkt, b.rkt, and c.rkt are sitting in a subdirectory, src, of the current directory. It is important that the programs are in separate files, and that none are in the current directory. If I make a single-file, multi-submodule equivalent of this example, everything works.

src/a.rkt

#lang typed/racket/base
(provide a-func)
(define (a-func whatever) "hi")

src/b.rkt

#lang typed/racket/base
(provide b-func)
(require (file "a.rkt"))
(define (b-func thing)
  (a-func (cons 'foo thing)))

src/c.rkt

#lang racket/base
(require (file "b.rkt")
         (file "a.rkt"))
(define (c-func x)
  (a-func (b-func x)))

Notice that src/c.rkt is an untyped module.

What should have happened?

raco exe src/c.rkt should not have failed.

If you got an error message, please include it here.

$ raco exe src/c.rkt 
instantiate: unknown module
  module name: (submod "/Users/jesse/tr-bug/a.rkt" #%contract-defs)
  context...:
   /Applications/Racket v8.0/collects/compiler/embed.rkt:450:0: get-code
   /Applications/Racket v8.0/collects/racket/private/map.rkt:269:4: loop
   /Applications/Racket v8.0/collects/compiler/embed.rkt:1159:0: do-write-module-bundle
   /Applications/Racket v8.0/collects/compiler/embed.rkt:1531:6
   "/Applications/Racket v8.0/share/pkgs/compiler-lib/compiler/commands/exe.rkt": [running body]
   "/Applications/Racket v8.0/collects/raco/raco.rkt": [running body]
   "/Applications/Racket v8.0/collects/raco/main.rkt": [running body]

Additional Information

• If you switch the order of the requires in src/c.rkt, raco exe src/c.rkt works as expected.
• You can see the problem if you do raco expand src/c.rkt, so the error seems to not be one with raco exe per se. What I mean is that in the raco expand output, you will see the problematic #%require:

...
(#%require
    (rename (submod
             #<path:./a.rkt>
             #%contract-defs-reference
             ".."
             #%contract-defs)
            a-func
            a-func))
...

Presumably that #<path:./a.rkt> should be (file "a.rkt"), which is how b.rkt gets handled:

   (#%require
    (rename (submod
             (file "b.rkt")
             #%contract-defs-reference
             ".."
             #%contract-defs)
            b-func
            b-func))

• The problem is a TR one: if I change a.rkt and b.rkt to racket/base, raco exe works as expected.

[capfredf]

I didn't know TR is doing some magic here. Will look into it.
Also, if I change (file "xx.rkt") to "xx.rkt" in c.rkt, racket src/c.rkt works fine.