I'm not sufficiently familiar with Idris to comment -- I will learn Idris in the future, hopefully in December.
Be that as it may, I'm somewhat sceptical of implementation inference: after all, you need to give a spec, exactly the thing you typically do not have in large-scale software engineering. The spec emerges at the end and often the program is the spec itself. Moreover, as far as I gather, implementation inference works by program synthesis, and unless Brady has had a massive breakthrough here, that's an exponential search process, so it won't scale much beyond inferring small programs like the zip function. (Still I think implementation inference is a useful tool- but it's not magic.)
Be that as it may, I'm somewhat sceptical of implementation inference: after all, you need to give a spec, exactly the thing you typically do not have in large-scale software engineering. The spec emerges at the end and often the program is the spec itself. Moreover, as far as I gather, implementation inference works by program synthesis, and unless Brady has had a massive breakthrough here, that's an exponential search process, so it won't scale much beyond inferring small programs like the zip function. (Still I think implementation inference is a useful tool- but it's not magic.)