In general, dependently typed systems lack the ability to metaprogram at the syntactic level. This is particularly true we’re binding forms are concerned. The most thoroughly pursued type theoretic way to do this is to implement a modal type system, which is technically orthogonal to the dependency capabilities of the type system, but integration of the two is tricky.