Reference counting would go a long way though as there is very little mutation in a typical Idris program, so you could probably sew something together in Rust

Reference counting would go a long way though as there is very little mutation in a typical Idris program, so you could probably sew something together in Rust with Rc cells and a simple cycle detector. 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.