Lots of type systems support type inference. It seemed (I could have misinterpreted) like the OP was suggesting that in a perfect world all types would be inferred. That's the idea I was disagreeing with.
Normal type inference deduces the type from the code, Idris can infer the implementation from the type if the type is specific enough. In a way, this is Church in action: the type is a theorem, and the compiler is a proof assistant that helps to automatically find a proof (a correct program having that type).
So Idris is an argument supporting your position: if it works (it is still part of a research program), the types are the primary expression, and the code is secondary.
