One reason why Idris is its own language is that you can't just lie dependent types atop a language---that's the whole point, the types interact with the values

One reason why Idris is its own language is that you can't just lie dependent types atop a language---that's the whole point, the types interact with the values and the values the types. This blurs the boundary between compiler phases. Sometimes you get type erasure, but for really interesting programs to arise (the kind that I'm sure Idris is aiming at, though I don't know for certain) you really want to operate in that blurry divide.