Type inference for higher-order dependent types is undecidable[1]. Going higher up the ladder of "polymorphism orders" one would eventually have to sacrifice Haskell's type inference -- which, I'm sure, few want to: otherwise, a lot more people would have programmed in Coq already.

[1] J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994. (Shamelessly copied from Wikipedia)