Type inference in idris works well if the types of the terms in question are non dependent. The moment you introduce complicated types, type inference suffers, which is expected because even idris cannot break the fundamental nature of logic.
Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.
