It's almost a meme at this point, but the solution, of course, is algebraic effects. Among other things they let us implement checked exceptions, but in a sane way that's safe without requiring the annotation of every single function.

https://www.microsoft.com/en-us/research/wp-content/uploads/...