One of the most important lessons learned by the Haskell community is that we shouldn't worry about whether complete type inference is possible. We should worry about whether type inference can be maintained in the easy cases, while falling back to explicit annotation for the hard cases. All of rank-n types, GADTs, type families, even basic type classes, break complete type inference. The solution has always been to document the limitations, draw as clear a line in the sand as possible, and then go on and introduce those features. This doesn't affect the usability of the language.
What does affect the usability of the language is when (a) the line in the sand isn't very clear from an end-user point of view [see simplified subsumption in GHC 9, for example], or (b) the line is on the wrong side of simple features [see monomorphic local bindings, for example].
I guess what I'm saying is that Idris having minimal type inference is kind of terrible, and the excuse that it's not decidable for dependent types is a flimsy one.
What does affect the usability of the language is when (a) the line in the sand isn't very clear from an end-user point of view [see simplified subsumption in GHC 9, for example], or (b) the line is on the wrong side of simple features [see monomorphic local bindings, for example].
I guess what I'm saying is that Idris having minimal type inference is kind of terrible, and the excuse that it's not decidable for dependent types is a flimsy one.