[Agda] sequencing 3 IO operations

[Jeremy Shaw]

Hello,

I realize I am in uncharted territory here, but I am wondering how to  
improve the sequencing of three IO operations. If you have:

foo2 : IO ⊤
foo2 =
    ♯ putStrLn "foo 1" >>
    ♯ putStrLn "foo 2"

Everything is fine. But if you try to extend it to three:

foo3 : IO ⊤
foo3 =
    ♯ putStrLn "foo 1" >>
    ♯ putStrLn "foo 2" >>
    ♯ putStrLn "foo 3"

It does not typecheck.
If we look at the definition for >>:

data IO : Set → Set₁ where
   lift   : ∀ {A} (m : Prim.IO A) → IO A
   return : ∀ {A} (x : A) → IO A
   _>>=_  : ∀ {A B} (m : ∞ (IO A)) (f : (x : A) → ∞ (IO B)) →  
IO B
   _>>_   : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → IO B


we see that >> returns an IO B value. So we can't do

   (♯ a >> ♯ b) >> ♯ c

Instead we need an extra, ♯

  ♯ (♯ a >> ♯ b) >> ♯ c

Well, that gets ugly pretty fast. Is there any obvious work around ?

Here is a complete example (using Agda and lib from darcs head):
module IOIOIO where

open import Coinduction using (♯_)
open import Data.Unit using (⊤)
open import IO using (IO; _>>_; putStrLn; run)
import IO.Primitive as Prim

foo4 : IO ⊤
foo4 =
    ♯ putStrLn "foo 1" >>
    ♯ (♯ putStrLn "foo 2" >>
       ♯ (♯ putStrLn "foo 3" >>
          ♯ putStrLn "foo 4"))

main : Prim.IO ⊤
main = run foo4