Macros are run at compile time, and are used to rewrite source code prior to interpretation or compilation. They're mostly used to make nicer syntax, e.g. a macro could turn an expression like `(with-file (f "/tmp/foo") ...)` into a working implementation like:

    (let* ((f (open "/tmp/foo"))
           (result ...))
      (close f)
      result)

Here, the authors make macros for type annotations, i.e. they take expressions like `(my-value : my-type)`, check whether the types unify correctly, and spit out an untyped expression implementing that value if they do.

By using macros, the type system becomes modular: new type system features (subtyping, kinds, etc.) can be written by the programmer as a set of macros, rather than as a whole new language (and all of the work that entails). They test their claim by implementing a bunch of features, combining/reusing them in a bunch of mini languages, and write some semi-plausible programs in these languages, to see if they're realistic.