SCP-4701 - Add kind annotations to (Client|Server)HasAgency constru…

…ctors
input-output-hk · Nov 24, 2022 · 20a9a85 · 20a9a85
1 parent 6b1138a
commit 20a9a85
Show file tree

Hide file tree

Showing 6 changed files with 30 additions and 51 deletions.
diff --git a/marlowe-protocols/src/Network/Protocol/ChainSeek/Codec.hs b/marlowe-protocols/src/Network/Protocol/ChainSeek/Codec.hs
@@ -17,7 +17,6 @@ import Data.Type.Equality (type (:~:)(Refl))
 import Network.Protocol.ChainSeek.Types
 import Network.Protocol.Codec (DeserializeError, GetMessage, PutMessage, binaryCodec)
 import Network.TypedProtocol.Codec
-import Unsafe.Coerce (unsafeCoerce)
 
 codecChainSeek
   :: forall query point tip m
@@ -51,14 +50,14 @@ codecChainSeek = binaryCodec putMsg getMsg
 
     putMsg (ServerAgency (TokNext tag _)) (MsgRejectQuery err tip) = do
         putWord8 0x05
-        putTag $ coerceTag tag
-        putErr (coerceTag tag) err
+        putTag tag
+        putErr tag err
         put tip
 
     putMsg (ServerAgency (TokNext tag _)) (MsgRollForward result pos tip) = do
         putWord8 0x06
-        putTag $ coerceTag tag
-        putResult (coerceTag tag) result
+        putTag tag
+        putResult tag result
         put pos
         put tip
 
@@ -91,7 +90,7 @@ codecChainSeek = binaryCodec putMsg getMsg
 
         (0x05, ServerAgency (TokNext qtag _)) -> do
           SomeTag qtag' :: SomeTag query <- getTag
-          case tagEq (coerceTag qtag) qtag' of
+          case tagEq qtag qtag' of
             Nothing -> fail "decoded query tag does not match expected query tag"
             Just (Refl, Refl) -> do
               err <- getErr qtag'
@@ -100,7 +99,7 @@ codecChainSeek = binaryCodec putMsg getMsg
 
         (0x06, ServerAgency (TokNext qtag _)) -> do
           SomeTag qtag' :: SomeTag query <- getTag
-          case tagEq (coerceTag qtag) qtag' of
+          case tagEq qtag qtag' of
             Nothing -> fail "decoded query tag does not match expected query tag"
             Just (Refl, Refl) -> do
               result <- getResult qtag'
@@ -121,9 +120,3 @@ codecChainSeek = binaryCodec putMsg getMsg
 
         _ -> fail $ "Unexpected tag " <> show tag
 
-    -- Unfortunately, the poly-kinded query parameter doesn't play nicely with
-    -- the `PeerHasAgency` type and it gets confused, thinking that 'query1'
-    -- and 'query' are unrelated types. So we have to coerce them (they will
-    -- absolutely be the same type constructor though).
-    coerceTag :: forall query1 err result. Tag query1 err result -> Tag query err result
-    coerceTag = unsafeCoerce
diff --git a/marlowe-protocols/src/Network/Protocol/ChainSeek/Types.hs b/marlowe-protocols/src/Network/Protocol/ChainSeek/Types.hs
@@ -147,7 +147,7 @@ instance Protocol (ChainSeek query point tip) where
 
   data ServerHasAgency st where
     TokHandshake :: ServerHasAgency 'StHandshake
