Большинство моих макросов стали const и static

Логику держат вне раскрывателя ради переопределения. Макрос, который раскрывается в вызов обычной функции, даёт маленькое раскрытие, а функцию можно переопределить и протестировать, не трогая вызывающий код. Если же логика сидит внутри раскрывателя, каждое место использования макроса хранит то, что раскрыватель выдал при компиляции этого места. Тогда изменение логики требует найти и перекомпилировать эти места, а у читателя программы нет записи о том, какие они. Код на Common Lisp обычно следует такому разделению именно поэтому.

Согласен наполовину. В C++ шаблон одновременно и макрос, и обобщённый тип, так что «держать маленьким» тут толком не выйдет. Можно вынести из него работу. Большая часть старого метапрограммирования теперь это функции constexpr, то есть просто функции, с циклами и if, которые вычисляются при компиляции, когда этого требует контекст. Если хочется настоять, есть consteval.

Выбор перегрузки по тому, что умеет тип, достался концептам. template <std::integral T> падает в месте вызова с сообщением о невыполненном ограничении, а не тремя экранами провала подстановки из глубин библиотеки. Не всегда коротко. Короче.

Историческая сноска. CoffeeScript был в каком-то смысле одним большим фиксированным макросом над JavaScript. Толстые стрелки, классы, деструктуризация, аргументы по умолчанию, сплаты, интерполяция строк. Добавить свой сахар никто не мог, компилятор привозил всё сам. Потом почти всё это вошло в язык с ES2015, иногда с тонко отличающейся семантикой (=> в CoffeeScript в скомпилированном коде захватывал this из объемлющей области, а у стрелочной функции ES своей привязки this нет вовсе, снаружи выглядит одинаково, но механизм другой).

Это мой довод за маленькие макросы с другой стороны. Сахар, который себя оправдал, обычно повышают до языка. Если макрос маленький, слезть с него потом дёшево.

В Agda нет отдельного языка времени компиляции, который надо держать маленьким, и это звучит прекрасно, пока не приходит счёт. Проверка типов нормализует термы, так что вычисление во время компиляции это просто вычисление, и там может выполняться всё тотальное. Цена в том, что тотальность проверяют. Проверка завершаемости хочет рекурсии по структурно меньшим аргументам, и вполне разумную функцию с рекурсией по n / 2 отвергнут, пока не перепишешь её через фундированную рекурсию или аргумент-топливо. Честно говоря, переписанный вариант бывает длиннее самой функции.

Макросы в Agda есть, через рефлексию, но мне они почти никогда не нужны. Когда проверка типов и так исполняет код, макросу мало что остаётся.