This is a little more general. They implement a stack of type systems all the way up to F-omega, and they're able reuse and compose the macro libraries to make the more elaborate type checkers. It's pretty impressive.

Ok, that is rather cool. Could something like this be used to make a better Template Haskell?

Someone's working on something like that already https://github.com/lexi-lambda/hackett

Awesome! Nice find.

Typed Racket runs after macro expansion, performing analysis on fully-expanded code. This technique runs as part of macro expansion, rather than after. The upshot is that macros get to use and generate type information, so language and type system features like typeclasses or GADTs can be library-provided macros.

Typed Racket uses macro expansion to translate its typed surface language into a typed core language, and then typechecks the core language.

Our approach uses macro expansion to typecheck the surface language and translates it into an untyped core language.

The two approaches should be considered alternative tools in a programmer's toolbox.