Well, TH does all its transformation at compile-time, and the output is fed to the type-checker then and there: if your macro produces ill-typed code, you learn about it quickly. Whereas in Lisp, as I understand it, macros can be invoked at runtime, causing type errors while the program's actually running.
I remember reading somewhere that some well-known theorem, possibly Rice's Theorem (http://en.wikipedia.org/wiki/Rice's_Theorem), implies that
it's impossible to write a static type system that catches all bugs;
the stronger you make your type system, the more valid code will be rejected.
. Hence the perfect static type system you want is actually impossible. It also seems to be the case that inference imposes a large cost on a type system: if you want your compiler to infer types, you're greatly limited in the features your type system can offer.
Re: I don't know about that
I remember reading somewhere that some well-known theorem, possibly Rice's Theorem (http://en.wikipedia.org/wiki/Rice's_Theorem), implies that
- it's impossible to write a static type system that catches all bugs;
- the stronger you make your type system, the more valid code will be rejected.
. Hence the perfect static type system you want is actually impossible. It also seems to be the case that inference imposes a large cost on a type system: if you want your compiler to infer types, you're greatly limited in the features your type system can offer.