I'm certain that this can be modelled using dependent types (after all, anything can), but I can't think of a way to do it that's anywhere near as ergonomic as Rust.
Mandatory GC is not a zero-cost abstraction (it is ridiculously inefficient and unnecessary in general), and a language with mandatory GC is a non-starter as a universal language. C programs (like web browsers) are starting to have new code written in a different language only now that Rust is available as the first zero-cost non-GC safe language.
Yes, dependent types improve performance by eliding checks, but that's only likely to be a net win if the rest of the compilation is optimal.
Even more, the performance limitations of most GC languages have more to do with the lack of good ways of writing code which simply doesn't allocate, rather then the problem of collection. GCs are often faster than malloc/free, but not as fast as simply not allocating/freeing anything.
Finally, it's important to remember that there are algorithms that are significantly more difficult to implement without a GC tahn with a GC. Even simple compare-and-swap atomic sets can require many times more code and care to implement if you have to handle cleanup of temporaries as well.
malloc/free is fast with a moving GC, but moving is not, and if an object is never moved it's likely that it should not have been allocated on the heap in the first place.
The cmpxchg problem is solvable by epoch-based reclamation libraries (RCU, crossbeam-epoch, etc.), and while a traditional GC also solves it, it's not necessary.
You don't need linear types for in-place updates. You can use a monad (which is another thing you can easily do with dependent types) to express the side effect of doing mutations. Then you can compile that monadic Coq code to Haskell, which then compiles to efficient machine code that actually does in-place updates.
Though, perhaps it is also worth mentioning that Idris 2 has both linear types and dependent types.
Regarding the need for automatic memory management: yes, most dependently typed languages have a garbage collector, but many "real" programming languages have garbage collectors and programmers are still happy to use them. I don't know why everyone in this thread is so concerned about performance. Dependently typed code can compile to reasonable machine code without any stretch of the imagination.
> Also it's not enough to erase irrelevant types, the types that end up in the program also need to be treated efficiently, which means generic monomorphization, not auto-boxing things unless essential (or ideally never), using computed layouts where possible (i.e. store (n, [T; n], [T; n]) in a single allocation if n is immutable), etc.
Memory layout is certainly something that needs to be dealt with, but compilers can monomorphize where possible to generate fast code with unboxed types in many cases. I don't think this is the main blocker for dependent types. I've written dependently typed code that easily outperforms the dynamically typed code I write for production at work (by at least an order of magnitude). In fact, dependent types can be used to guarantee that certain things don't need to be checked at runtime, which can in some cases give even better performance than what you'd get in a regular old statically-typed language.