Needing tests != Unit Tests.
Adding larger system tests after the fact is perfectly reasonable. TDD wants you to write tiny tests for every square millimeter of functionality. It's just not worth it, and 99% of the value is to make up for shortcomings in dynamic languages.
Idris is carefully and purposefully described by its creators as not production ready. Nonetheless, because of what Idris is, it’s arguably more production-ready than languages which don’t even attempt formal soundness to anywhere near the same degree. In other words: Idris is not a complete Idris. But! All the other languages are even less complete Idrises!
Big old “personal opinion” disclaimer here though. –Let’s prove it’s not possible to use Idris by doing it! Shall we?
I agree with Jim Coplien when he argues that most unit testing is waste. And TDD is even worse, because it is equivalent to designing a complex system purely from the bottom up, in miniature steps.
What fool uses TDD to design? The second "D" is "Development". If people want to act foolishly, let them. Then come in later and make money cleaning up their mess.
There is a small scale design benefit to writing tests, and that is simply that you always have a "user" of your code, even if it's only focused on tiny bits of it.
But having said that, I get essentially the same design benefit from writing tests afterwards, or writing a test client, or writing user documentation. I usually discover code needs some design improvement once I have to explain or use it.