I think a good design would involve stage polymorphism, but it does need to be the kind of polymorphism that preserves the distinction rather than just smooshing stages together or having ad-hoc special cases. (I've gone through this in the past, with Java 1.2 style types vs untyped vs typed with polymorphism, or more recently with the "function colouring" debate; Rust-style linearity is heading in the same direction too).

As far as I can see from a quick skim your links are one meta level up, about using macros to implement a type system for a DSL (which may have polymorphism and the like within that DSL) rather than using them to implement typing itself. There's still a distinction between types and macros, it's just that macros are being used to process types.

> 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.