Fortunately, you can write a sound type system for a Lisp without needing to verify individual macros. That's what Typed Racket does, described in this paper: http://www.ccs.neu.edu/racket/pubs/pldi11-thacff.pdf
The basic idea is to first expand the whole program (really the whole module) and then to type check the fully expanded code, which doesn't have macros.
The basic idea is to first expand the whole program (really the whole module) and then to type check the fully expanded code, which doesn't have macros.