> rather than using them to implement typing itself. I'm not sure what this means exactly. Those papers do use macros to implement extensible/pluggable static

> rather than using them to implement typing itself. I'm not sure what this means exactly. Those papers do use macros to implement extensible/pluggable static type systems just like those we use every day. The point is that the phase distinction is respected as macros run at compile-time. If your macro language roughly matches your value language, then this would look something like Zig, but more expressive, and the compilation output is a residual program that can run without types (although runtime type embeddings are also possible where needed). The problem I have with typing all of this is that I haven't yet found a satisfactory approach that doesn't explode into a typing zoo that's only usable for niche experts. Economy of mechanism is very important for wider adoption IMO. People can debug ordinary programs, so if your compiler runs your source program like an ordinary program, people can straightforwardly debug that too if this is designed well.