[stchang]

It could, though it's not clear whether it would be an improvement.

Typed Racket uses macro expansion to translate its typed surface language into a typed core language, and then type checks that core language.

This approach works well because the surface and core languages are similar, and thus the type checker need only handle a small number of core forms.

This approach is limited, however, to constructs that are translatable into the core typed language. For example, a few Racket `for/X` comprehension forms are not supported in Typed Racket because they are difficult to translate.

Our approach alternatively uses macro expansion to type check the surface language and translates it into an untyped core language. Thus it's less limited in the typed languages one may implement. The tradeoff is that the programmer must implement type rules for all forms in the surface language, rather than just the core language.