That is not the only reason to have an IO monad. PureScript and Idris are both strict languages that still reify IO effects. Its still useful to know which functions are pure.
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.
I'm not a Haskeller but I would like to use a language that indeed separates all code into two areas, one in which I can write non-pure functions and one in which I can not.
That would obviously make it easier to analyze and test and verify the program by first focusing on the pure part of it, then on the impure part. I'm not sure if that is possible in "strict languages" but perhaps.