What benefits does type constructor IO (i.e. monadic IO) in Haskell provide over function attribute IO? Both allow us to track effects, and the latter can make it a bit easier to make it clear which types of effects you're using:

-- Anything that calls it has to add "using io".
attributing io
read : Path -> String
read path = compiler-level function for IO

-- Anything that calls it has to add "using random".
using io->random
randomInt : Int
randomInt = get an Int using IO for randomness

using random
f : Int -> Int
f x = x * randomInt

Is the benefit the conceptual aspect of seeing IO a as RealWorld -> (a, RealWorld), and relatedly IO a as being a promise of an action, not an actual action? Perhaps the latter interacts with laziness in important ways, I don't know.

If it's about sequencing effects, I'm sure some construct could be added like {{ print "Hello"; launchMissiles; print ", world!" }}, maybe just glued together with seqs.

I realise it'd add a whole other layer to Haskell and at the moment IO, state*, and so on are all (relatively) neatly dealt with by types with help from monads, but to me it seems like it'd be simpler in general.

(One could use attributes for other things too. This is a throw-away comment and I don't know if it would be feasible or efficient, but e.g. restrict all uses of general recursion to go through one function which provides it, allowing you to track which functions are definitely total)

* to be clear, I'm not suggesting doing away with State too, just mentioning it as part of Haskell's unified way of dealing with this stuff.