Every module is indeed compiled with a fresh context. The untyped
module doesn't directly refer to typed-racket/utils/tc-utils, which is
the file that defines typed-context?, but it does refer to a typed
module, whose expansion will contain a reference to that module.
Consider:
#lang typed/racket
(provide f)
(define (f [x : Integer]) (+ x 1))
That expands to (among a lot of other things):
(define-values (f) (lambda (x) (#%app + x '1)))
(define-syntaxes (f.1) (#%app make-redirect2 (quote-syntax f.3)))
(define-syntaxes
(f.2)
(#%app make-typed-renaming (t-quote-syntax f) (t-quote-syntax f.1)))
Where f.2 is provided as f, and f.3 is the contracted version of the identifier.
Then `make-typed-renaming` is effectively `(lambda (a b) (lambda (stx)
(if (unbox typed-context?) a b)))`
So it's the definition of `f` that depends on the box, and so there's
a fresh instantiation of `tc-utils` for every module that gets
expanded that depends on the typed module above.
Hopefully that clarifies things a bit more.
Sam
On Wed, Oct 7, 2020 at 10:07 PM Nathaniel Griswold
<
nategr...@gmail.com> wrote:
>
> Hm, I have this two reads for a over and I didn’t quite get it. I thought every module was compiled in a fresh context so my issue is I’m wondering how that identifier for the box is defined for syntax expansion in untyped modules. Maybe you understand what I mean; otherwise I’ll give the paper a look later tonight or tomorrow to see what I’m missing here.
>
> Thanks
>
> > On Oct 7, 2020, at 8:44 PM, Sam Tobin-Hochstadt <
sa...@cs.indiana.edu> wrote:
> >
> > The way this works, the box doesn't have to "get into" any modules