We would need to add the following instance to fix this example
```lean
instance ExceptT.monadIO {σ} (m : Type → Type) [Monad m] [MonadIO m] : MonadIO (ExceptT σ m) := {}
```
However, this instance may create problems for polymorphic functions on
`MonadIO m`. If `m` is of the form `ExcepT Except1 ... EIO Exception2`,
then `finally` and `catch` is catching `Except1`. This is particularly
bad for code that uses `finally`.
Right now, we are not using monad stacks with multiple `ExceptT`s for
performance reasons, but we should have a solution for users.
eec12232e3