Interesting post. As a non-expert, I wondered whether dependent types fit here: macros extend what you can write, and dependent types could let the compiler check what those new constructs mean. Lean 4 does both, with user-definable syntax on a dependently typed core. Curious whether that influenced Sweetener at all.

score 1 · canonical