Syntax for Haskell do?

[asajeffrey]

Can we use Agda 2.2.8's syntax mechanism to define a binder similar to Haskell's do?

[treep]

One can write something like this:

module IOTest where

open import System.IO

infixl 1 _<_
infixr 1 bind
infixr 2 _!_

_<_  = _>>_
_!_  = _>>_
bind = _>>=_
do   = skip

syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂

main = do
  < s ← getStr
  , putStr "Hi, "
  ! putStr s
  ! putStr "!\n"
  < m ← getStr
  , putStr m

it's similar, but unfortunately includes all these random characters.