How to write a coterminating, effectful program?
In these sorts of cases, one idiomatic way is to run it with gas, and to create one non-total gas value to let you finish the program. Yes, perhaps Idris should offer a combinator for IO that allows full streams to be run, but this is sufficient, and doesn't affect the validity of anything else.

Seeing this, I'd agree that the IO monad should be coinductive, not inductive.

%default total

data Gas : Type where
  More : Lazy Gas -&gt; Gas
  Done : Gas

runStream : Gas -&gt; Stream (IO ()) -&gt; IO ()
runStream (More g) (i :: is) = i &gt;&gt;= \_ =&gt; runStream g is
runStream Done _ = pure ()

partial
unbounded : Gas
unbounded = More unbounded