diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,6 @@
 # Revision history for typed-session
+## 0.2.0.0
+* Remove data Recv
 
 ## 0.1.1.0
 * add protocol TH
diff --git a/src/TypedSession/Codec.hs b/src/TypedSession/Codec.hs
--- a/src/TypedSession/Codec.hs
+++ b/src/TypedSession/Codec.hs
@@ -21,7 +21,7 @@
 newtype Encode role' ps bytes = Encode
   { encode
       :: forall (send :: role') (recv :: role') (st :: ps) (st' :: ps) (st'' :: ps)
-       . Msg role' ps st '(send, st') '(recv, st'')
+       . Msg role' ps st send st' recv st''
       -> bytes
   }
 
diff --git a/src/TypedSession/Core.hs b/src/TypedSession/Core.hs
--- a/src/TypedSession/Core.hs
+++ b/src/TypedSession/Core.hs
@@ -72,15 +72,25 @@
 Describe the state of each role when it terminates.
 
 @
-data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))
+data
+  Msg
+    role'
+    ps
+    (fromSt :: ps)
+    (sender :: role')
+    (senderNewSt :: ps)
+    (receiver :: role')
+    (receiverNewSt :: ps)
 @
 * role': the type of the role.
 * ps: the type of the state machine.
-* ​​from: when sending a message, the sender is in this state,
+* ​​fromSt: when sending a message, the sender is in this state,
 where the receiver may be in this state, or a more generalized state related to this state.
 For example, the sender is in state (S1 [True]), and the receiver is in state (S1 s).
-* sendAndSt: the role that sends the message and the state of the role after sending the message.
-* recvAndSt: the role that receives the message and the state of the role after receiving the message.
+* sender: the role that sends the message
+* senderNewSt: the state of the role after sending the message
+* receiver: the role that receives the message
+* receiverNewSt: the state of the role after receiving the message
 
 There are two principles to follow when designing the state of Msg:
 
@@ -101,20 +111,15 @@
 -}
 class (SingToInt role', SingToInt ps) => Protocol role' ps where
   type Done (sr :: role') :: ps
-  data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))
-
-{- |
-Package Msg and extract the required type.
-
-@
-Msg  role' ps from '(send, sps) '(recv,     rps)
-Recv role' ps                     recv from rps
-@
--}
-data Recv role' ps recv from to where
-  Recv
-    :: Msg role' ps from '(send, sps) '(recv, rps)
-    -> Recv role' ps recv from rps
+  data
+    Msg
+      role'
+      ps
+      (fromSt :: ps)
+      (sender :: role')
+      (senderNewSt :: ps)
+      (receiver :: role')
+      (receiverNewSt :: ps)
 
 {- |
 Messages received from the outside are placed in MsgCache. When interpreting
@@ -132,13 +137,13 @@
        , SingToInt role'
        , SingToInt ps
        )
-    => Msg role' ps st '(send, st') '(recv, st'')
+    => Msg role' ps st send st' recv st''
     -> AnyMsg role' ps
 
 msgFromStSing
   :: forall role' ps st send recv st' st''
    . (SingI recv, SingI st)
-  => Msg role' ps st '(send, st') '(recv, st'')
+  => Msg role' ps st send st' recv st''
   -> Sing st
 msgFromStSing _ = sing @st
 
@@ -178,7 +183,7 @@
      , SingI from
      , SingToInt ps
      )
-  => (Recv role' ps recv from ~> Peer role' ps recv m ia)
+  => (Msg role' ps from send sps recv ~> Peer role' ps recv m ia)
   -> Peer role' ps recv m ia from
 @
 
@@ -194,7 +199,7 @@
        , SingI from
        , SingToInt ps
        )
-    => Msg role' ps from '(send, sps) '(recv, rps)
+    => Msg role' ps from send sps recv rps
     -> Peer role' ps send m ia sps
     -> Peer role' ps send m ia from
   Await
@@ -202,7 +207,7 @@
        , SingI from
        , SingToInt ps
        )
-    => (Recv role' ps recv from ~> Peer role' ps recv m ia)
+    => (Msg role' ps from send sps recv ~> Peer role' ps recv m ia)
     -> Peer role' ps recv m ia from
 
 instance (Functor m) => IMonadFail (Peer role' ps r m) where
@@ -232,7 +237,7 @@
      , SingI from
      , SingToInt ps
      )
-  => Msg role' ps from '(send, sps) '(recv, rps)
+  => Msg role' ps from send sps recv rps
   -> Peer role' ps send m (At () sps) from
 yield msg = Yield msg (returnAt ())
 
@@ -245,7 +250,7 @@
      , SingI from
      , SingToInt ps
      )
-  => Peer role' ps recv m (Recv role' ps recv from) from
+  => Peer role' ps recv m (Msg role' ps from send sps recv) from
 await = Await ireturn
 
 {- |
diff --git a/src/TypedSession/Driver.hs b/src/TypedSession/Driver.hs
--- a/src/TypedSession/Driver.hs
+++ b/src/TypedSession/Driver.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NumericUnderscores #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -10,7 +11,6 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-unused-do-bind #-}
-{-# LANGUAGE NumericUnderscores #-}
 
 {- |
 Schematic diagram of the communication structure of three roles through typed-session:
@@ -56,7 +56,7 @@
          , SingToInt role'
          )
       => Sing recv
-      -> Msg role' ps st '(send, st') '(recv, st'')
+      -> Msg role' ps st send st' recv st''
       -> m ()
   , recvMsg
       :: forall (st' :: ps)
@@ -85,12 +85,12 @@
     -> m a
   go (IReturn (At a)) = pure a
   go (LiftM k) = k >>= go
-  go (Yield (msg :: Msg role' ps (st' :: ps) '(r, sps) '(recv :: role', rps)) k) = do
+  go (Yield (msg :: Msg role' ps st' r sps recv rps) k) = do
     sendMsg (sing @recv) msg
     go k
-  go (Await (k :: (Recv role' ps r st' I.~> Peer role' ps r m ia))) = do
+  go (Await (k :: (Msg role' ps st' send sps r I.~> Peer role' ps r m ia))) = do
     AnyMsg msg <- recvMsg (sing @st')
-    go (k $ unsafeCoerce (Recv msg))
+    go (k $ unsafeCoerce msg)
 
 {- |
 A wrapper around AnyMsg that represents sending and receiving Msg.
@@ -158,7 +158,7 @@
        , SingToInt role'
        )
     => Sing recv
-    -> Msg role' ps from '(send, st) '(recv, st1)
+    -> Msg role' ps from send st recv st1
     -> m ()
   sendMsg role msg = liftFun $ do
     case IntMap.lookup (singToInt role) sendMap of
diff --git a/src/TypedSession/TH.hs b/src/TypedSession/TH.hs
--- a/src/TypedSession/TH.hs
+++ b/src/TypedSession/TH.hs
@@ -231,8 +231,10 @@
                   , ConT roleName
                   , ConT protName
                   , tAnyToType s a
-                  , typeListT [PromotedTupleT 2, PromotedT (mkName (show from)), tAnyToType s b]
-                  , typeListT [PromotedTupleT 2, PromotedT (mkName (show to)), tAnyToType s c]
+                  , PromotedT (mkName (show from))
+                  , tAnyToType s b
+                  , PromotedT (mkName (show to))
+                  , tAnyToType s c
                   ]
           let val =
                 let gadtc =
@@ -256,35 +258,40 @@
   instMsgDesc <- mkDataInstanceMsg ssVar (msgT1)
   fromVar <- newName "from"
   sendVar <- newName "send"
+  sendNewStVar <- newName "sendNewSt"
   recvVar <- newName "recv"
+  receiverNewStVar <- newName "receiverNewSt"
   let instanceMsg =
         [ InstanceD
             Nothing
             []
             (AppT (AppT (ConT ''TSC.Protocol) (ConT roleName)) (ConT protName))
             ( instDoneDesc
-                ++ let ct1 = (AppT (AppT (TupleT 2) (ConT roleName)) (ConT protName))
-                    in [ DataInstD
-                          []
-                          ( Just
-                              [ KindedTV fromVar () (ConT protName)
-                              , KindedTV sendVar () ct1
-                              , KindedTV recvVar () ct1
-                              ]
-                          )
-                          ( typeListT
-                              [ ConT ''TSC.Msg
-                              , ConT roleName
-                              , ConT protName
-                              , (SigT (VarT fromVar) (ConT protName))
-                              , (SigT (VarT sendVar) ct1)
-                              , (SigT (VarT recvVar) ct1)
-                              ]
-                          )
-                          Nothing
-                          instMsgDesc
-                          []
-                       ]
+                ++ [ DataInstD
+                      []
+                      ( Just
+                          [ KindedTV fromVar () (ConT protName)
+                          , KindedTV sendVar () (ConT roleName)
+                          , KindedTV sendNewStVar () (ConT protName)
+                          , KindedTV recvVar () (ConT roleName)
+                          , KindedTV receiverNewStVar () (ConT protName)
+                          ]
+                      )
+                      ( typeListT
+                          [ ConT ''TSC.Msg
+                          , ConT roleName
+                          , ConT protName
+                          , (SigT (VarT fromVar) (ConT protName))
+                          , (SigT (VarT sendVar) (ConT roleName))
+                          , (SigT (VarT sendNewStVar) (ConT protName))
+                          , (SigT (VarT recvVar) (ConT roleName))
+                          , (SigT (VarT receiverNewStVar) (ConT protName))
+                          ]
+                      )
+                      Nothing
+                      instMsgDesc
+                      []
+                   ]
             )
         ]
 
diff --git a/test/Book.hs b/test/Book.hs
deleted file mode 100644
--- a/test/Book.hs
+++ /dev/null
@@ -1,232 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QualifiedDo #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# OPTIONS_GHC -Wno-unused-do-bind #-}
-
-module Book where
-
-import Control.Concurrent.Class.MonadSTM
-import Control.Monad
-import Control.Monad.Class.MonadFork (MonadFork, forkIO)
-import Control.Monad.Class.MonadSay
-import Control.Monad.Class.MonadThrow (MonadThrow)
-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)
-import qualified Data.IFunctor as I
-import qualified Data.IntMap as IntMap
-import Data.Kind
-import GHC.Exts (dataToTag#)
-import GHC.Int (Int (I#))
-import TypedSession.Codec
-import TypedSession.Core
-import TypedSession.Driver
-import Control.Monad.Class.MonadTimer (MonadDelay)
-
-{-
-
---------------------------------------------------------------------------
-    Buyer                                                      Seller
-    :S0                                                        :S0
-     <                     Title String  ->                     >
-    :S1                                                        :S1
-     <                     <-  Price Int                         >
-    :S12 s                                                     :S12 s
-
-   ---------------------------------------------------------------------
-   |:S12 EnoughBudget                                          :S12 s
-   | <                  Afford ->                               >
-   |:S3                                                        :S3
-   | <                  <- Data Int                             >
-   |:End                                                       :End
-   ---------------------------------------------------------------------
-
-   ---------------------------------------------------------------------
-   |:S12 NotEnoughBuget                                        :S12 s
-   | <                  NotBuy ->                               >
-   |:End                                                       :End
-   ---------------------------------------------------------------------
- -}
-
-data Role = Buyer | Seller
-  deriving (Show, Eq, Ord)
-
-data SRole :: Role -> Type where
-  SBuyer :: SRole Buyer
-  SSeller :: SRole Seller
-
-type instance Sing = SRole
-
-instance SingI Buyer where
-  sing = SBuyer
-
-instance SingI Seller where
-  sing = SSeller
-
-data BudgetSt
-  = EnoughBudget
-  | NotEnoughBuget
-
-data BookSt
-  = S0
-  | S1
-  | S12 BudgetSt
-  | S3
-  | End
-
-data SBookSt :: BookSt -> Type where
-  SS0 :: SBookSt S0
-  SS1 :: SBookSt S1
-  SS12 :: SBookSt (S12 (s :: BudgetSt))
-  SS3 :: SBookSt S3
-  SEnd :: SBookSt End
-
-type instance Sing = SBookSt
-
-instance SingI S0 where
-  sing = SS0
-
-instance SingI S1 where
-  sing = SS1
-
-instance SingI (S12 s) where
-  sing = SS12
-
-instance SingI S3 where
-  sing = SS3
-
-instance SingI End where
-  sing = SEnd
-
-type Date = Int
-
-instance SingToInt Role where
-  singToInt x = I# (dataToTag# x)
-
-instance SingToInt BookSt where
-  singToInt x = I# (dataToTag# x)
-
-instance Protocol Role BookSt where
-  type Done Buyer = End
-  type Done Seller = End
-
-  data Msg Role BookSt from send recv where
-    Title :: String -> Msg Role BookSt S0 '(Buyer, S1) '(Seller, S1)
-    Price :: Int -> Msg Role BookSt S1 '(Seller, S12 s) '(Buyer, S12 s)
-    Afford :: Msg Role BookSt (S12 EnoughBudget) '(Buyer, S3) '(Seller, S3)
-    Date :: Date -> Msg Role BookSt S3 '(Seller, End) '(Buyer, End)
-    NotBuy :: Msg Role BookSt (S12 NotEnoughBuget) '(Buyer, End) '(Seller, End)
-
-encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)
-encodeMsg = Encode $ \x -> case x of
-  Title{} -> AnyMsg x
-  Price{} -> AnyMsg x
-  Afford{} -> AnyMsg x
-  Date{} -> AnyMsg x
-  NotBuy{} -> AnyMsg x
-
-decodeMsg
-  :: DecodeStep
-      (AnyMsg Role BookSt)
-      CodecFailure
-      (AnyMsg Role BookSt)
-decodeMsg =
-  DecodePartial $ \case
-    Nothing -> DecodeFail (CodecFailure "expected more data")
-    Just anyMsg -> DecodeDone anyMsg Nothing
-
-budget :: Int
-budget = 100
-
-data CheckPriceResult :: BookSt -> Type where
-  Yes :: CheckPriceResult (S12 EnoughBudget)
-  No :: CheckPriceResult (S12 NotEnoughBuget)
-
-checkPrice :: (Monad m) => Int -> Peer Role BookSt Buyer m CheckPriceResult (S12 s)
-checkPrice i =
-  if i <= budget
-    then LiftM $ pure (ireturn Yes)
-    else LiftM $ pure (ireturn No)
-
-buyerPeer
-  :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0
-buyerPeer = I.do
-  yield (Title "haskell book")
-  Recv (Price i) <- await
-  res <- checkPrice i
-  case res of
-    Yes -> I.do
-      yield Afford
-      Recv (Date d) <- await
-      returnAt (Just d)
-    No -> I.do
-      yield NotBuy
-      returnAt Nothing
-
-sellerPeer :: (Functor m) => Peer Role BookSt Seller m (At () (Done Seller)) S0
-sellerPeer = I.do
-  Recv (Title _name) <- await
-  yield (Price 30)
-  Recv msg <- await
-  case msg of
-    Afford -> I.do
-      yield (Date 100)
-    NotBuy -> I.do
-      returnAt ()
-
-mvarsAsChannel
-  :: (MonadSTM m)
-  => TMVar m a
-  -> TMVar m a
-  -> Channel m a
-mvarsAsChannel bufferRead bufferWrite =
-  Channel{send, recv}
- where
-  send x = atomically (putTMVar bufferWrite x)
-  recv = atomically (Just <$> takeTMVar bufferRead)
-
-myTracer :: (MonadSay m) => String -> Tracer Role BookSt m
-myTracer st v = say (st <> show v)
-
-instance Show (AnyMsg Role BookSt) where
-  show (AnyMsg msg) = case msg of
-    Title st -> "Title " <> show st
-    Price i -> "Price " <> show i
-    Afford -> "Afford"
-    Date i -> "Date " <> show i
-    NotBuy -> "NotBuy"
-
-runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()
-runAll = do
-  buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  let buyerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar
-      sellerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar
-      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)
-      sendToRole =
-        IntMap.fromList
-          [ (singToInt SSeller, sendFun sellerTMVar)
-          , (singToInt SBuyer, sendFun buyerTMVar)
-          ]
-  buyerTvar <- newTVarIO IntMap.empty
-  sellerTvar <- newTVarIO IntMap.empty
-  let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id
-      sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id
-  -- fork buyer decode thread, seller -> buyer
-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerChannel buyerTvar
-  -- fork seller decode thread, buyer -> seller
-  forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerChannel sellerTvar
-  -- fork seller Peer thread
-  forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer
-  -- run buyer Peer
-  void $ runPeerWithDriver buyerDriver buyerPeer
diff --git a/test/Book1.hs b/test/Book1.hs
deleted file mode 100644
--- a/test/Book1.hs
+++ /dev/null
@@ -1,281 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QualifiedDo #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# OPTIONS_GHC -Wno-unused-do-bind #-}
-
-module Book1 where
-
-import Control.Concurrent.Class.MonadSTM
-import Control.Monad
-import Control.Monad.Class.MonadFork (MonadFork, forkIO)
-import Control.Monad.Class.MonadSay
-import Control.Monad.Class.MonadThrow (MonadThrow)
-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)
-import qualified Data.IFunctor as I
-import qualified Data.IntMap as IntMap
-import Data.Kind
-import GHC.Exts (dataToTag#)
-import GHC.Int (Int (I#))
-import TypedSession.Codec
-import TypedSession.Core
-import TypedSession.Driver
-import Control.Monad.Class.MonadTimer (MonadDelay)
-
-{-
-
------------------------------------------------------------------------------------------------
-    Buyer                                                      Seller                  Buyer2
-    :S0                                                        :S0
-     <                     Title String  ->                     >
-    :S1                                                        :S1
-     <                     <-  Price Int                         >
-    :S11                                                       :S12 s                  :S11
-     <                                  PriceToBuyer2 Int ->                            >
-    :S110                                                                              :S110
-     <                                  <- HalfPrice  Int                               >
-    :S12 s                                                                             :End
-
-   ---------------------------------------------------------------------
-   |:S12 EnoughBudget                                          :S12 s
-   | <                  Afford ->                               >
-   |:S3                                                        :S3
-   | <                  <- Data Int                             >
-   |:End                                                       :End
-   ---------------------------------------------------------------------
-
-   ---------------------------------------------------------------------
-   |:S12  NotEnoughBuget                                       :S12
-   | <                  NotBuy ->                               >
-   |:End                                                       :End
-   ---------------------------------------------------------------------
--}
-
-data Role = Buyer | Seller | Buyer2
-  deriving (Show, Eq, Ord)
-
-data SRole :: Role -> Type where
-  SBuyer :: SRole Buyer
-  SBuyer2 :: SRole Buyer2
-  SSeller :: SRole Seller
-
-type instance Sing = SRole
-
-instance SingI Buyer where
-  sing = SBuyer
-
-instance SingI Buyer2 where
-  sing = SBuyer2
-
-instance SingI Seller where
-  sing = SSeller
-
-data BudgetSt
-  = EnoughBudget
-  | NotEnoughBuget
-
-data BookSt
-  = S0
-  | S1
-  | S11
-  | S110
-  | S12 BudgetSt
-  | S3
-  | End
-
-data SBookSt :: BookSt -> Type where
-  SS0 :: SBookSt S0
-  SS1 :: SBookSt S1
-  SS11 :: SBookSt S11
-  SS110 :: SBookSt S110
-  SS12 :: SBookSt (S12 (s :: BudgetSt))
-  SS3 :: SBookSt S3
-  SEnd :: SBookSt End
-
-type instance Sing = SBookSt
-
-instance SingI S0 where
-  sing = SS0
-
-instance SingI S1 where
-  sing = SS1
-
-instance SingI S11 where
-  sing = SS11
-
-instance SingI S110 where
-  sing = SS110
-
-instance SingI (S12 s) where
-  sing = SS12
-
-instance SingI S3 where
-  sing = SS3
-
-instance SingI End where
-  sing = SEnd
-
-type Date = Int
-
-instance SingToInt Role where
-  singToInt x = I# (dataToTag# x)
-
-instance SingToInt BookSt where
-  singToInt x = I# (dataToTag# x)
-
-instance Protocol Role BookSt where
-  type Done Buyer = End
-  type Done Seller = End
-  type Done Buyer2 = End
-  data Msg Role BookSt from send recv where
-    Title :: String -> Msg Role BookSt S0 '(Buyer, S1) '(Seller, S1)
-    Price :: Int -> Msg Role BookSt S1 '(Seller, S12 s) '(Buyer, S11)
-    PriceToB2 :: Int -> Msg Role BookSt S11 '(Buyer, S110) '(Buyer2, S110)
-    HalfPrice :: Int -> Msg Role BookSt S110 '(Buyer2, End) '(Buyer, S12 s)
-    Afford :: Msg Role BookSt (S12 EnoughBudget) '(Buyer, S3) '(Seller, S3)
-    Date :: Date -> Msg Role BookSt S3 '(Seller, End) '(Buyer, End)
-    NotBuy :: Msg Role BookSt (S12 NotEnoughBuget) '(Buyer, End) '(Seller, End)
-
-encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)
-encodeMsg = Encode $ \x -> case x of
-  Title{} -> AnyMsg x
-  Price{} -> AnyMsg x
-  PriceToB2{} -> AnyMsg x
-  HalfPrice{} -> AnyMsg x
-  Afford{} -> AnyMsg x
-  Date{} -> AnyMsg x
-  NotBuy{} -> AnyMsg x
-
-decodeMsg
-  :: DecodeStep
-      (AnyMsg Role BookSt)
-      CodecFailure
-      (AnyMsg Role BookSt)
-decodeMsg =
-  DecodePartial $ \case
-    Nothing -> DecodeFail (CodecFailure "expected more data")
-    Just anyMsg -> DecodeDone anyMsg Nothing
-
-budget :: Int
-budget = 16
-
-data CheckPriceResult :: BookSt -> Type where
-  Yes :: CheckPriceResult (S12 EnoughBudget)
-  No :: CheckPriceResult (S12 NotEnoughBuget)
-
-checkPrice :: (Monad m) => Int -> Int -> Peer Role BookSt Buyer m CheckPriceResult (S12 s)
-checkPrice i h =
-  if i <= budget + h
-    then LiftM $ pure (ireturn Yes)
-    else LiftM $ pure (ireturn No)
-
-buyerPeer
-  :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0
-buyerPeer = I.do
-  yield (Title "haskell book")
-  Recv (Price i) <- await
-  yield (PriceToB2 i)
-  Recv (HalfPrice hv) <- await
-  res <- checkPrice i hv
-  case res of
-    Yes -> I.do
-      yield Afford
-      Recv (Date d) <- await
-      returnAt (Just d)
-    No -> I.do
-      yield NotBuy
-      returnAt Nothing
-
-buyer2Peer
-  :: (Monad m) => Peer Role BookSt Buyer2 m (At () (Done Buyer2)) S11
-buyer2Peer = I.do
-  Recv (PriceToB2 i) <- await
-  yield (HalfPrice (i `div` 2))
-
-sellerPeer :: (Monad m) => Peer Role BookSt Seller m (At () (Done Seller)) S0
-sellerPeer = I.do
-  Recv (Title _name) <- await
-  yield (Price 30)
-  Recv msg <- await
-  case msg of
-    Afford -> yield (Date 100)
-    NotBuy -> returnAt ()
-
-mvarsAsChannel
-  :: (MonadSTM m)
-  => TMVar m a
-  -> TMVar m a
-  -> Channel m a
-mvarsAsChannel bufferRead bufferWrite =
-  Channel{send, recv}
- where
-  send x = atomically (putTMVar bufferWrite x)
-  recv = atomically (Just <$> takeTMVar bufferRead)
-
-myTracer :: (MonadSay m) => String -> Tracer Role BookSt m
-myTracer st v = say (st <> show v)
-
-instance Show (AnyMsg Role BookSt) where
-  show (AnyMsg msg) = case msg of
-    Title st -> "Title " <> show st
-    Price i -> "Price " <> show i
-    PriceToB2 i -> "PriceToB2 " <> show i
-    HalfPrice i -> "HalfPrice " <> show i
-    Afford -> "Afford"
-    Date i -> "Date " <> show i
-    NotBuy -> "NotBuy"
-
-runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()
-runAll = do
-  buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  buyer2TMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  let buyerSellerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar
-      buyerBuyer2Channel = mvarsAsChannel @m buyerTMVar buyer2TMVar
-
-      sellerBuyerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar
-
-      buyer2BuyerChannel = mvarsAsChannel @m buyer2TMVar buyerTMVar
-
-      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)
-      sendToRole =
-        IntMap.fromList
-          [ (singToInt SSeller, sendFun sellerTMVar)
-          , (singToInt SBuyer, sendFun buyerTMVar)
-          , (singToInt SBuyer2, sendFun buyer2TMVar)
-          ]
-  buyerTvar <- newTVarIO IntMap.empty
-  buyer2Tvar <- newTVarIO IntMap.empty
-  sellerTvar <- newTVarIO IntMap.empty
-  let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id
-      buyer2Driver = driverSimple (myTracer "buyer2") encodeMsg sendToRole buyer2Tvar id
-      sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id
-  -- fork buyer decode thread, seller -> buyer
-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerSellerChannel buyerTvar
-  -- fork buyer decode thread, buyer2 -> buyer
-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerBuyer2Channel buyerTvar
-
-  -- fork seller decode thread, buyer -> seller
-  forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar
-
-  -- fork buyer2 decode thread, buyer -> buyer2
-  forkIO $ decodeLoop (myTracer "buyer2") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar
-
-  -- fork seller Peer thread
-  forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer
-
-  -- fork buyer2 Peer thread
-  forkIO $ void $ runPeerWithDriver buyer2Driver buyer2Peer
-  -- run buyer Peer
-  void $ runPeerWithDriver buyerDriver buyerPeer
diff --git a/test/Book2.hs b/test/Book2.hs
deleted file mode 100644
--- a/test/Book2.hs
+++ /dev/null
@@ -1,342 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QualifiedDo #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# OPTIONS_GHC -Wno-unused-do-bind #-}
-
-module Book2 where
-
-import Control.Concurrent.Class.MonadSTM
-import Control.Monad
-import Control.Monad.Class.MonadFork (MonadFork, forkIO)
-import Control.Monad.Class.MonadSay
-import Control.Monad.Class.MonadThrow (MonadThrow)
-import Control.Monad.Class.MonadTimer (MonadDelay)
-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)
-import qualified Data.IFunctor as I
-import qualified Data.IntMap as IntMap
-import Data.Kind
-import GHC.Exts (dataToTag#)
-import GHC.Int (Int (I#))
-import TypedSession.Codec
-import TypedSession.Core
-import TypedSession.Driver
-
-{-
-
------------------Buyer---------------Seller--------------Buyer2-----------------
-                   S0                  S0                 S1 s
-       Title       |        --->       |
-                  S2 s                S2 s                S1 s
-    ------------------------------BookNotFound------------------------------
-                  S2 s          S2 BookNotFound           S1 s
-    BookNotFoun    |        <---       |
-            S1 BookNotFound           End                 S1 s
-  SellerNotFoundB  |                  --->                 |
-                  End                 End                 End
-                                    Terminal
-
-    -------------------------------BookFound--------------------------------
-                  S2 s            S2 BookFound            S1 s
-       Price       |        <---       |
-              S1 BookFound            S3 s                S1 s
-   PriceToBuyer2   |                  --->                 |
-                   S4                 S3 s                 S4
-     HalfPrice     |                  <---                 |
-                  S3 s                S3 s                S5 s
-        --------------------------EnoughBudget--------------------------
-            S3 EnoughBudget           S3 s                S5 s
-       Afford      |        --->       |
-                   S6                  S6                 S5 s
-        Data       |        <---       |
-            S5 EnoughBudget           End                 S5 s
-      Success      |                  --->                 |
-                  End                 End                 End
-                                    Terminal
-
-        ------------------------NotEnoughBudget-------------------------
-           S3 NotEnoughBudget         S3 s                S5 s
-       NotBuy      |        --->       |
-           S5 NotEnoughBudget         End                 S5 s
-       Failed      |                  --->                 |
-                  End                 End                 End
-                                    Terminal
--}
-
-data Role = Buyer | Seller | Buyer2
-  deriving (Show, Eq, Ord)
-
-data SRole :: Role -> Type where
-  SBuyer :: SRole Buyer
-  SBuyer2 :: SRole Buyer2
-  SSeller :: SRole Seller
-
-type instance Sing = SRole
-
-instance SingI Buyer where
-  sing = SBuyer
-
-instance SingI Buyer2 where
-  sing = SBuyer2
-
-instance SingI Seller where
-  sing = SSeller
-
-data FindBook
-  = BookNotFound
-  | BookFound
-
-data BudgetSt
-  = EnoughBudget
-  | NotEnoughBuget
-
-data BookSt
-  = S0
-  | S1 FindBook
-  | S2 FindBook
-  | S3 BudgetSt
-  | S4
-  | S5 BudgetSt
-  | S6
-  | End
-
-data SBookSt :: BookSt -> Type where
-  SS0 :: SBookSt S0
-  SS1 :: SBookSt (S1 (s :: FindBook))
-  SS2 :: SBookSt (S2 (s :: FindBook))
-  SS3 :: SBookSt (S3 (s :: BudgetSt))
-  SS4 :: SBookSt S4
-  SS5 :: SBookSt (S5 (s :: BudgetSt))
-  SS6 :: SBookSt S6
-  SEnd :: SBookSt End
-
-type instance Sing = SBookSt
-
-instance SingI S0 where
-  sing = SS0
-
-instance SingI (S1 s) where
-  sing = SS1
-
-instance SingI (S2 s) where
-  sing = SS2
-
-instance SingI (S3 s) where
-  sing = SS3
-
-instance SingI S4 where
-  sing = SS4
-
-instance SingI (S5 s) where
-  sing = SS5
-
-instance SingI S6 where
-  sing = SS6
-
-instance SingI End where
-  sing = SEnd
-
-type Date = Int
-
-instance SingToInt Role where
-  singToInt x = I# (dataToTag# x)
-
-instance SingToInt BookSt where
-  singToInt x = I# (dataToTag# x)
-
-instance Protocol Role BookSt where
-  type Done Buyer = End
-  type Done Seller = End
-  type Done Buyer2 = End
-  data Msg Role BookSt from send recv where
-    Title :: String -> Msg Role BookSt S0 '(Buyer, S2 s) '(Seller, S2 s)
-    Price :: Int -> Msg Role BookSt (S2 BookFound) '(Seller, S3 s) '(Buyer, S1 BookFound)
-    PriceToB2 :: Int -> Msg Role BookSt (S1 BookFound) '(Buyer, S4) '(Buyer2, S4)
-    HalfPrice :: Int -> Msg Role BookSt S4 '(Buyer2, S5 s) '(Buyer, S3 s)
-    Afford :: Msg Role BookSt (S3 EnoughBudget) '(Buyer, S6) '(Seller, S6)
-    Date :: Date -> Msg Role BookSt S6 '(Seller, End) '(Buyer, S5 EnoughBudget)
-    Success :: Int -> Msg Role BookSt (S5 EnoughBudget) '(Buyer, End) '(Buyer2, End)
-    NotBuy :: Msg Role BookSt (S3 NotEnoughBuget) '(Buyer, S5 NotEnoughBuget) '(Seller, End)
-    Failed :: Msg Role BookSt (S5 NotEnoughBuget) '(Buyer, End) '(Buyer2, End)
-    BookNotFoun :: Msg Role BookSt (S2 BookNotFound) '(Seller, End) '(Buyer, S1 BookNotFound)
-    SellerNotFoundBook :: Msg Role BookSt (S1 BookNotFound) '(Buyer, End) '(Buyer2, End)
-
-encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)
-encodeMsg = Encode $ \x -> case x of
-  Title{} -> AnyMsg x
-  Price{} -> AnyMsg x
-  PriceToB2{} -> AnyMsg x
-  HalfPrice{} -> AnyMsg x
-  Afford{} -> AnyMsg x
-  Date{} -> AnyMsg x
-  Success{} -> AnyMsg x
-  NotBuy{} -> AnyMsg x
-  Failed{} -> AnyMsg x
-  BookNotFoun{} -> AnyMsg x
-  SellerNotFoundBook{} -> AnyMsg x
-
-decodeMsg
-  :: DecodeStep
-      (AnyMsg Role BookSt)
-      CodecFailure
-      (AnyMsg Role BookSt)
-decodeMsg =
-  DecodePartial $ \case
-    Nothing -> DecodeFail (CodecFailure "expected more data")
-    Just anyMsg -> DecodeDone anyMsg Nothing
-
-budget :: Int
-budget = 16
-
-data CheckPriceResult :: BookSt -> Type where
-  Yes :: CheckPriceResult (S3 EnoughBudget)
-  No :: CheckPriceResult (S3 NotEnoughBuget)
-
-checkPrice :: (Monad m) => Int -> Int -> Peer Role BookSt Buyer m CheckPriceResult (S3 s)
-checkPrice i h =
-  if i <= budget + h
-    then LiftM $ pure (ireturn Yes)
-    else LiftM $ pure (ireturn No)
-
-buyerPeer
-  :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0
-buyerPeer = I.do
-  yield (Title "haskell book")
-  Recv msg <- await
-  case msg of
-    BookNotFoun -> I.do
-      yield SellerNotFoundBook
-      returnAt Nothing
-    Price i -> I.do
-      yield (PriceToB2 i)
-      Recv (HalfPrice hv) <- await
-      res <- checkPrice i hv
-      case res of
-        Yes -> I.do
-          yield Afford
-          Recv (Date d) <- await
-          yield (Success d)
-          returnAt (Just d)
-        No -> I.do
-          yield NotBuy
-          yield Failed
-          returnAt Nothing
-
-buyer2Peer
-  :: (Monad m) => Peer Role BookSt Buyer2 m (At () (Done Buyer2)) (S1 s)
-buyer2Peer = I.do
-  Recv msg' <- await
-  case msg' of
-    SellerNotFoundBook -> returnAt ()
-    PriceToB2 i -> I.do
-      yield (HalfPrice (i `div` 2))
-      Recv msg <- await
-      case msg of
-        Success _ -> returnAt ()
-        Failed -> returnAt ()
-
-data FindBookResult :: BookSt -> Type where
-  Found :: FindBookResult (S2 BookFound)
-  NotFound :: FindBookResult (S2 BookNotFound)
-
-findBook :: (Monad m) => String -> Peer Role BookSt Seller m FindBookResult (S2 s)
-findBook st =
-  if st /= ""
-    then LiftM $ pure (ireturn Found)
-    else LiftM $ pure (ireturn NotFound)
-
-sellerPeer :: (Monad m) => Peer Role BookSt Seller m (At () (Done Seller)) S0
-sellerPeer = I.do
-  Recv (Title name) <- await
-  res <- findBook name
-  case res of
-    Found -> I.do
-      yield (Price 30)
-      Recv msg <- await
-      case msg of
-        Afford -> yield (Date 100)
-        NotBuy -> returnAt ()
-    NotFound -> yield BookNotFoun
-
-mvarsAsChannel
-  :: (MonadSTM m)
-  => TMVar m a
-  -> TMVar m a
-  -> Channel m a
-mvarsAsChannel bufferRead bufferWrite =
-  Channel{send, recv}
- where
-  send x = atomically (putTMVar bufferWrite x)
-  recv = atomically (Just <$> takeTMVar bufferRead)
-
-myTracer :: (MonadSay m) => String -> Tracer Role BookSt m
-myTracer st v = say (st <> show v)
-
-instance Show (AnyMsg Role BookSt) where
-  show (AnyMsg msg) = case msg of
-    Title st -> "Title " <> show st
-    Price i -> "Price " <> show i
-    PriceToB2 i -> "PriceToB2 " <> show i
-    HalfPrice i -> "HalfPrice " <> show i
-    Afford -> "Afford"
-    Date i -> "Date " <> show i
-    NotBuy -> "NotBuy"
-    Success i -> "Success " <> show i
-    Failed -> "Failed"
-    BookNotFoun -> "BookNotFound"
-    SellerNotFoundBook -> "SellerNotFoundBook"
-
-runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()
-runAll = do
-  buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  buyer2TMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)
-  let buyerSellerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar
-      buyerBuyer2Channel = mvarsAsChannel @m buyerTMVar buyer2TMVar
-
-      sellerBuyerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar
-
-      buyer2BuyerChannel = mvarsAsChannel @m buyer2TMVar buyerTMVar
-
-      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)
-      sendToRole =
-        IntMap.fromList
-          [ (singToInt SSeller, sendFun sellerTMVar)
-          , (singToInt SBuyer, sendFun buyerTMVar)
-          , (singToInt SBuyer2, sendFun buyer2TMVar)
-          ]
-  buyerTvar <- newTVarIO IntMap.empty
-  buyer2Tvar <- newTVarIO IntMap.empty
-  sellerTvar <- newTVarIO IntMap.empty
-  let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id
-      buyer2Driver = driverSimple (myTracer "buyer2") encodeMsg sendToRole buyer2Tvar id
-      sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id
-  -- fork buyer decode thread, seller -> buyer
-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerSellerChannel buyerTvar
-  -- fork buyer decode thread, buyer2 -> buyer
-  forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerBuyer2Channel buyerTvar
-
-  -- fork seller decode thread, buyer -> seller
-  forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar
-
-  -- fork buyer2 decode thread, buyer -> buyer2
-  forkIO $ decodeLoop (myTracer "buyer2") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar
-
-  -- fork seller Peer thread
-  forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer
-
-  -- fork buyer2 Peer thread
-  forkIO $ void $ runPeerWithDriver buyer2Driver buyer2Peer
-  -- run buyer Peer
-  void $ runPeerWithDriver buyerDriver buyerPeer
diff --git a/test/Book3/Peer.hs b/test/Book3/Peer.hs
--- a/test/Book3/Peer.hs
+++ b/test/Book3/Peer.hs
@@ -55,38 +55,33 @@
 buyerPeer = I.do
   yield (Title "haskell book")
   await I.>>= \case
-    Recv NoBook -> I.do
+    NoBook -> I.do
       yield SellerNoBook
       returnAt Nothing
-    Recv (Price i) -> I.do
+    Price i -> I.do
       choiceOT i I.>>= \case
         BranchSt_One -> I.do
           yield OneAccept
-          Recv (OneDate d) <- await
+          OneDate d <- await
           yield (OneSuccess d)
           returnAt $ Just d
-        BranchSt_Two -> f1
- where
-  f1
-    :: (Has Random sig m)
-    => Peer BookRole Book 'Buyer m (At (Maybe Date) (Done Buyer)) ('S1 'Two)
-  f1 = I.do
-    yield (PriceToBuyer2 300)
-    await I.>>= \case
-      Recv NotSupport1 -> I.do
-        yield TwoNotBuy
-        returnAt Nothing
-      Recv (SupportVal h) -> I.do
-        checkPrice 10 h I.>>= \case
-          BranchSt_Enough -> I.do
-            yield TwoAccept
-            Recv (TwoDate d) <- await
-            yield (TwoSuccess d)
-            returnAt (Just d)
-          BranchSt_NotEnough -> I.do
-            yield TwoNotBuy1
-            yield TwoFailed
-            returnAt Nothing
+        BranchSt_Two -> I.do
+          yield (PriceToBuyer2 (i `div` 2))
+          await I.>>= \case
+            NotSupport1 -> I.do
+              yield TwoNotBuy
+              returnAt Nothing
+            SupportVal h -> I.do
+              checkPrice 10 h I.>>= \case
+                BranchSt_Enough -> I.do
+                  yield TwoAccept
+                  TwoDate d <- await
+                  yield (TwoSuccess d)
+                  returnAt (Just d)
+                BranchSt_NotEnough -> I.do
+                  yield TwoNotBuy1
+                  yield TwoFailed
+                  returnAt Nothing
 
 choiceB
   :: (Has Random sig m)
@@ -103,9 +98,9 @@
   => Peer BookRole Book Buyer2 m (At (Maybe Date) (Done Buyer2)) (S1 s)
 buyer2Peer = I.do
   await I.>>= \case
-    Recv SellerNoBook -> returnAt Nothing
-    Recv (OneSuccess d) -> returnAt (Just d)
-    Recv (PriceToBuyer2 i) -> I.do
+    SellerNoBook -> returnAt Nothing
+    (OneSuccess d) -> returnAt (Just d)
+    (PriceToBuyer2 i) -> I.do
       choiceB i I.>>= \case
         BranchSt_NotSupport -> I.do
           yield NotSupport1
@@ -113,8 +108,8 @@
         BranchSt_Support -> I.do
           yield (SupportVal (i `div` 2))
           await I.>>= \case
-            Recv (TwoSuccess d) -> returnAt $ Just d
-            Recv TwoFailed -> returnAt Nothing
+            TwoSuccess d -> returnAt $ Just d
+            TwoFailed -> returnAt Nothing
 
 findBook
   :: (Has Random sig m)
@@ -130,13 +125,13 @@
   :: (Has Random sig m)
   => Peer BookRole Book Seller m (At () (Done Seller)) S0
 sellerPeer = I.do
-  Recv (Title st) <- await
+  (Title st) <- await
   findBook st I.>>= \case
     BranchSt_NotFound -> yield NoBook
     BranchSt_Found -> I.do
       yield (Price 30)
       await I.>>= \case
-        Recv OneAccept -> yield (OneDate 100)
-        Recv TwoNotBuy -> returnAt ()
-        Recv TwoAccept -> yield (TwoDate 100)
-        Recv TwoNotBuy1 -> returnAt ()
+        OneAccept -> yield (OneDate 100)
+        TwoNotBuy -> returnAt ()
+        TwoAccept -> yield (TwoDate 100)
+        TwoNotBuy1 -> returnAt ()
diff --git a/test/Book3/Protocol.hs b/test/Book3/Protocol.hs
--- a/test/Book3/Protocol.hs
+++ b/test/Book3/Protocol.hs
@@ -17,7 +17,6 @@
 
 import Book3.Type
 
-import Language.Haskell.TH hiding (Type)
 import TypedSession.Codec
 import TypedSession.Core
 
diff --git a/test/PingPong.hs b/test/PingPong.hs
deleted file mode 100644
--- a/test/PingPong.hs
+++ /dev/null
@@ -1,196 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QualifiedDo #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# OPTIONS_GHC -Wno-unused-do-bind #-}
-
-module PingPong where
-
-import Control.Concurrent.Class.MonadSTM
-import Control.Monad
-import Control.Monad.Class.MonadFork (MonadFork, forkIO)
-import Control.Monad.Class.MonadSay
-import Control.Monad.Class.MonadThrow (MonadThrow)
-import Control.Monad.Class.MonadTimer (MonadDelay)
-import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)
-import qualified Data.IFunctor as I
-import qualified Data.IntMap as IntMap
-import Data.Kind
-import GHC.Exts (dataToTag#)
-import GHC.Int (Int (I#))
-import TypedSession.Codec
-import TypedSession.Core
-import TypedSession.Driver
-
-{-
-
---------------------------------------------------------------------------
-   Client                               Server
-    :S0 s                                 :S0 s
-  -----------------------------------------------------------------------
-  | :S0 True                           :S0 s
-  |             Ping    ->
-  | :S1                                :S1
-  |             <- Pong
-  | :S0 s                               :S0 s
-  -----------------------------------------------------------------------
-
-  -----------------------------------------------------------------------
-  |  :S0 False                          :S0 s
-  |               Stop    ->
-  |  :End                               :End
-  -----------------------------------------------------------------------
- -}
-
-data Role = Client | Server
-  deriving (Show, Eq, Ord)
-
-data SRole :: Role -> Type where
-  SClient :: SRole Client
-  SServer :: SRole Server
-
-type instance Sing = SRole
-
-instance SingI Client where
-  sing = SClient
-
-instance SingI Server where
-  sing = SServer
-
-data PingPong
-  = S0 Bool
-  | S1
-  | End
-
-data SPingPong :: PingPong -> Type where
-  SS0 :: SPingPong (S0 b)
-  SS1 :: SPingPong S1
-  SEnd :: SPingPong End
-
-type instance Sing = SPingPong
-
-instance SingI (S0 b) where
-  sing = SS0
-
-instance SingI S1 where
-  sing = SS1
-
-instance SingI End where
-  sing = SEnd
-
-instance SingToInt Role where
-  singToInt x = I# (dataToTag# x)
-
-instance SingToInt PingPong where
-  singToInt x = I# (dataToTag# x)
-
-instance Protocol Role PingPong where
-  type Done Client = End
-  type Done Server = End
-  data Msg Role PingPong from send recv where
-    Ping :: Int -> Msg Role PingPong (S0 True) '(Client, S1) '(Server, S1)
-    Pong :: Int -> Msg Role PingPong S1 '(Server, S0 s) '(Client, S0 s)
-    Stop :: Msg Role PingPong (S0 False) '(Client, End) '(Server, End)
-
-encodeMsg :: Encode Role PingPong (AnyMsg Role PingPong)
-encodeMsg = Encode $ \x -> case x of
-  Ping{} -> AnyMsg x
-  Pong{} -> AnyMsg x
-  Stop{} -> AnyMsg x
-
-decodeMsg
-  :: DecodeStep
-      (AnyMsg Role PingPong)
-      CodecFailure
-      (AnyMsg Role PingPong)
-decodeMsg =
-  DecodePartial $ \case
-    Nothing -> DecodeFail (CodecFailure "expected more data")
-    Just anyMsg -> DecodeDone anyMsg Nothing
-
-data Choice :: PingPong -> Type where
-  ST :: Choice (S0 True)
-  SF :: Choice (S0 False)
-
-choice :: (Monad m) => Int -> Peer Role PingPong Client m Choice (S0 s)
-choice i =
-  if i <= 5
-    then LiftM $ pure (ireturn ST)
-    else LiftM $ pure (ireturn SF)
-
-clientPeer
-  :: (Monad m) => Int -> Peer Role PingPong Client m (At () (Done Client)) (S0 s)
-clientPeer i = I.do
-  res <- choice i
-  case res of
-    ST -> I.do
-      yield (Ping i)
-      Recv (Pong i') <- await
-      clientPeer i'
-    SF -> yield Stop
-
-serverPeer
-  :: (Monad m) => Peer Role PingPong Server m (At () (Done Server)) (S0 s)
-serverPeer = I.do
-  Recv msg <- await
-  case msg of
-    Ping i -> I.do
-      yield (Pong (i + 1))
-      serverPeer
-    Stop -> returnAt ()
-
-mvarsAsChannel
-  :: (MonadSTM m)
-  => TMVar m a
-  -> TMVar m a
-  -> Channel m a
-mvarsAsChannel bufferRead bufferWrite =
-  Channel{send, recv}
- where
-  send x = atomically (putTMVar bufferWrite x)
-  recv = atomically (Just <$> takeTMVar bufferRead)
-
-myTracer :: (MonadSay m) => String -> Tracer Role PingPong m
-myTracer st v = say (st <> show v)
-
-instance Show (AnyMsg Role PingPong) where
-  show (AnyMsg msg) = case msg of
-    Ping i -> "Ping " <> show i
-    Pong i -> "Pong " <> show i
-    Stop -> "Stop"
-
-runAll :: forall m. (Monad m, MonadDelay m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()
-runAll = do
-  clientTMVar <- newEmptyTMVarIO @m @(AnyMsg Role PingPong)
-  serverTMVar <- newEmptyTMVarIO @m @(AnyMsg Role PingPong)
-  let clientChannel = mvarsAsChannel @m clientTMVar serverTMVar
-      serverChannel = mvarsAsChannel @m serverTMVar clientTMVar
-      sendFun bufferWrite x = atomically (putTMVar bufferWrite x)
-      sendToRole =
-        IntMap.fromList
-          [ (singToInt SServer, sendFun serverTMVar)
-          , (singToInt SClient, sendFun clientTMVar)
-          ]
-  clientTvar <- newTVarIO IntMap.empty
-  serverTvar <- newTVarIO IntMap.empty
-  let clientDriver = driverSimple (myTracer "client: ") encodeMsg sendToRole clientTvar id
-      serverDriver = driverSimple (myTracer "server: ") encodeMsg sendToRole serverTvar id
-  -- fork client decode thread
-  forkIO $ decodeLoop (myTracer "client: ") Nothing (Decode decodeMsg) clientChannel clientTvar
-  -- fork server decode thread
-  forkIO $ decodeLoop (myTracer "server: ") Nothing (Decode decodeMsg) serverChannel serverTvar
-  -- fork server Peer thread
-  forkIO $ void $ runPeerWithDriver serverDriver serverPeer
-  -- run client Peer
-  void $ runPeerWithDriver clientDriver (clientPeer 0)
diff --git a/typed-session.cabal b/typed-session.cabal
--- a/typed-session.cabal
+++ b/typed-session.cabal
@@ -20,7 +20,7 @@
 -- PVP summary:     +-+------- breaking API changes
 --                  | | +----- non-breaking API additions
 --                  | | | +--- code changes with no API change
-version:            0.1.3.0
+version:            0.2.0.0
 
 -- A short (one-line) description of the package.
 synopsis: typed session framework
@@ -95,14 +95,10 @@
     default-language: Haskell2010
 
     -- Modules included in this executable, other than Main.
-    other-modules: Book
-                 , Book1
-                 , Book2
-                 , Book3.Type
+    other-modules: Book3.Type
                  , Book3.Protocol
                  , Book3.Peer
                  , Book3.Main
-                 , PingPong
 
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions: