As I understand it, one selling point of Idris' type system is that it's actually simpler than haskell as it's based on a single very generic concept that covers a wide range of applications, rather than a sum of specialized things.

There was some discussion previously on HN about this https://news.ycombinator.com/item?id=12350273

But type inference takes a hit. Trade offs -- conceptually similar but potentially needing more annotation

While dependent type inference is more difficult, you get program inference in exchange. That's not a bad tradeoff because I'd rather write the spec (type) and have the computer fill in the boring bits, rather than the other way around.

I remember seeing an Edwin Brady talk (it featured a now-possibly-famous Brexit joke) in which the compiler almost inferred ... I think it was either zip or a fold.

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.

Good Haskell style already presupposes top-level type annotations.

Highly generic code yields complicated signatures, so even if it's good style to add those signatures for top level declarations, it's really good to have the compiler help you figure out what that signature is.