Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd be really eager to try that out.

e.g.:

- embedding a prolog/asp DSL: https://github.com/kiranandcode/cleango

- embedding a tex/latex DSL: https://github.com/kiranandcode/LeanTeX