diff --git a/cabal.project b/cabal.project
index 4c697357..8e1227c1 100644
--- a/cabal.project
+++ b/cabal.project
@@ -19,7 +19,7 @@ packages: ./typed-protocols
           ./typed-protocols-stateful
           ./typed-protocols-stateful-cborg
           ./typed-protocols-examples
-          -- ./typed-protocols-doc
+          ./typed-protocols-doc
 
 test-show-details: direct
 
@@ -30,3 +30,7 @@ if impl (ghc >= 9.12)
     , cborg:ghc-prim
     , serialise:base
     , serialise:ghc-prim
+
+if(os(windows))
+  package text
+    flags: -simdutf
diff --git a/typed-protocols-doc/demo/DemoProtocol.hs b/typed-protocols-doc/demo/DemoProtocol.hs
index 01364eb6..b60d56d4 100644
--- a/typed-protocols-doc/demo/DemoProtocol.hs
+++ b/typed-protocols-doc/demo/DemoProtocol.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -12,19 +13,23 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 
+-- for `deriveSerDoc`
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 module DemoProtocol
 where
 
-import Network.TypedProtocol.Core
-import Data.SerDoc.Info
 import Control.Monad.Identity
 import Control.Monad.Except
+
 import Data.Proxy
-import Data.Word
-import Data.Typeable
 import Data.SerDoc.Class
+import Data.SerDoc.Info
 import Data.SerDoc.TH
 import Data.Text (Text)
+import Data.Word
+
+import Network.TypedProtocol.Core
 
 data PongInfo =
   PongInfo
@@ -44,6 +49,15 @@ data DemoProtocol a where
   -- | End state: either side has terminated the session
   EndState :: DemoProtocol a
 
+data SingDemoProtocol a where
+    SingIdleState         :: SingDemoProtocol (IdleState         :: DemoProtocol a)
+    SingAwaitingPongState :: SingDemoProtocol (AwaitingPongState :: DemoProtocol a)
+    SingEndState          :: SingDemoProtocol (EndState          :: DemoProtocol a)
+
+instance StateTokenI IdleState         where stateToken = SingIdleState
+instance StateTokenI AwaitingPongState where stateToken = SingAwaitingPongState
+instance StateTokenI EndState          where stateToken = SingEndState
+
 instance Protocol (DemoProtocol a) where
   data Message (DemoProtocol a) st st' where
     PingMessage :: Message (DemoProtocol a) IdleState AwaitingPongState
@@ -51,27 +65,13 @@ instance Protocol (DemoProtocol a) where
     ComplexPongMessage :: Message (DemoProtocol a) AwaitingPongState IdleState
     EndMessage :: Message (DemoProtocol a) st EndState
 
-  data ServerHasAgency st where
-    TokIdle :: ServerHasAgency IdleState
-
-  data ClientHasAgency st where
-    TokAwaitingPongState :: ClientHasAgency AwaitingPongState
-
-  data NobodyHasAgency st where
-    TokEnd :: NobodyHasAgency EndState
-
+  type StateAgency IdleState         = ServerAgency
+  type StateAgency AwaitingPongState = ClientAgency
+  type StateAgency EndState          = NobodyAgency
 
-  exclusionLemma_ClientAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokAwaitingPongState -> case tok2 of {}
+  type StateToken = SingDemoProtocol
 
-  exclusionLemma_NobodyAndClientHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
 
-  exclusionLemma_NobodyAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
 
 data DemoCodec a
 
diff --git a/typed-protocols-doc/src/Network/TypedProtocol/Documentation/DefaultMain.hs b/typed-protocols-doc/src/Network/TypedProtocol/Documentation/DefaultMain.hs
index b293094d..a8dfe744 100644
--- a/typed-protocols-doc/src/Network/TypedProtocol/Documentation/DefaultMain.hs
+++ b/typed-protocols-doc/src/Network/TypedProtocol/Documentation/DefaultMain.hs
@@ -65,8 +65,7 @@ pMainOptions =
           )
 
 
