> Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program.

> You can recover a sort of phase distinction

Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like System F will have the same erasure.

> inherently involve a kind of compile-time evaluation.

compile-time evaluation doesn't pose a phase-separation problem. Indeed, nothing to the right of a `:` will ever need to be evaluated on runtime.