I used macro expansion for type checking in Zeta-C [0], the first C compiler for Lisp Machines, in 1983. Didn't write a paper about it, though.

Dependent types are certainly interesting -- I'll give this a read. Thanks!

[0] http://bitsavers.trailing-edge.com/bits/TI/Explorer/zeta-c/