JonChesterfield parent
What's the objection to putting type annotations on the macro, and refusing to compile code where the arguments to the macro don't match the type?
There's no objection, but I think this solves a different problem than above described, and is possibly a more complicate matter in itself than it may look like. First, are you describing a way to typecheck macro so that it doesn't generate ill-typed code? The type system that does this is active research (I think requires modal typing?). Also this does not increase the expressive power of untyped Lisp macro -- just making them safer, while I was proposing their expressive power is unsatisfactory and should be enhanced via a sort of reflection. That would only makes them even harder to type!
Since a macro is a definition of syntax, I think you'd essentially need something like typing judgments to show how the typed elements of the syntax relate to one another, so that the type checker (e.g., a typical Hindley-Milner unifier) can use those rules. These are usually written as the fraction-looking things that show up in PLT papers. This is, as GP says, essentially extending the type system, which is a task fraught with peril (people write entire papers about type system extensions and their soundness, confluence, etc.).
Depends on your point of view really. I'd define a macro as a function with slightly weird evaluation rules.
If you want to write a macro where any call to it which typechecks creates code which itself typechecks, you have to deal with eval of sexpr which is roughly a recursive typecheck on partial information, which sounds tractable to me.