class Protocol ps where

  -- | The messages for this protocol. It is expected to be a GADT that is
  -- indexed by the @from@ and @to@ protocol states. That is the protocol state
  -- the message transitions from, and the protocol state it transitions into.
  -- These are the edges of the protocol state transition system.
  --
  data Message ps (st :: ps) (st' :: ps)

  -- | Associate an 'Agency' for each state.
  --
  type StateAgency (st :: ps) :: Agency

  -- | A protocol state token, i.e. a term level representation of type level
  -- state (also known as a singleton).
  --
  type StateToken :: ps -> Type

-- | An association from type level states to term level 'StateToken's.
--
class StateTokenI (st :: ps) where
  stateToken :: StateToken st

-- using `QuantifiedConstraints`
class (forall (st :: ps). StateTokenI st) => Protocol ps where ...

data PingPong = Idle | Busy | Done
  deriving Typeable

data SingPingPong (st :: PingPong) where
  SingIdle :: SingPingPong Idle
  SingBusy :: SingPingPong Busy
  SingDone :: SingPingPong Done

instance Typeable st => StateTokenI (st :: PingPong) where
  stateToken =     case eqT @st @StIdle of
    { Just Refl -> SingIdle
    ; Nothing   -> case eqT @st @StBusy of
    { Just Refl -> SingBusy
    ; Nothing   -> case eqT @st @StDone of
    { Just Refl -> SingDone
    ; Nothing   -> error "impossible"
    }}}

data Channel m = Channel {

    send :: LBS.ByteString -> m (),

    recv :: STM m (Maybe LBS.ByteString)
  }

data Codec ps failure m bytes = Codec {
       encode :: forall (st :: ps) (st' :: ps).
                 SingI st
              => ActiveState st
              => Message ps st st'
              -> bytes,

       decode :: forall (st :: ps).
                 ActiveState st
              => Sing st
              -> m (DecodeStep bytes failure m (SomeMessage st))
     }

runDecoderWithChannel :: MonadSTM m
                      => Channel m bytes
                      -> Maybe bytes
                      -> DecodeStep bytes failure m a
                      -> m (Either failure (a, Maybe bytes))


tryRunDecoderWithChannel :: Monad m
                         => Channel m bytes
                         -> Maybe bytes
                         -> DecodeStep bytes failure m (SomeMessage st)
                         -> m (Either failure
                                (Either (DriverState ps pr st bytes failure (Maybe bytes) m)
                                        (SomeMessage st, Maybe bytes)))

data Driver ps (pr :: PeerRole) bytes failure dstate m =
        Driver {
          ...
          tryRecvMessage :: forall (st :: ps).
                            SingI st
                         => ActiveState st
                         => ReflRelativeAgency (StateAgency st)
                                                TheyHaveAgency
                                               (Relative pr (StateAgency st))
                         -> DriverState ps pr st bytes failure dstate m
                         -> m (Either (DriverState ps pr st bytes failure dstate m)
                                      ( SomeMessage st
                                      , dstate
                                      ))
        , -- | Construct a non-blocking stm action which awaits for the
          -- message.
          --
          recvMessageSTM :: forall (st :: ps).
                            SingI st
                         => ActiveState st
                         => ReflRelativeAgency (StateAgency st)
                                                TheyHaveAgency
                                               (Relative pr (StateAgency st))
                         -> DriverState ps pr st bytes failure dstate m
                         -> m (STM m (SomeMessage st, dstate))

        , startDState    :: dstate
        }

pingPongClientPeer :: Has (State Int) sig m 
                   => Peer PingPong AsClient m (At () StDone) StIdle
pingPongClientPeer = I.do
    -- ghc bug: https://gitlab.haskell.org/ghc/ghc/-/issues/22788 
    -- we can't use this: 
    -- i <- effect (get @Int) 
    -- if i > 10 
    --   then  ...
    --   else ...
    --
    effect (get @Int) I.>>= 
      \(At i ) ->
         if i > 10 
          then I.do
            yield (ClientAgency TokIdle) MsgDone
            done TokDone ()
          else I.do
            yield (ClientAgency TokIdle) MsgPing 
            effect $ modify @Int (+1)
            await (ServerAgency TokBusy) I.>>= \case
              MsgPong -> pingPongClientPeer

pingPongServerPeer :: Has (Lift IO ) sig m 
                   => Peer PingPong AsServer m (At () StDone) StIdle
pingPongServerPeer = Indexed.do 
    await (ClientAgency TokIdle) I.>>= \case
      MsgDone -> I.do 
        effect $ sendIO (print "recv MsgDone, finish")
        done TokDone ()
      MsgPing -> I.do 
        effect $ sendIO (print "recv MsgPing, send MsgPong")
        yield (ServerAgency TokBusy) MsgPong
        pingPongServerPeer

pingPongClientPeer' :: Has (State Int) sig m 
                   => Peer PingPong AsClient m (At () StDone) StIdle
pingPongClientPeer' = I.do
  At i <- effect (get @Int) 
  if i > 10 
   then I.do
     yield (ClientAgency TokIdle) MsgDone
     done TokDone ()
   else I.do
     yield (ClientAgency TokIdle) MsgPing 
     effect $ modify @Int (+1)
     await (ServerAgency TokBusy) I.>>= \case
       MsgPong -> pingPongClientPeer