But the real strength of Lisp is in the macros, the metaprogramming system. And I suspect that typing most macros properly would be a bit less trivial than even typing of complex generic types, like lenses. Not typing a macro, and only typechecking the macroexpansion would formally work, but, usability-wise, could be on par with C++ template error reporting.
I think we (the Clojure community) quickly figured out we don't really want static typing, which is a bit evident by the low uptake of Typed Clojure.
Personally I found it to A) make it a hassle for downstream consumers since your design is suddenly impacting others, because you can "lock things down" and B) have that very same effect on your own codebase, where it becomes a lot less flexible where it needs to be flexible.
Nowadays, I just use another language if I want static types, which happens sometimes but not nearly as often to say that dynamically typed languages are "dead" or whatever.
My point was that you could implement type checking with macros, not that you could type check macros. (Though that would be cool!) As opposed to having to change the language definition first (Python) or implement an entirely new compiler (TypeScript).
Certainly you can implement the typechecker with macros, but it should also work on macros, before expansion. That is, you likely want (-> ...) typechecked as written, not (only) as expanded, and typing errors reported on the non-expanded form.
Word. This is a problem of lisps in general, they loose information as the same "thing" traverse the various meta-layers that constitute the system. A parsed expression is not tied to its string, and the expansion of the expression, provided it is a macro, is not tied to the original expression. In the same vein: you can't easily find the source code of a lambda that was compiled/interpreted.
Of course you can do all of this, but you need to build it yourself: see rewrite-clj. If you want to build a clojure debugger that is able to display or refer to code with the same indentation the programmer is dealing with in his text editor, you need to bridge the gap between clojure expressiosn and their string representation.
Anyway I concur that reversible macros would be great. Tag the output, have those tags propagate to the input by playing the macro backwards. Complex stuff really. That's a job for category theory I guess.
But the real strength of Lisp is in the macros, the metaprogramming system. And I suspect that typing most macros properly would be a bit less trivial than even typing of complex generic types, like lenses. Not typing a macro, and only typechecking the macroexpansion would formally work, but, usability-wise, could be on par with C++ template error reporting.