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:

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 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.