[throwaway17_17]

I sort of glossed over the differences between macros and dependent types in another answer in this thread, but I'll expand on it here. Typically the term macros is used to imply one of two things (that may be used in the same instance of a macro):

1 - 'compile-time' code execution of some arbitrary code with the result of that execution then being available at run time

2 - a specific type of function which takes the AST of some language and then uses some procedural methodology to mutate/alter that AST transforming it into some other AST

I would say, that while dependent types can be a useful basis for covering several of the typical use cases of macros, they do not without some additional structure, provide a firm proof/type theory for the whole scope of macros.

I would suggest that the most sound attempts at describing the computational phenomena encapsulated by the most common usage of the term 'macro' would be found in the following: a) implementation of Temporal Logic (per Frank Pfenning's interpretation) for description of compile-time code execution and b) implementation of Modal Logic, describing multi-staged compilation, as in Davies and Pfenning

So, I would not say that dependent types can eliminate macros, but they do cover a chunk of the areas that are often implemented by macros, including generics and other type based compile time code patterns.