[colorint]

>without macros

Type systems are macro systems, it's just not obvious because type languages are very different from expression languages. The main "innovation" of Idris is hammering harder on this front. And in any case, the fact that most type languages are logic languages gives people with a formalist bent a warm feeling in their stomachs.

[dllthomas]

There's a valid perspective from which type systems are particularly-constrained macro systems. That doesn't mean there aren't contexts where it's useful and/or interesting to distinguish. But if you wish, pretend I had written "traditionally conceived general purpose macros" :)