I have no experience with Idris or dependent types, so I may be completely wrong.
But from my understanding, a dependent type system allows for types to include values (which are evaluated at compile-time).
If so, then you might not even need macros at all to create the "," behavior.
Instead, you create a typeclass which will dispatch to the appropriate behavior:
data Pair a b = pair a b
interface Comma a b c where
comma : a -> b -> c
Comma Type Type Type where
comma = Pair
Comma a b (Pair a b) where
comma = pair
Now whenever you use the "comma" function, it will dispatch depending on whether its arguments are Types or not:
And since types may include arbitrary expressions, you can of course use the "comma" function inside of a type:
foo : a -> b -> (comma a b)
Note: all of the above code is completely untested and probably wrong, but you get the idea.
Basically, your language needs first-class types, and the ability to run arbitrary expressions at compile-time (even within types), and then you can use an ordinary typeclass to get the desired type dispatch. No macros needed.
"If so, then you might not even need macros at all to create the "," behavior."
I never said the overloading of "," was accomplished with macros.
The example I gave was of a macro whose name was overloaded in a type-directed way, similarly to the way "," is overloaded in Idris. (Maybe the macro itself is named ",".) My point is that if the macro system is designed to support that kind of overloading, then sometimes a macro call will depend on intermediate results obtained by the typechecker, so we can't run the macroexpander in a phase of its own.
---
For the sake of remembering Idris more accurately, I checked out the Idris docs to look for the particular "macro system" I was dealing with.
It turns out what I mean by the "macro system" in Idris is its system of elaborator extensions (http://docs.idris-lang.org/en/latest/reference/elaborator-re...). The elaborator's purpose is to fill in holes in the program, like the holes that remain when someone calls a function without supplying its implicit arguments.[1]
It's pretty natural to handle name overloading in the same phase as implicit arguments, because it's effectively a special case. Thanks to dependent types and implicit arguments, instead of having two differently typed functions named (,), you could have one function that implicitly takes a boolean:
(,) : {isType : Bool} ->
if isType then (... -> Type) else (... -> (a, b))
(,) = ...
The elaborator phase is complex enough that I don't understand how to use it yet, but I think almost all that complexity belongs to implicit arguments. Name overloading is probably seamless relative to that.
Another "macro system" I encountered in the docs was Idris's system of syntax extensions (http://docs.idris-lang.org/en/latest/tutorial/syntax.html). As far as I can tell, these apply before the elaborator and typechecker, but they might not be able to run arbitrary code or break hygiene. Maybe someday they'll gain those abilities and become a Nulan-like macro system.
[1] Implicit arguments effectively generalize type classes. Idris still has something like type class declarations, which it calls "interfaces," but I bet this is primarily so a programmer can define the interface type and the method lookup functions together in one fell swoop.
