> Idris provides tools I can see as useful, things like checking at compile time all file handles are correctly opened before use, and closed after use (that's a very simple example, but just one type of thing you can do)
Tracking state (sort of like Typestate) is not part of the type system, but you can encode it in the type system. So far, I've found this much more usable in practice than linear types, but I expect future work on linear types will change this, especially now that they're coming to GHC.
AFAIK that sounds like unique/linear types, which Idris doesn't provide at this point, it's an experimental/work in progress feature: http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...