-    TokNext :: Tag query err result -> TokNextKind k -> ServerHasAgency ('StNext err result k)
+    TokNext :: Tag query err result -> TokNextKind k -> ServerHasAgency ('StNext err result k :: ChainSeek query point tip)
 
   data NobodyHasAgency st where
     TokFault :: NobodyHasAgency 'StFault

diff --git a/marlowe-protocols/src/Network/Protocol/Job/Codec.hs b/marlowe-protocols/src/Network/Protocol/Job/Codec.hs
@@ -14,7 +14,6 @@ import Data.Type.Equality (type (:~:)(Refl))
 import Network.Protocol.Codec (DeserializeError, GetMessage, PutMessage, binaryCodec)
 import Network.Protocol.Job.Types
 import Network.TypedProtocol.Codec
-import Unsafe.Coerce (unsafeCoerce)
 
 codecJob
   :: forall cmd m
@@ -38,16 +37,16 @@ codecJob = binaryCodec putMsg getMsg
       ServerAgency (TokCmd tag) -> \case
         MsgFail err -> do
           putWord8 0x03
-          putTag (coerceTag tag)
-          putErr (coerceTag tag) err
+          putTag tag
+          putErr tag err
         MsgSucceed result -> do
           putWord8 0x04
-          putTag (coerceTag tag)
-          putResult (coerceTag tag) result
+          putTag tag
+          putResult tag result
         MsgAwait status jobId -> do
           putWord8 0x05
-          putTag (coerceTag tag)
-          putStatus (coerceTag tag) status
+          putTag tag
+          putStatus tag status
           putJobId jobId
       ClientAgency (TokAwait _) -> \case
         MsgPoll   -> putWord8 0x06
@@ -73,21 +72,21 @@ codecJob = binaryCodec putMsg getMsg
         0x03 -> case tok of
           ServerAgency (TokCmd ctag) -> do
             SomeTag ctag' <- getTag
-            case tagEq (coerceTag ctag) ctag' of
+            case tagEq ctag ctag' of
               Nothing                 -> fail "decoded command tag does not match expected command tag"
               Just (Refl, Refl, Refl) -> SomeMessage . MsgFail <$> getErr ctag'
           _ -> fail "Invalid protocol state for MsgFail"
         0x04 -> case tok of
           ServerAgency (TokCmd ctag) -> do
             SomeTag ctag' <- getTag
-            case tagEq (coerceTag ctag) ctag' of
+            case tagEq ctag ctag' of
               Nothing                 -> fail "decoded command tag does not match expected command tag"
               Just (Refl, Refl, Refl) -> SomeMessage . MsgSucceed <$> getResult ctag'
           _ -> fail "Invalid protocol state for MsgSucceed"
         0x05 -> case tok of
           ServerAgency (TokCmd ctag) -> do
             SomeTag ctag' <- getTag
-            case tagEq (coerceTag ctag) ctag' of
+            case tagEq ctag ctag' of
               Nothing                 -> fail "decoded command tag does not match expected command tag"
               Just (Refl, Refl, Refl) -> SomeMessage <$> (MsgAwait <$> getStatus ctag' <*> getJobId ctag')
           _ -> fail "Invalid protocol state for MsgAwait"
@@ -105,9 +104,3 @@ codecJob = binaryCodec putMsg getMsg
           _                          -> fail "Invalid protocol state for MsgAttachFailed"
         _ -> fail $ "Invalid msg tag " <> show tag
 
-    -- Unfortunately, the poly-kinded cmd parameter doesn't play nicely with
-    -- the `PeerHasAgency` type and it gets confused, thinking that cmd1
-    -- and 'cmd' are unrelated types. So we have to coerce them (they will
-    -- absolutely be the same type constructor though).
-    coerceTag :: forall cmd1 status err result. Tag cmd1 status err result -> Tag cmd status err result
-    coerceTag = unsafeCoerce
diff --git a/marlowe-protocols/src/Network/Protocol/Job/Types.hs b/marlowe-protocols/src/Network/Protocol/Job/Types.hs
@@ -130,10 +130,10 @@ instance Protocol (Job cmd) where
 
   data ClientHasAgency st where
     TokInit :: ClientHasAgency 'StInit
-    TokAwait :: Tag cmd status err result -> ClientHasAgency ('StAwait status err result)
+    TokAwait :: Tag cmd status err result -> ClientHasAgency ('StAwait status err result :: Job cmd)
 
   data ServerHasAgency st where
-    TokCmd :: Tag cmd status err result -> ServerHasAgency ('StCmd status err result)
+    TokCmd :: Tag cmd status err result -> ServerHasAgency ('StCmd status err result :: Job cmd)
     TokAttach :: Tag cmd status err result -> ServerHasAgency ('StAttach status err result)
 
   data NobodyHasAgency st where

diff --git a/marlowe-protocols/src/Network/Protocol/Query/Codec.hs b/marlowe-protocols/src/Network/Protocol/Query/Codec.hs
@@ -14,7 +14,6 @@ import Data.Type.Equality (type (:~:)(Refl))
 import Network.Protocol.Codec (DeserializeError, GetMessage, PutMessage, binaryCodec)
 import Network.Protocol.Query.Types
 import Network.TypedProtocol.Codec
-import Unsafe.Coerce (unsafeCoerce)
 
 codecQuery
   :: forall query m
@@ -32,20 +31,20 @@ codecQuery = binaryCodec putMsg getMsg
       ServerAgency (TokNext _ tag) -> \case
         MsgReject err -> do
           putWord8 0x02
-          putTag (coerceTag tag)
-          putErr (coerceTag tag) err
+          putTag tag
+          putErr tag err
         MsgNextPage results delimiter -> do
           putWord8 0x03
-          putTag (coerceTag tag)
-          putResult (coerceTag tag) results
+          putTag tag
+          putResult tag results
           case delimiter of
             Nothing -> putWord8 0x01
-            Just d  -> putDelimiter (coerceTag tag) d
+            Just d  -> putDelimiter tag d
       ClientAgency (TokPage tag) -> \case
         MsgRequestNext delimiter -> do
           putWord8 0x04
-          putTag (coerceTag tag)
-          putDelimiter (coerceTag tag) delimiter
+          putTag tag
+          putDelimiter tag delimiter
         MsgDone -> putWord8 0x05
 
     getMsg :: GetMessage (Query query)
@@ -60,14 +59,14 @@ codecQuery = binaryCodec putMsg getMsg
         0x02 -> case tok of
           ServerAgency (TokNext TokCanReject qtag) -> do
             SomeTag qtag' :: SomeTag query <- getTag
-            case tagEq (coerceTag qtag) qtag' of
+            case tagEq qtag qtag' of
               Nothing                 -> fail "decoded query tag does not match expected query tag"
               Just (Refl, Refl, Refl) -> SomeMessage . MsgReject <$> getErr qtag'
           _ -> fail "Invalid protocol state for MsgReject"
         0x03 -> case tok of
           ServerAgency (TokNext _ qtag) -> do
             SomeTag qtag' :: SomeTag query <- getTag
-            case tagEq (coerceTag qtag) qtag' of
+            case tagEq qtag qtag' of
               Nothing   -> fail "decoded query tag does not match expected query tag"
               Just (Refl, Refl, Refl) -> do
                 result <- getResult qtag'
@@ -81,7 +80,7 @@ codecQuery = binaryCodec putMsg getMsg
         0x04 -> case tok of
           ClientAgency (TokPage qtag) -> do
             SomeTag qtag' :: SomeTag query <- getTag
-            case tagEq (coerceTag qtag) qtag' of
+            case tagEq qtag qtag' of
               Nothing                 -> fail "decoded query tag does not match expected query tag"
               Just (Refl, Refl, Refl) -> SomeMessage . MsgRequestNext <$> getDelimiter qtag'
           _                            -> fail "Invalid protocol state for MsgRequestNext"
@@ -90,9 +89,3 @@ codecQuery = binaryCodec putMsg getMsg
           _                        -> fail "Invalid protocol state for MsgDone"
         _ -> fail $ "Invalid msg tag " <> show tag
 
-    -- Unfortunately, the poly-kinded query parameter doesn't play nicely with
-    -- the `PeerHasAgency` type and it gets confused, thinking that 'query1'
-    -- and 'query' are unrelated types. So we have to coerce them (they will
-    -- absolutely be the same type constructor though).
-    coerceTag :: forall query1 delimiter err results. Tag query1 delimiter err results -> Tag query delimiter err results
-    coerceTag = unsafeCoerce
diff --git a/marlowe-protocols/src/Network/Protocol/Query/Types.hs b/marlowe-protocols/src/Network/Protocol/Query/Types.hs
@@ -91,10 +91,10 @@ instance Protocol (Query query) where
 
   data ClientHasAgency st where
     TokInit :: ClientHasAgency 'StInit
-    TokPage :: Tag query delimiter err results -> ClientHasAgency ('StPage delimiter err results)
+    TokPage :: Tag query delimiter err results -> ClientHasAgency ('StPage delimiter err results :: Query query)
 
   data ServerHasAgency st where
-    TokNext :: TokNextKind k -> Tag query delimiter err results -> ServerHasAgency ('StNext k delimiter err results)
+    TokNext :: TokNextKind k -> Tag query delimiter err results -> ServerHasAgency ('StNext k delimiter err results :: Query query)
 
   data NobodyHasAgency st where
     TokDone :: NobodyHasAgency 'StDone