I'm actually not a fan of Idris' implementation of the IO monad, it really should have been a free monad with a cofree comonad so you can enforce invariants against the world without a bunch of extra machinery. It seems kind of important for a dependent type system.

I quite like Mercury's non-monadic linear IO + determinism semantics. You can subtype the world with insts and unify against the world-state pretty easily.