Let-binding intermediate results in IO monad

Question

Given this context:

open import IO
open import Data.String
open import Data.Unit
open import Coinduction

postulate
  A : Set
  f : String → A
  g₁ g₂ : A → String

let's say I want to implement something like

foo : IO ⊤
foo = ♯ readFiniteFile "input.txt" >>= \s →
      ♯ (♯ putStrLn (g₁ (f s)) >>
      ♯ putStrLn (g₂ (f s)))

by let-binding the intermediate result f s. I was hoping this would work:

foo₁ : IO ⊤
foo₁ = ♯ readFiniteFile "input.txt" >>= \s →
       let x = f s in
       ♯ (♯ putStrLn (g₁ x) >>
       ♯ putStrLn (g₂ x))

but this fails with

Not implemented: coinductive constructor in the scope of a let-bound variable

so I tried moving out the ♯:

foo₂ : IO ⊤
foo₂ = ♯ readFiniteFile "input.txt" >>= \s →
       ♯ (let x = f s in
       ♯ putStrLn (g₁ x) >>
       ♯ putStrLn (g₂ x))

same problem as before.

I managed to get around this by just lifting out the ♯ening step:

_>>′_ : ∀ {a} {A B : Set a} → IO A → IO B → IO B
m >>′ m′ = ♯ m >> ♯ m′

foo₂ : IO ⊤
foo₂ = ♯ readFiniteFile "input.txt" >>= \s →
       ♯ let x = f s in
       putStrLn (g₁ x) >>′ putStrLn (g₂ x)

but why does that work if the "inlined" version doesn't?

Answer 1

FYI, this problem was a long standing one and as I was having a look at it today, I noticed that it had been fixed just a few days before you asked your question. The fix is part of the currently released version (version 2.5.1.1).