A common language for dependently-typed programming?

The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types.

1. Epigram
2. ATS (successor to Dependent ML and Xanadu)
3. Agda (successor to Cayenne)
4. Ωmega
5. NuPrl
6. Twelf
7. Isabelle
8. Coq
9. Delphin
10. Concoqtion
11. Aldor
12. Guru (successor to RSP1)

And now, a list of caveats about the above list:

• Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq.
• This list does not include several languages that are new or new variants (PIE, Matita), not checked at compile-time (Sage), or not actively maintained (most proof assistants, Charity).
• Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Aldor can't understand most type equalities, making its dependent types somewhat weak, though Atypical and Aldor-- aimed to remedy this five years ago. Agda and Epigram have New Exciting Versions 2 coming out, so they suffer from the Osborne Effect.

Is it time yet to do anything about the cornucopia of options? When Haskell began, there were many similar options; the list above is heterogeneous. Is that because it's too early in to tell what the Right choices will be? Is this problem fundamentally harder than the one that inspired the Haskell precursors?

I'm not sure, though deciding how to ensure termination seems particularly tricky. Nonetheless, there are other decisions that aren't as directly related to the central dependent type issues, like syntax, functional purity (though this is related to termination), and editing environment. Maybe these issues will divide the ecosystem into a few niches, each dominated by one player. In the meantime, it's tough to choose.