I recall once, not quite 20 years ago, porting a large CL program from a 32-bit implementation to one of the then-new 64-bit Lisps. Someone who didn't know CL thought that would be a hellish job, but it turned out to be quite straightforward.
Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf
Dependent Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/cbtb-popl2020.pdf
It's so cool - especially the bits where they reconstruct each part of the type system and show how each feature they add contributes to the power/capability of it. :D
Dependent types are certainly interesting -- I'll give this a read. Thanks!
[0] http://bitsavers.trailing-edge.com/bits/TI/Explorer/zeta-c/