> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs.

AIUI, dependently-typed languages don't really have a fixed phase distinction between "compile time" and "run time". The type checking pass can involve execution of "run time" code (this is one way to understand why these languages are generally not Turing complete), and "run time" code may be required to somehow build complex code like a JSON parser "on the fly", depending perhaps on user input.

In practice, some systems have a "code extraction" component that's intended to filter out the "irrelevant" parts of the code and transpile it to a conventional programming language, which obviously reintroduces a separate "run time" deployment step. This could definitely be done using, e.g. Rust, provided that the issues due to a lack of general GC in that language are addressed too.