Also, using a type checker to wholly check your Lisp code basically makes it a static language, the difference then is pretty much philosophical I'd say.
I'd rather avoid someone forcing me into using a hardcoded type system, among other reasons because I'm contemplating a (perhaps novel?) search-based program/expression-manipulating system that wouldn't play well with any fixed typing system. For one thing, the types of expression results (being return values of operators applied to input expressions or programs) can easily be emergent (is the resulting expression linear? Is it an odd function? Is it analytically integrable? Etc.) and not easily arrived at in something ML-like. If I had to use something like Haskell, I'd still be rolling out my own type system/prover on top of the existing language implementation anyway. However, types in general (as something you can compute with in the meta-program) would be absolutely mandatory for a system like this (for example, some algorithms or operations can have more desirable refinements that work only on subsets of values - consider determinants of triangular matrices, with triangular matrices being an emergent type - and I absolutely want to find out if such a thing is available for the specific problem being transformed), just not types that any specific existing language offers, to my knowledge.
So it's not that I dismiss the notion of proving things about programs - that is a vital thing to have - but the ability to impose restrictions on a program from the outside seems much more flexible to me than going for some fixed type discipline that could force me to straddle inconvenient fixed walls in the structure of a complicated program (such as this transformation system that would search the tree of possible transformations for a result with some desirable properties, with the transformations concisely expressed in some very-high-level DSL source code).