typed-protocols: simplify evidence of termination in a terminal state

The simplest solution seem to add `StateAgency st ~ NobodyAgency` to the
`Done` constructor.  Which can be carried over to `TerminalStates`.

typed-protocols-examples/test/Network/TypedProtocol/PingPong/Tests.hs

@@ -18,7 +18,6 @@ module Network.TypedProtocol.PingPong.Tests
 
 import           Network.TypedProtocol.Channel
 import           Network.TypedProtocol.Codec
-import           Network.TypedProtocol.Core
 import           Network.TypedProtocol.Driver.Simple
 import           Network.TypedProtocol.Proofs
 
@@ -196,11 +195,7 @@ prop_connect (NonNegative n) =
            (pingPongClientPeer (pingPongClientCount n))
            (pingPongServerPeer  pingPongServerCount))
 
-    of ((), n', TerminalStates SingDone
-                               ReflNobodyAgency
-                               SingDone
-                               ReflNobodyAgency) ->
-        n == n'
+    of ((), n', TerminalStates SingDone SingDone) -> n == n'
 
 
 --
@@ -219,11 +214,7 @@ connect_pipelined client cs =
          (connectPipelined cs []
             (pingPongClientPeerPipelined client)
             (promoteToPipelined $ pingPongServerPeer pingPongServerCount))
-
-    of (reqResps, n, TerminalStates SingDone
-                                    ReflNobodyAgency
-                                    SingDone
-                                    ReflNobodyAgency) ->
+    of (reqResps, n, TerminalStates SingDone SingDone) ->
          (n, reqResps)
 
 

typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs

@@ -1,15 +1,11 @@
-{-# LANGUAGE BangPatterns             #-}
 {-# LANGUAGE CPP                      #-}
 {-# LANGUAGE DataKinds                #-}
 {-# LANGUAGE FlexibleInstances        #-}
 {-# LANGUAGE GADTs                    #-}
 {-# LANGUAGE NamedFieldPuns           #-}
 {-# LANGUAGE PolyKinds                #-}
 {-# LANGUAGE ScopedTypeVariables      #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TupleSections            #-}
-{-# LANGUAGE TypeApplications         #-}
-{-# LANGUAGE TypeOperators            #-}
 
 -- orphaned arbitrary instances
 {-# OPTIONS_GHC -Wno-orphans #-}
@@ -19,7 +15,6 @@ module Network.TypedProtocol.ReqResp.Tests (tests) where
 
 import           Network.TypedProtocol.Channel
 import           Network.TypedProtocol.Codec
-import           Network.TypedProtocol.Core
 import           Network.TypedProtocol.Driver.Simple
 import           Network.TypedProtocol.Proofs
 
@@ -163,10 +158,7 @@ prop_connect f xs =
              (reqRespClientPeer (reqRespClientMap xs))
              (reqRespServerPeer (reqRespServerMapAccumL (\a -> pure . f a) 0)))
 
-      of (c, s, TerminalStates SingDone
-                               ReflNobodyAgency
-                               SingDone
-                               ReflNobodyAgency) ->
+      of (c, s, TerminalStates SingDone SingDone) ->
            (s, c) == mapAccumL f 0 xs
 
 
@@ -178,10 +170,7 @@ prop_connectPipelined cs f xs =
              (promoteToPipelined $ reqRespServerPeer
                (reqRespServerMapAccumL (\a -> pure . f a) 0)))
 
-      of (c, s, TerminalStates SingDone
-                               ReflNobodyAgency
-                               SingDone
-                               ReflNobodyAgency) ->
+      of (c, s, TerminalStates SingDone SingDone) ->
            (s, c) == mapAccumL f 0 xs
 
 

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

@@ -181,7 +181,9 @@ data Peer ps pr pl n st m a where
   --
   Done
     :: forall ps pr pl (st :: ps) m a.
-       SingI st
+       ( SingI st
+       , StateAgency st ~ NobodyAgency
+       )
     => NobodyHasAgencyProof pr st
     -- ^ (no) agency proof
     -> a

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

@@ -7,6 +7,7 @@
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
 
 
 -- This is already implied by the -Wall in the .cabal file, but lets just be
@@ -82,7 +83,7 @@ connect
       (Monad m, SingI pr)
    => Peer ps             pr  NonPipelined Z initSt m a
    -> Peer ps (FlipAgency pr) NonPipelined Z initSt m b
-   -> m (a, b, TerminalStates ps pr)
+   -> m (a, b, TerminalStates ps)
 connect = go
   where
     singPeerRole :: Sing pr
@@ -91,14 +92,14 @@ connect = go
     go :: forall (st :: ps).
           Peer ps             pr  NonPipelined Z st m a
        -> Peer ps (FlipAgency pr) NonPipelined Z st m b
-       -> m (a, b, TerminalStates ps pr)
-    go (Done reflA a)  (Done reflB b)  = return (a, b, terminals)
+       -> m (a, b, TerminalStates ps)
+    go (Done ReflNobodyAgency a)  (Done ReflNobodyAgency b) =
+        return (a, b, terminals)
       where
-        terminals :: TerminalStates ps pr
+        terminals :: TerminalStates ps
         terminals = TerminalStates (sing :: Sing st)
-                                    reflA
                                    (sing :: Sing st)
-                                    reflB
+
     go (Effect a )      b              = a >>= \a' -> go a' b
     go  a              (Effect b)      = b >>= \b' -> go a  b'
     go (Yield _ msg a) (Await _ b)     = go  a     (b msg)
@@ -134,18 +135,13 @@ connect = go
 -- | The terminal states for the protocol. Used in 'connect' and
 -- 'connectPipelined' to return the states in which the peers terminated.
 --
-data TerminalStates ps (pr :: PeerRole) where
+data TerminalStates ps where
      TerminalStates
-       :: forall ps pr (st :: ps) (st' :: ps).
-          Sing st
-       -> ReflRelativeAgency (StateAgency st)
-                              NobodyHasAgency
-                             (Relative             pr  (StateAgency st))
-       -> Sing st'
-       -> ReflRelativeAgency (StateAgency st')
-                              NobodyHasAgency
-                             (Relative (FlipAgency pr) (StateAgency st'))
-       -> TerminalStates ps pr
+       :: forall ps (st :: ps).
+          (StateAgency st  ~ NobodyAgency)
+       => Sing st
+       -> Sing st
+       -> TerminalStates ps
 
 --
 -- Remove Pipelining
@@ -248,7 +244,7 @@ connectPipelined
     -> [Bool]
     -> Peer ps             pr  ('Pipelined c)  Z st m a
     -> Peer ps (FlipAgency pr) ('Pipelined c') Z st m b
-    -> m (a, b, TerminalStates ps pr)
+    -> m (a, b, TerminalStates ps)
 connectPipelined csA csB a b =
     connect (forgetPipelined csA a)
             (forgetPipelined csB b)