-defaultMain :: ( Codec codec
-               , HasInfo codec (DefEnumEncoding codec)
+defaultMain :: ( HasInfo codec (DefEnumEncoding codec)
                , HasInfo codec Word32
                ) => [ProtocolDescription codec] -> IO ()
 defaultMain descriptions = do
@@ -79,8 +78,7 @@ defaultMain descriptions = do
         render = getRenderer (moOutputFormat mainOptions) (moOutputFile mainOptions)
     write . render $ descriptions
 
-getRenderer :: ( Codec codec
-               , HasInfo codec (DefEnumEncoding codec)
+getRenderer :: ( HasInfo codec (DefEnumEncoding codec)
                , HasInfo codec Word32
                )
             => OutputFormat
diff --git a/typed-protocols-doc/src/Network/TypedProtocol/Documentation/TH.hs b/typed-protocols-doc/src/Network/TypedProtocol/Documentation/TH.hs
index 79ecfe2d..6c2acffa 100644
--- a/typed-protocols-doc/src/Network/TypedProtocol/Documentation/TH.hs
+++ b/typed-protocols-doc/src/Network/TypedProtocol/Documentation/TH.hs
@@ -15,6 +15,7 @@ import Control.Monad
 -- This import is only needed when 'getDoc' is available.
 import Data.Maybe (maybeToList)
 #endif
+import Data.Maybe (mapMaybe)
 import Data.Proxy
 import Language.Haskell.TH
 import Language.Haskell.TH.Datatype
@@ -34,45 +35,29 @@ describeProtocol protoTyCon protoTyArgs codecTyCon codecTyArgs = do
   protoDescription <- getDescription protoTyCon
   let pname = nameBase (datatypeName info)
 
-  let extractMessageStateNames :: InstanceDec -> [Name]
-      extractMessageStateNames (DataInstD _ _ _ _ tys _) =
-        [ case ty of
-            ForallC _ _ (GadtC _ _ ty') -> go ty'
-            GadtC _ _ ty' -> go ty'
-            _ -> error $ "Not a GADT: " ++ show ty
-        | ty <- tys
-        ]
-        where
-          go (PromotedT tyName) = tyName
-          go (SigT ty' _) = go ty'
-          go (AppT _ ty') = go ty'
-          go ty' = error $ "Cannot detect message name from type: " ++ show ty'
-      extractMessageStateNames i = error $ "Not a DataInstD: " ++ show i
+  let extractAgency :: InstanceDec -> Maybe Name
+      extractAgency (TySynInstD (TySynEqn _ _ (PromotedT agency))) = Just agency
+      extractAgency dec = error $ "Unexpected InstanceDec: " ++ show dec
+
+  let extractAgencies :: [InstanceDec] -> [Name]
+      extractAgencies = mapMaybe extractAgency
+
+  let extractTheAgency :: [InstanceDec] -> Name
+      extractTheAgency inst = case extractAgencies inst of
+        [agency] -> agency
+        xs -> error $ "Incorrect number of agencies: " ++ show xs
 
   pstates <- forM (datatypeCons info) $ \conInfo -> do
     let conName = constructorName conInfo
     stateDescription <- getDescription conName
 
-    serverAgencies <- reifyInstances ''ServerHasAgency [ConT conName]
-    let serverAgencies' =
-          [ nameBase tyName
-          | inst <- serverAgencies
-          , tyName <- extractMessageStateNames inst
-          , nameBase tyName == nameBase conName
-          ]
-    clientAgencies <- reifyInstances ''ClientHasAgency [ConT conName]
-    let clientAgencies' =
-          [ nameBase tyName
-          | inst <- clientAgencies
-          , tyName <- extractMessageStateNames inst
-          , nameBase tyName == nameBase conName
-          ]
-
-    let agencyID = case (serverAgencies', clientAgencies') of
-          ([], []) -> NobodyAgencyID
-          (_, []) -> ServerAgencyID
-          ([], _) -> ClientAgencyID
-          _ -> error $ show (nameBase conName, serverAgencies', clientAgencies')
+    stateAgencies <- reifyInstances ''StateAgency [ConT conName]
+    let agencyName = extractTheAgency stateAgencies
+        agencyID = case nameBase agencyName of
+          "ServerAgency" -> 'ServerAgencyID
+          "ClientAgency" -> 'ClientAgencyID
+          "NobodyAgency" -> 'NobodyAgencyID
+          x -> error $ "Unknown agency type " ++ x ++ " in state " ++ nameBase conName
 
     return (conName, stateDescription, agencyID)
 
@@ -87,7 +72,7 @@ describeProtocol protoTyCon protoTyArgs codecTyCon codecTyArgs = do
         protoDescription
         ""
         $(listE
-            [ [| ( $(makeState $ ConT conName), stateDescription, agencyID) |]
+            [ [| ( $(makeState $ ConT conName), stateDescription, $(conE agencyID)) |]
             | (conName, stateDescription, agencyID) <- pstates
             ]
          )
diff --git a/typed-protocols-doc/test/Network/TypedProtocol/Tests/ControlProtocol.hs b/typed-protocols-doc/test/Network/TypedProtocol/Tests/ControlProtocol.hs
index 520f44bb..69553f19 100644
--- a/typed-protocols-doc/test/Network/TypedProtocol/Tests/ControlProtocol.hs
+++ b/typed-protocols-doc/test/Network/TypedProtocol/Tests/ControlProtocol.hs
@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE EmptyCase #-}
@@ -30,10 +32,10 @@ import Data.Typeable
 import Data.Word
 import Network.TypedProtocol.Core
 
-data AgentInfo c =
+data AgentInfo =
   AgentInfo
-    { agentInfoCurrentBundle :: !(Maybe (BundleInfo c))
-    , agentInfoStagedKey :: !(Maybe (KeyInfo c))
+    { agentInfoCurrentBundle :: !(Maybe BundleInfo)
+    , agentInfoStagedKey :: !(Maybe KeyInfo)
     , agentInfoBootstrapConnections :: ![BootstrapInfo]
     }
     deriving (Show, Eq)
@@ -50,7 +52,6 @@ deriving via (ViaEnum Command)
   instance
     ( Codec codec
     , HasInfo codec (DefEnumEncoding codec)
-    , Integral (DefEnumEncoding codec)
     ) => HasInfo codec Command
 
 instance
@@ -63,16 +64,16 @@ instance
     encode codec = encodeEnum codec (Proxy @(DefEnumEncoding codec))
     decode codec = decodeEnum codec (Proxy @(DefEnumEncoding codec))
 
-newtype FakeKey k = FakeKey { fakeKeyData :: ByteString }
+newtype FakeKey = FakeKey { fakeKeyData :: ByteString }
   deriving (Show, Eq, Ord)
 
 newtype VersionIdentifier = VersionIdentifier { versionIdentifierData :: ByteString }
   deriving (Show, Eq, Ord)
 
-instance HasInfo (TestCodec ()) VersionIdentifier where
+instance HasInfo TestCodec VersionIdentifier where
   info _ _ = basicField "Bytes" (FixedSize 32)
 
-instance HasInfo (TestCodec ()) (FakeKey k) where
+instance HasInfo TestCodec FakeKey where
   info _ _ = basicField "Bytes" (FixedSize 128)
 
 data BootstrapInfo =
@@ -92,25 +93,25 @@ deriving via (ViaEnum ConnectionStatus)
   instance (Codec codec, HasInfo codec (DefEnumEncoding codec))
     => HasInfo codec ConnectionStatus
 
-data BundleInfo c =
+data BundleInfo =
   BundleInfo
     { bundleInfoEvolution :: !Word32
     , bundleInfoOCertN :: !Word64
-    , bundleInfoVK :: !(FakeKey c)
+    , bundleInfoVK :: !FakeKey
     }
     deriving (Show, Eq)
 
-newtype KeyInfo c =
+newtype KeyInfo =
   KeyInfo
-    { keyInfoVK :: FakeKey c
+    { keyInfoVK :: FakeKey
     }
     deriving (Show, Eq)
 
 deriving newtype
   instance
-    ( HasInfo codec (FakeKey c)
+    ( HasInfo codec FakeKey
     , Codec codec
-    ) => HasInfo codec (KeyInfo c)
+    ) => HasInfo codec KeyInfo
 
 $(deriveSerDoc ''TestCodec [] ''BundleInfo)
 $(deriveSerDoc ''TestCodec [] ''BootstrapInfo)
@@ -129,27 +130,27 @@ $(deriveSerDoc ''TestCodec [] ''AgentInfo)
 -- through. This allows the control client to report success to the user, but it
 -- also helps make things more predictable in testing, because it means that
 -- sending keys is now synchronous.
-data ControlProtocol (m :: Type -> Type) (k :: Type) where
+data ControlProtocol (m :: Type -> Type) (c :: Type) where
   -- | Default state after connecting, but before the protocol version has been
   -- negotiated.
-  InitialState :: ControlProtocol m k
+  InitialState :: ControlProtocol m c
 
   -- | System is idling, waiting for the server to push the next key.
-  IdleState :: ControlProtocol m k
+  IdleState :: ControlProtocol m c
 
   -- | Client has requested a new KES key to be generated in the staging area.
-  WaitForPublicKeyState :: ControlProtocol m k
+  WaitForPublicKeyState :: ControlProtocol m c
 
   -- | Client has requested agent information
-  WaitForInfoState :: ControlProtocol m k
+  WaitForInfoState :: ControlProtocol m c
 
   -- | An OpCert has been pushed, client must now confirm that it has been
   -- received, and that it matches the staged KES key.
-  WaitForConfirmationState :: ControlProtocol m k
+  WaitForConfirmationState :: ControlProtocol m c
 
   -- | The server has closed the connection, thus signalling the end of the
   -- session.
-  EndState :: ControlProtocol m k
+  EndState :: ControlProtocol m c
 
 {-# ANN VersionMessage (Description ["Announce the protocol version."]) #-}
 {-# ANN GenStagedKeyMessage
@@ -217,10 +218,10 @@ instance Protocol (ControlProtocol m c) where
 
           DropStagedKeyMessage :: Message (ControlProtocol m c) IdleState WaitForPublicKeyState
 
-          PublicKeyMessage :: Maybe (FakeKey c)
+          PublicKeyMessage :: Maybe FakeKey
                            -> Message (ControlProtocol m c) WaitForPublicKeyState IdleState
 
-          InstallKeyMessage :: FakeKey c
+          InstallKeyMessage :: FakeKey
                             -> Message (ControlProtocol m c) IdleState WaitForConfirmationState
 
           InstallResultMessage :: Word32
@@ -228,7 +229,7 @@ instance Protocol (ControlProtocol m c) where
 
           RequestInfoMessage :: Message (ControlProtocol m c) IdleState WaitForInfoState
 
-          InfoMessage :: AgentInfo c
+          InfoMessage :: AgentInfo
                       -> Message (ControlProtocol m c) WaitForInfoState IdleState
 
           AbortMessage :: Message (ControlProtocol m c) InitialState EndState
@@ -236,42 +237,30 @@ instance Protocol (ControlProtocol m c) where
           ProtocolErrorMessage :: Message (ControlProtocol m c) a EndState
 
   -- | Server always has agency, except between sending a key and confirming it
-  data ServerHasAgency st where
-    TokInitial :: ServerHasAgency InitialState
-    TokIdle :: ServerHasAgency IdleState
-
-  -- | Client only has agency between sending a key and confirming it
-  data ClientHasAgency st where
-    TokWaitForConfirmation :: ClientHasAgency WaitForConfirmationState
-    TokWaitForPublicKey :: ClientHasAgency WaitForPublicKeyState
-    TokWaitForInfo :: ClientHasAgency WaitForInfoState
-
-  -- | Someone, i.e., the server, always has agency
-  data NobodyHasAgency st where
-    TokEnd :: NobodyHasAgency EndState
-
-  exclusionLemma_ClientAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokWaitForConfirmation ->
-        case tok2 of {}
-      TokWaitForPublicKey ->
-        case tok2 of {}
-      TokWaitForInfo ->
-        case tok2 of {}
-  exclusionLemma_NobodyAndClientHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
-  exclusionLemma_NobodyAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
-
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) InitialState IdleState) where
+  type StateAgency InitialState = ServerAgency
+  type StateAgency IdleState = ServerAgency
+  type StateAgency WaitForConfirmationState = ClientAgency
+  type StateAgency WaitForPublicKeyState = ClientAgency
+  type StateAgency WaitForInfoState = ClientAgency
+  type StateAgency EndState = NobodyAgency
+
+  type StateToken = SControlProtocol
+
+data SControlProtocol (st :: ControlProtocol m c) where
+  SInitialState :: SControlProtocol InitialState
+  SIdleState :: SControlProtocol IdleState
+  SWaitForConfirmationState :: SControlProtocol WaitForConfirmationState
+  SWaitForPublicKeyState :: SControlProtocol WaitForPublicKeyState
+  SWaitForInfoState :: SControlProtocol WaitForInfoState
+  SEndState :: SControlProtocol EndState
+
+instance HasInfo TestCodec (Message (ControlProtocol m c) InitialState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "InitialState,IdleState" ++
               ">")
             (info codec (Proxy @VersionIdentifier))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitForPublicKeyState) where
+instance HasInfo TestCodec (Message (ControlProtocol m c) IdleState WaitForPublicKeyState) where
   info codec _ = aliasField
             ("Message<" ++
               "IdleState,WaitForPublicKeyState" ++
@@ -283,39 +272,39 @@ instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitFor
 --    QueryStagedKeyMessage -> infoOf QueryStagedKeyCmd
 --    DropStagedKeyMessage -> infoOf DropStagedKeyCmd
 
-instance (HasInfo (TestCodec ()) (FakeKey c)) => HasInfo (TestCodec ()) (Message (ControlProtocol m c) WaitForPublicKeyState IdleState) where
+instance (HasInfo TestCodec FakeKey) => HasInfo TestCodec (Message (ControlProtocol m c) WaitForPublicKeyState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "WaitForPublicKeyState,IdleState" ++
               ">")
-            (info codec (Proxy @(Maybe (FakeKey c))))
-instance (HasInfo (TestCodec ()) (FakeKey c)) => HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitForConfirmationState) where
+            (info codec (Proxy @(Maybe FakeKey)))
+instance (HasInfo TestCodec FakeKey) => HasInfo TestCodec (Message (ControlProtocol m c) IdleState WaitForConfirmationState) where
   info codec _ = aliasField
             ("Message<" ++
               "IdleState,WaitForConfirmationState" ++
               ">")
-            (info codec (Proxy @(FakeKey c)))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) WaitForConfirmationState IdleState) where
+            (info codec (Proxy @FakeKey))
+instance HasInfo TestCodec (Message (ControlProtocol m c) WaitForConfirmationState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "WaitForConfirmationState,IdleState" ++
               ">")
             (info codec (Proxy @Word32))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitForInfoState) where
+instance HasInfo TestCodec (Message (ControlProtocol m c) IdleState WaitForInfoState) where
   info codec _ = aliasField
             ("Message<" ++
               "IdleState,WaitForInfoState" ++
               ">")
             (info codec (Proxy @()))
-instance ( HasInfo (TestCodec ()) (FakeKey c)
-         , HasInfo (TestCodec ()) (AgentInfo c)
-         ) => HasInfo (TestCodec ()) (Message (ControlProtocol m c) WaitForInfoState IdleState) where
+instance ( HasInfo TestCodec FakeKey
+         , HasInfo TestCodec AgentInfo
+         ) => HasInfo TestCodec (Message (ControlProtocol m c) WaitForInfoState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "WaitForInfoState,IdleState" ++
               ">")
-            (info codec (Proxy @(AgentInfo c)))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) _st EndState) where
+            (info codec (Proxy @AgentInfo))
+instance HasInfo TestCodec (Message (ControlProtocol m c) _st EndState) where
   info codec _ = aliasField
             ("Message<" ++
               "st,EndState" ++
diff --git a/typed-protocols-doc/test/Network/TypedProtocol/Tests/Documentation.hs b/typed-protocols-doc/test/Network/TypedProtocol/Tests/Documentation.hs
index e5b2b505..15b7554a 100644
--- a/typed-protocols-doc/test/Network/TypedProtocol/Tests/Documentation.hs
+++ b/typed-protocols-doc/test/Network/TypedProtocol/Tests/Documentation.hs
@@ -24,10 +24,10 @@ tests = testGroup "Documentation"
           , testProperty "state transitions" (p_correctStateTransitions testProtocolDescription)
           ]
 
-testProtocolDescription :: ProtocolDescription (TestCodec ())
-testProtocolDescription = $(describeProtocol ''ControlProtocol [''IO, ''()] ''TestCodec [''()])
+testProtocolDescription :: ProtocolDescription TestCodec
+testProtocolDescription = $(describeProtocol ''ControlProtocol [''IO, ''()] ''TestCodec [])
 
-p_correctAgencies :: ProtocolDescription (TestCodec ()) -> Property
+p_correctAgencies :: ProtocolDescription TestCodec -> Property
 p_correctAgencies d =
   counterexample (show stateAgencyMap) .
   once $
@@ -45,7 +45,7 @@ p_correctAgencies d =
   where
     stateAgencyMap = [(state, agency) | (state, _, agency) <- protocolStates d]
 
-p_correctStateTransitions :: ProtocolDescription (TestCodec ()) -> Property
+p_correctStateTransitions :: ProtocolDescription TestCodec -> Property
 p_correctStateTransitions d =
   once $
     checkMessage "VersionMessage" (State "InitialState") (State "IdleState")
@@ -83,6 +83,6 @@ p_correctStateTransitions d =
           counterexample "toState"
             (messageToState msg === toState)
 
-    findMessage :: String -> Maybe (MessageDescription (TestCodec ()))
+    findMessage :: String -> Maybe (MessageDescription TestCodec)
     findMessage msgName =
       listToMaybe [ msg | msg <- protocolMessages d, messageName msg == msgName ]
diff --git a/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocol.hs b/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocol.hs
index c090ee39..265899f2 100644
--- a/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocol.hs
+++ b/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocol.hs
@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE EmptyCase #-}
@@ -21,7 +23,6 @@ import Control.Monad.Identity
 import Control.Monad.Except
 import Data.Proxy
 import Data.Word
-import Data.Typeable
 import Data.SerDoc.Class
 import Data.SerDoc.TH
 import Data.Text (Text)
@@ -34,50 +35,47 @@ data PongInfo =
     }
     deriving (Show, Eq)
 
-data TestProtocol a where
+data TestProtocol where
   -- | Idle state: server waits for ping.
-  IdleState :: TestProtocol a
+  IdleState :: TestProtocol
 
   -- | Awaiting pong state: server has received ping, client waits for pong.
-  AwaitingPongState :: TestProtocol a
+  AwaitingPongState :: TestProtocol
 
   -- | End state: either side has terminated the session
-  EndState :: TestProtocol a
-
-instance Protocol (TestProtocol a) where
-  data Message (TestProtocol a) st st' where
-    PingMessage :: Message (TestProtocol a) IdleState AwaitingPongState
-    PongMessage :: Message (TestProtocol a) AwaitingPongState IdleState
-    ComplexPongMessage :: Message (TestProtocol a) AwaitingPongState IdleState
-    EndMessage :: Message (TestProtocol a) st EndState
-
-  data ServerHasAgency st where
-    TokIdle :: ServerHasAgency IdleState
+  EndState :: TestProtocol
 
-  data ClientHasAgency st where
-    TokAwaitingPongState :: ClientHasAgency AwaitingPongState
+instance Protocol TestProtocol where
+  data Message TestProtocol st st' where
+    PingMessage :: Message TestProtocol IdleState AwaitingPongState
+    PongMessage :: Message TestProtocol AwaitingPongState IdleState
+    ComplexPongMessage :: Message TestProtocol AwaitingPongState IdleState
+    EndMessage :: Message TestProtocol st EndState
 
-  data NobodyHasAgency st where
-    TokEnd :: NobodyHasAgency EndState
+  type StateAgency IdleState = ServerAgency
+  type StateAgency AwaitingPongState = ClientAgency
+  type StateAgency EndState = NobodyAgency
 
+  type StateToken = STestProtocol
 
-  exclusionLemma_ClientAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokAwaitingPongState -> case tok2 of {}
+data STestProtocol (st :: TestProtocol) where
+  SingIdle :: STestProtocol IdleState
+  SingAwaitingPong :: STestProtocol AwaitingPongState
+  SingEnd :: STestProtocol EndState
 
-  exclusionLemma_NobodyAndClientHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
+instance StateTokenI IdleState where stateToken = SingIdle
+instance StateTokenI AwaitingPongState where stateToken = SingAwaitingPong
+instance StateTokenI EndState where stateToken = SingEnd
 
-  exclusionLemma_NobodyAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
+data TestCodec
 
-data TestCodec a
+instance Codec TestCodec where
+  type MonadEncode TestCodec = Identity
+  type MonadDecode TestCodec = Except String
 
-instance Codec (TestCodec a) where
-  type MonadEncode (TestCodec a) = Identity
-  type MonadDecode (TestCodec a) = Except String
+instance Serializable TestCodec a where
+  encode _ = pure (pure ())
+  decode _ = throwError "this is a mock codec"
 
 data PongEnum = NormalPong | ComplexPong
   deriving (Show, Read, Eq, Ord, Enum, Bounded)
@@ -91,17 +89,17 @@ deriving via (ViaEnum PongEnum)
 deriving via (ViaEnum PingEnum)
   instance (Codec codec, HasInfo codec (DefEnumEncoding codec)) => HasInfo codec PingEnum
 
-instance HasInfo (TestCodec b) () where
+instance HasInfo TestCodec () where
   info _ _ = basicField "()" (FixedSize 0)
 
-instance HasInfo (TestCodec b) Text where
+instance HasInfo TestCodec Text where
   info codec _ =
     compoundField "Text"
       [ ("length", info codec (Proxy @Word32))
       , ("data", basicField "UTF8 dat" (FixedSize 0))
       ]
 
-instance HasInfo (TestCodec b) a => HasInfo (TestCodec b) [a] where
+instance HasInfo TestCodec a => HasInfo TestCodec [a] where
   info codec (_ :: Proxy [a]) =
     compoundField "List"
       [ ( "length", info codec (Proxy @Word32))
@@ -111,7 +109,7 @@ instance HasInfo (TestCodec b) a => HasInfo (TestCodec b) [a] where
       ]
 
 
-instance HasInfo (TestCodec b) a => HasInfo (TestCodec b) (Maybe a) where
+instance HasInfo TestCodec a => HasInfo TestCodec (Maybe a) where
   info codec (_ :: Proxy (Maybe a)) =
     compoundField "Maybe"
       [ ("isJust", info codec (Proxy @Word32))
@@ -123,24 +121,24 @@ instance HasInfo (TestCodec b) a => HasInfo (TestCodec b) (Maybe a) where
         )
       ]
 
