typed-protocols: renamed Pipelined kind to IsPipelined

This allows us to not worry about the promoted type and kind to have the
same name.

Author: coot

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Client.hs

@@ -141,20 +141,20 @@ data PingPongClientIdle (n :: Outstanding) c m a where
 pingPongClientPeerPipelined
   :: Functor m
   => PingPongClientPipelined c m a
-  -> Client PingPong ('Pipelined c) Z StIdle m a
+  -> Client PingPong (Pipelined c) Z StIdle m a
 pingPongClientPeerPipelined (PingPongClientPipelined peer) =
     pingPongClientPeerIdle peer
 
 
 pingPongClientPeerIdle
   :: forall (n :: Outstanding) c m a. Functor m
   => PingPongClientIdle             n        c m a
-  -> Client PingPong ('Pipelined c) n StIdle   m a
+  -> Client PingPong (Pipelined c) n StIdle   m a
 pingPongClientPeerIdle = go
   where
     go :: forall (n' :: Outstanding).
           PingPongClientIdle             n'        c m a
-       -> Client PingPong ('Pipelined c) n' StIdle   m a
+       -> Client PingPong (Pipelined c) n' StIdle   m a
 
     go (SendMsgPingPipelined receive next) =
       -- Pipelined yield: send `MsgPing`, immediately follow with the next step.

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Client.hs

@@ -118,7 +118,7 @@ data ReqRespIdle req resp c n m a where
 reqRespClientPeerPipelined
   :: Functor m
   => ReqRespClientPipelined req resp       c           m a
-  -> Client (ReqResp req resp) ('Pipelined c) Z StIdle m a
+  -> Client (ReqResp req resp) (Pipelined c) Z StIdle m a
 reqRespClientPeerPipelined (ReqRespClientPipelined peer) =
     reqRespClientPeerIdle peer
 
@@ -127,13 +127,13 @@ reqRespClientPeerIdle
   :: forall req resp n c m a.
      Functor m
   => ReqRespIdle   req resp                c  n         m a
-  -> Client (ReqResp req resp) ('Pipelined c) n StIdle  m a
+  -> Client (ReqResp req resp) (Pipelined c) n StIdle  m a
 
 reqRespClientPeerIdle = go
   where
     go :: forall n'.
           ReqRespIdle   req resp                c  n'        m a
-       -> Client (ReqResp req resp) ('Pipelined c) n' StIdle m a
+       -> Client (ReqResp req resp) (Pipelined c) n' StIdle m a
 
     go (SendMsgReqPipelined req receive next) =
       -- Pipelined yield: send `MsgReq`, immediately follow with the next step.

typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Client.hs

@@ -21,14 +21,14 @@ import           Network.TypedProtocol.Peer.Client
 reqResp2Client :: forall req resp m.
                   ()
                => [Either req req]
-               -> Client (ReqResp2 req resp) ('Pipelined (Either resp resp)) Z StIdle m [Either resp resp]
+               -> Client (ReqResp2 req resp) (Pipelined (Either resp resp)) Z StIdle m [Either resp resp]
 reqResp2Client = send Zero
   where
     -- pipeline all the requests, either through `MsgReq` or `MsgReq'`.
     send :: forall (n :: N).
             Nat n
          -> [Either req req] -- requests to send
-         -> Client (ReqResp2 req resp) ('Pipelined (Either resp resp))  n StIdle m [Either resp resp]
+         -> Client (ReqResp2 req resp) (Pipelined (Either resp resp))  n StIdle m [Either resp resp]
 
     send !n (Left req : reqs) =
       YieldPipelined (MsgReq  req) receiver (send (Succ n) reqs)
@@ -50,7 +50,7 @@ reqResp2Client = send Zero
     -- collect all the responses
     collect :: Nat n
             -> [Either resp resp] -- all the responses received so far
-            -> Client (ReqResp2 req resp) ('Pipelined (Either resp resp)) n StIdle m [Either resp resp]
+            -> Client (ReqResp2 req resp) (Pipelined (Either resp resp)) n StIdle m [Either resp resp]
 
     collect Zero !resps = Yield MsgDone (Done (reverse resps))
 

typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs

@@ -125,7 +125,7 @@ pingPong2Client =
   $ Client.Done ()
 
 
-pingPong2Client' :: forall m. Client.Client PingPong2 ('Pipelined ()) Client.Z StIdle m ()
+pingPong2Client' :: forall m. Client.Client PingPong2 (Pipelined ()) Client.Z StIdle m ()
 pingPong2Client' =
     --
     -- Pipeline first protocol

typed-protocols/src/Network/TypedProtocol/Core.hs

@@ -41,7 +41,7 @@ module Network.TypedProtocol.Core
   , TheyHaveAgencyProof
   , NobodyHasAgencyProof
   , FlipAgency
-  , Pipelined (..)
+  , IsPipelined (..)
   , ActiveAgency
   , ActiveAgency' (..)
   , IsActiveState (..)
@@ -476,10 +476,10 @@ type family FlipAgency pr where
 -- | Promoted data type which indicates if 'Peer' is used in
 -- pipelined mode or not.
 --
-data Pipelined where
+data IsPipelined where
     -- | Pipelined peer which is using `c :: Type` for collecting responses
     -- from a pipelined messages.
-    Pipelined    :: Type -> Pipelined
+    Pipelined    :: Type -> IsPipelined
 
     -- | Non-pipelined peer.
-    NonPipelined :: Pipelined
+    NonPipelined :: IsPipelined

typed-protocols/src/Network/TypedProtocol/Peer.hs

@@ -95,7 +95,7 @@ import           Network.TypedProtocol.Core as Core
 --
 type Peer :: forall ps
           -> PeerRole
-          -> Pipelined
+          -> IsPipelined
           -> Outstanding
           -> ps
           -> (Type -> Type)
@@ -209,9 +209,9 @@ data Peer ps pr pl n st m a where
     -> Message ps st st'
     -- ^ protocol message
     -> Receiver ps pr st' st'' m c
-    -> Peer ps pr ('Pipelined c) (S n) st'' m a
+    -> Peer ps pr (Pipelined c) (S n) st'' m a
     -- ^ continuation
-    -> Peer ps pr ('Pipelined c)  n    st   m a
+    -> Peer ps pr (Pipelined c)  n    st   m a
 
   -- | Partially collect promised transition.
   --
@@ -220,11 +220,11 @@ data Peer ps pr pl n st m a where
        ( SingI st
        , ActiveState st
        )
-    => Maybe (Peer ps pr ('Pipelined c) (S n) st m a)
+    => Maybe (Peer ps pr (Pipelined c) (S n) st m a)
     -- ^ continuation, executed if no message has arrived so far
-    -> (c ->  Peer ps pr ('Pipelined c)    n  st m a)
+    -> (c ->  Peer ps pr (Pipelined c)    n  st m a)
     -- ^ continuation
-    -> Peer        ps pr ('Pipelined c) (S n) st m a
+    -> Peer        ps pr (Pipelined c) (S n) st m a
 
 deriving instance Functor m => Functor (Peer ps pr pl n st m)
 

typed-protocols/src/Network/TypedProtocol/Peer/Client.hs

@@ -24,7 +24,7 @@ module Network.TypedProtocol.Peer.Client
   , pattern ReceiverAwait
   , pattern ReceiverDone
     -- * re-exports
-  , Pipelined (..)
+  , IsPipelined (..)
   , Outstanding
   , N (..)
   , Nat (..)
@@ -40,7 +40,7 @@ import qualified Network.TypedProtocol.Peer as TP
 
 
 type Client :: forall ps
-            -> Pipelined
+            -> IsPipelined
             -> Outstanding
             -> ps
             -> (Type -> Type)
@@ -114,9 +114,9 @@ pattern YieldPipelined :: forall ps st n c m a.
                        => Message ps st st'
                        -- ^ pipelined message
                        -> Receiver ps st' st'' m c
-                       -> Client ps ('Pipelined c) (S n) st'' m a
+                       -> Client ps (Pipelined c) (S n) st'' m a
                        -- ^ continuation
-                       -> Client ps ('Pipelined c)    n  st   m a
+                       -> Client ps (Pipelined c)    n  st   m a
 pattern YieldPipelined msg receiver k = TP.YieldPipelined ReflClientAgency msg receiver k
 
 
@@ -127,11 +127,11 @@ pattern Collect :: forall ps st n c m a.
                 => ( SingI st
                    , ActiveState st
                    )
-                => Maybe (Client ps ('Pipelined c) (S n) st m a)
+                => Maybe (Client ps (Pipelined c) (S n) st m a)
                 -- ^ continuation, executed if no message has arrived so far
-                -> (c ->  Client ps ('Pipelined c)    n  st m a)
+                -> (c ->  Client ps (Pipelined c)    n  st m a)
                 -- ^ continuation
-                -> Client        ps ('Pipelined c) (S n) st m a
+                -> Client        ps (Pipelined c) (S n) st m a
 pattern Collect k' k = TP.Collect k' k
 
 {-# COMPLETE Effect, Yield, Await, Done, YieldPipelined, Collect #-}

typed-protocols/src/Network/TypedProtocol/Peer/Server.hs

@@ -24,7 +24,7 @@ module Network.TypedProtocol.Peer.Server
   , pattern ReceiverAwait
   , pattern ReceiverDone
     -- * re-exports
-  , Pipelined (..)
+  , IsPipelined (..)
   , Outstanding
   , N (..)
   , Nat (..)
@@ -40,7 +40,7 @@ import qualified Network.TypedProtocol.Peer as TP
 
 
 type Server :: forall ps
-            -> Pipelined
+            -> IsPipelined
             -> Outstanding
             -> ps
             -> (Type -> Type)
@@ -114,9 +114,9 @@ pattern YieldPipelined :: forall ps st n c m a.
                        => Message ps st st'
                        -- ^ pipelined message
                        -> Receiver ps st' st'' m c
-                       -> Server ps ('Pipelined c) (S n) st'' m a
+                       -> Server ps (Pipelined c) (S n) st'' m a
                        -- ^ continuation
-                       -> Server ps ('Pipelined c)    n  st   m a
+                       -> Server ps (Pipelined c)    n  st   m a
 pattern YieldPipelined msg receiver k = TP.YieldPipelined ReflServerAgency msg receiver k
 
 
@@ -127,11 +127,11 @@ pattern Collect :: forall ps st n c m a.
                 => ( SingI st
                    , ActiveState st
                    )
-                => Maybe (Server ps ('Pipelined c) (S n) st m a)
+                => Maybe (Server ps (Pipelined c) (S n) st m a)
                 -- ^ continuation, executed if no message has arrived so far
-                -> (c -> Server  ps ('Pipelined c)    n  st m a)
+                -> (c -> Server  ps (Pipelined c)    n  st m a)
                 -- ^ continuation
-                -> Server        ps ('Pipelined c) (S n) st m a
+                -> Server        ps (Pipelined c) (S n) st m a
 pattern Collect k' k = TP.Collect k' k
 
 

typed-protocols/src/Network/TypedProtocol/Proofs.hs

@@ -172,8 +172,13 @@ forgetPipelined
   :: forall ps (pr :: PeerRole) (st :: ps) c m a.
      Functor m
   => [Bool]
-  -> Peer ps pr ('Pipelined c) Z st m a
-  -> Peer ps pr 'NonPipelined  Z st m a
+  -- ^ interleaving choices for pipelining allowed by
+  -- `Collect` and `CollectSTM` primitive. False values or `[]` give no
+  -- pipelining.  For the 'CollectSTM' primitive, the stm action must not
+  -- block otherwise even if the choice is to pipeline more (a 'True' value),
+  -- we'll actually collect a result.
+  -> Peer ps pr (Pipelined c) Z st m a
+  -> Peer ps pr  NonPipelined  Z st m a
 forgetPipelined = goSender EmptyQ
   where
     goSender :: forall st' n.