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)
I think that "second-order lambda-calculus" usually refers to system F, which doesn't even have dependent types.
What I'm getting at is that there are plenty of parts of GHC's flavor of Haskell that you can't depend on type inference for. You have to give type signatures for polymorphic recursion, for instance.
[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)