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

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.