I've seen this over and over but it's false. Adding dependent types do not negatively affect type inference for the non-dependent fragment in any shape or form.

I've seen this over and over but it's false. Adding dependent types do not negatively affect type inference for the non-dependent fragment in any shape or form. On the contrary, Agda/Coq type inference is far more powerful than in Haskell. While Agda/Coq do not have let generalization, that is by purely a design decision and not some kind of limitation.