Speaking more generally, one of the desiderata when designing a dependent type system is to set things up so that type checking is a simpler problem than unrestricted theorem proving. Of course, if you want to prove an arbitrary theorem that can be arbitrarily hard, but that has nothing to do with using dependent types.
Type checking may be decidable in Coq but now the user has to do the work of putting things into a form that type checks. You're just pushing the problem elsewhere. Even for trivial Coq programs you have to write a large number of proofs compared to how much code you wrote.
> Speaking more generally, one of the desiderata when designing a dependent type system is to set things up so that type checking is a simpler problem than unrestricted theorem proving.
Do you know of any examples of this? I know DML limits you to linear arithmetic so type checking is decidable but that's a big limitation. All other languages like Coq, Idris and Agda require you to write proofs.
Dependent types allow you to express things such as `a == b` as a type, and proving that requires some work, but you don't need any of that at all. Idris is a superset of Haskell, you may say.
Even that quickly becomes undecidable as non-linear arithmetic is undecidable.