I was thinking of rust specifically because of GC, I don't know how to write a GC and I don't even want to try. But if I use rust, I won't have to because of rust's zero cost abstractions.
If you're producing code for a collected language, you can forward on all of the allocations to that language, and if not, you will need to implement one.
Zero-cost abstractions or not, Idris needs a GC from somewhere.
But basically, having true closures requires some kind of GC. That was already recognized in Steele's Lambda papers in the 70s. Rust has to make compromises with its closures to avoid that.