> Checked exceptions would be neat but still, if you don't catch the exception it will be propagated further up the chain, so the claim that it is impossible to create an unopened file handle still holds :)

True, but introducing invisible partiality to essentially all functions is a pretty stiff cost.

> Yes, object lifetime management is not provably safe in c++, due to lack of borrow checker, but that's a general problem for all types of objects, not specifically file management.

Well, that's a question of language design philosophy. Object management is so much more frequent than any other kind of resource management that it may be worth treating as a special case, as most languages other than C++ do.

Be that as it may, the point is that the really cool thing about Idris is that its type system is powerful enough to let you implement borrow-checker-like functionality in "userspace" rather than needing it built into the language. In theory one could use that (in an Idris-like language with a different record feature, standard library and so on) to have Rust-style manual-but-safe memory management for all objects, though I suspect that might be too cumbersome to be practical.