Как правильно использовать нотацию `do` с IO Agda-stdlib?

Question

Я пытаюсь использовать do-notation вместе с IO из agda-stdlib, но, как ни странно, тип _>>_ использует ∞: {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A.Из-за этого мне нужно чередовать ♯ s между приложениями, но это делает использование неудобным.Например, ♯ s необходимы для создания программы, которая печатает строку:

main : IO ⊤
main = do
  ♯ (putStrLn "hi")
  ♯ (return tt)

Более того, расширение его с помощью большего количества строк не проверяется.Я должен отказаться от do-notation, вот так:

main : IO ⊤
main = 
  ♯ (♯ putStrLn "hi" >> 
    ♯ putStrLn "ho") >>
    ♯ return tt

Что выглядит ужасно.Я мог бы переопределить _>>_ и _>>=_:

_>>_ : {A : Set} {B : Set} (m₁ : (IO B)) (m₂ : (IO A)) → IO A
_>>_ a b = (♯ a) IO.>> (♯ b)

Но я предполагаю, что это не то, что я должен делать.Итак, я что-то упустил?Как правильно его использовать?

Answer 1

Реализация IO в стандартной библиотеке предшествует добавлению примечания do в Agda, поэтому оно не было написано с учетом примечания do. Agda prelude Ульфа имеет более современную реализацию IO, которая поддерживает примечание do.