Dependently typed languages can still develop a degree of biformity via 'tactic' languages. In Coq, for example, you have Gallina and Ltac, which are basically separate languages.

This occurs because even with an elegant theorem proving system, you eventually want proof search, and proof search = macros.

I'm not sure there is a way out.

That said, if dependently typed languages had passable ecosystems I'd use them as is. Not sure if that is more stubbornness than good sense.