A language whose type level allows you to express arbitrary mathematical propositions can't possibly have as good inference as ML and Haskell have, because higher-order unification is known to be undecidable. Agda and Idris require manual type annotations for all let-bound identifiers. Coq requires all dependent pattern-matching blocks to be type-annotated. This is a real chore, and dependent types will never become mainstream unless their usability improves significantly.

What I have in mind is one way to hopefully achieve that “significant usability improvement”:

(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas.

(1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice.

But I don't see anyone in the FP community exploring this possibility.

I just got a bunch of papers on first-order verification, implementation, compilers, and so on as the simplicity & tractability part peaked my interest. I'm keeping them in case I run into some students or hobbyists that want to try that on top of some "verify the verifier" kind of issues. Then I see these suggestions...

"(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas.

(1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice."

I'll add those to the list given that sounds worth a good try. Especially if combined with automated approaches to generating & solving for common attributes like in SPARK and AutoCorres. Maybe something will come of it.