-instance HasInfo (TestCodec b) (Message (TestProtocol a) IdleState AwaitingPongState) where
+instance HasInfo TestCodec (Message TestProtocol IdleState AwaitingPongState) where
   info codec _ = infoOf "PingRequest" $ info codec (Proxy @PingEnum)
 
-instance HasInfo (TestCodec b) (Message (TestProtocol a) st EndState) where
+instance HasInfo TestCodec (Message TestProtocol st EndState) where
   info codec _ = infoOf "EndPing" $ info codec (Proxy @PingEnum)
 
-instance HasInfo (TestCodec a) Word16 where
+instance HasInfo TestCodec Word16 where
   info _ _ = basicField "Word16" (FixedSize 2)
 
-instance HasInfo (TestCodec a) Word32 where
+instance HasInfo TestCodec Word32 where
   info _ _ = basicField "Word32" (FixedSize 4)
 
-instance HasInfo (TestCodec a) Word64 where
+instance HasInfo TestCodec Word64 where
   info _ _ = basicField "Word64" (FixedSize 8)
 
 $(deriveSerDoc ''TestCodec [] ''PongInfo)
 
-instance HasInfo (TestCodec b) (Message (TestProtocol a) AwaitingPongState IdleState) where
+instance HasInfo TestCodec (Message TestProtocol AwaitingPongState IdleState) where
   info codec _ =
     compoundField "Pong"
       [ ("pongType", info codec (Proxy @PongEnum))
diff --git a/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocolTH.hs b/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocolTH.hs
index 9955feba..6f392f33 100644
--- a/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocolTH.hs
+++ b/typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocolTH.hs
@@ -25,8 +25,8 @@ import qualified Data.Text.Lazy as LText
 import Text.Blaze.Html.Renderer.Text (renderHtml)
 import qualified Text.Blaze.Html.Renderer.Pretty as Pretty
 
-testProtocolDescription :: ProtocolDescription (TestCodec ())
-testProtocolDescription = $(describeProtocol ''TestProtocol [''()] ''TestCodec [''()])
+testProtocolDescription :: ProtocolDescription TestCodec
+testProtocolDescription = $(describeProtocol ''TestProtocol [] ''TestCodec [])
 
 testProtocolHtmlString :: String
 testProtocolHtmlString =
diff --git a/typed-protocols-examples/typed-protocols-examples.cabal b/typed-protocols-examples/typed-protocols-examples.cabal
index 81bdee7f..cc6d8ba7 100644
--- a/typed-protocols-examples/typed-protocols-examples.cabal
+++ b/typed-protocols-examples/typed-protocols-examples.cabal
@@ -64,10 +64,12 @@ library
                      time,
                      typed-protocols ^>= 0.4,
                      typed-protocols-cborg,
-                     typed-protocols-stateful
-
+                     typed-protocols-stateful,
   hs-source-dirs:    src
   default-language:  Haskell2010
+  -- ghc-9.2 pulls `ghc-heap-9.12` which is not compatible
+  if impl(ghc < 9.4)
+    build-depends: ghc-heap < 9.12
   ghc-options:       -Wall
                      -Wno-unticked-promoted-constructors
                      -Wcompat