Note that I don't think there's really a better story out there for async exceptions - which are necessarily able to interrupt (almost) any bit of your computat

Note that I don't think there's really a better story out there for async exceptions - which are necessarily able to interrupt (almost) any bit of your computation. Ideally we may be able to make assertions about stack or heap overflow (especially for a non-Turing complete fragment of the language), but I'm not sure whether Idris is able to provide that. "ThreadKilled" and "UserInterrupt" are inherently unrelated to local program flow. For synchronous exceptions Haskell is sort of middle-of-the-road, differing from other languages mostly in providing other options that are substantially better for many use cases.