I'm not an expert, but yes compile times can get crazy if you're not careful. In theory, the situation is no different from (ab)use of C++ templates, the Rust

I'm not an expert, but yes compile times can get crazy if you're not careful. In theory, the situation is no different from (ab)use of C++ templates, the Rust macro discussed here, and so on. In practice, whereas C and Rust will choke on a 100kloc function, Idris might choke on a 100-liner, depending on what you're doing. Edwin Brady is currently making steady progress on a new compiler--this time written in Idris itself--that's much faster in practice: https://github.com/edwinb/Idris2 https://github.com/edwinb/Idris2