diff --git a/clash-protocols.cabal b/clash-protocols.cabal
index cd2ca014..22f40594 100644
--- a/clash-protocols.cabal
+++ b/clash-protocols.cabal
@@ -211,7 +211,7 @@ test-suite unittests
     Tests.Protocols.DfConv
     Tests.Protocols.Avalon
     Tests.Protocols.Axi4
-    Tests.Protocols.Plugin
+--    Tests.Protocols.Plugin
     Tests.Protocols.Wishbone
 
     Util
diff --git a/src/Protocols.hs b/src/Protocols.hs
index 4a0f8e05..b7f74901 100644
--- a/src/Protocols.hs
+++ b/src/Protocols.hs
@@ -13,9 +13,15 @@ definitions in @circuit-notation@ at <https://github.com/cchalmers/circuit-notat
 module Protocols
   ( -- * Circuit definition
     Circuit(Circuit)
-  , Protocol(Fwd, Bwd)
+  , Fwd
+  , Bwd
   , Backpressure(boolsToBwd)
   , Ack(..)
+  , NC
+  , I2
+  , I3
+  , IVec
+  , type (><)
 
     -- * Combinators & functions
   , (|>), (<|)
diff --git a/src/Protocols/Avalon/MemMap.hs b/src/Protocols/Avalon/MemMap.hs
index c018197d..20d58a28 100644
--- a/src/Protocols/Avalon/MemMap.hs
+++ b/src/Protocols/Avalon/MemMap.hs
@@ -85,8 +85,8 @@ module Protocols.Avalon.MemMap
   , subordinateInRemoveNonDf
 
     -- * Protocols
-  , AvalonMmManager(..)
-  , AvalonMmSubordinate(..)
+  , AvalonMmManager
+  , AvalonMmSubordinate
   ) where
 
 -- base
@@ -1001,25 +1001,17 @@ mmManagerInToBool ::
 mmManagerInToBool = not . mi_waitRequest
 
 -- | Datatype for the manager end of the Avalon memory-mapped protocol.
-data AvalonMmManager (dom :: Domain) (config :: AvalonMmManagerConfig)
-  = AvalonMmManager
+type AvalonMmManager (dom :: Domain) (config :: AvalonMmManagerConfig)
+  =  (Signal dom (AvalonManagerOut config))
+  >< (Signal dom (AvalonManagerIn config))
 
 -- | Datatype for the subordinate end of the Avalon memory-mapped protocol.
-data AvalonMmSubordinate
+type AvalonMmSubordinate
        (dom :: Domain)
        (fixedWaitTime :: Nat)
        (config :: AvalonMmSubordinateConfig)
-       = AvalonMmSubordinate
-
-instance Protocol (AvalonMmManager dom config) where
-  type Fwd (AvalonMmManager dom config) = Signal dom (AvalonManagerOut config)
-  type Bwd (AvalonMmManager dom config) = Signal dom (AvalonManagerIn config)
-
-instance Protocol (AvalonMmSubordinate dom fixedWaitTime config) where
-  type Fwd (AvalonMmSubordinate dom fixedWaitTime config)
-         = Signal dom (AvalonSubordinateIn config)
-  type Bwd (AvalonMmSubordinate dom fixedWaitTime config)
-         = Signal dom (AvalonSubordinateOut config)
+  =  (Signal dom (AvalonSubordinateIn config))
+  >< (Signal dom (AvalonSubordinateOut config))
 
 instance (KnownSubordinateConfig config, KeepWaitRequest config ~ 'True) =>
   Backpressure (AvalonMmSubordinate dom 0 config) where
diff --git a/src/Protocols/Avalon/Stream.hs b/src/Protocols/Avalon/Stream.hs
index bbad91dc..31654874 100644
--- a/src/Protocols/Avalon/Stream.hs
+++ b/src/Protocols/Avalon/Stream.hs
@@ -4,6 +4,7 @@ Types and instance declarations for the Avalon-stream protocol.
 
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -136,22 +137,28 @@ newtype AvalonStreamS2M (readyLatency :: Nat) = AvalonStreamS2M { _ready :: Bool
   deriving (Generic, C.NFDataX, C.ShowX, Eq, NFData, Show, Bundle)
 
 -- | Type for Avalon Stream protocol.
-data AvalonStream (dom :: Domain) (conf :: AvalonStreamConfig) (dataType :: Type)
+type AvalonStream (dom :: Domain) (conf :: AvalonStreamConfig) (dataType :: Type)
+  = AvalonStream# dom conf dataType (ReadyLatency conf)
 
-instance Protocol (AvalonStream dom conf dataType) where
-  type Fwd (AvalonStream dom conf dataType)
-    = Signal dom (Maybe (AvalonStreamM2S conf dataType))
-  type Bwd (AvalonStream dom conf dataType)
-    = Signal dom (AvalonStreamS2M (ReadyLatency conf))
+type AvalonStream#
+  (dom :: Domain)
+  (conf :: AvalonStreamConfig)
+  (dataType :: Type)
+  (n :: Nat)
+  =  (Signal dom (Maybe (AvalonStreamM2S conf dataType)))
+  >< (Signal dom (AvalonStreamS2M n))
 
 instance (ReadyLatency conf ~ 0) =>
-  Backpressure (AvalonStream dom conf dataType) where
+  Backpressure (AvalonStream# dom conf dataType 0) where
   boolsToBwd _ = C.fromList_lazy . fmap AvalonStreamS2M
 
-instance (KnownAvalonStreamConfig conf, NFDataX dataType) =>
-  DfConv.DfConv    (AvalonStream dom conf dataType) where
-  type Dom         (AvalonStream dom conf dataType) = dom
-  type FwdPayload  (AvalonStream dom conf dataType)
+instance
+  ( ReadyLatency conf ~ n
+  , KnownAvalonStreamConfig conf
+  , NFDataX dataType ) =>
+  DfConv.DfConv    (AvalonStream# dom conf dataType n) where
+  type Dom         (AvalonStream# dom conf dataType n) = dom
+  type FwdPayload  (AvalonStream# dom conf dataType n)
     = AvalonStreamM2S conf dataType
 
   toDfCircuit proxy = DfConv.toDfCircuitHelper proxy s0 blankOtp stateFn where
@@ -181,11 +188,11 @@ instance
   , KnownAvalonStreamConfig conf
   , NFDataX dataType
   , KnownDomain dom ) =>
-  Simulate (AvalonStream dom conf dataType) where
-  type SimulateFwdType (AvalonStream dom conf dataType)
+  Simulate (AvalonStream# dom conf dataType 0) where
+  type SimulateFwdType (AvalonStream# dom conf dataType 0)
     = [Maybe (AvalonStreamM2S conf dataType)]
-  type SimulateBwdType (AvalonStream dom conf dataType) = [AvalonStreamS2M 0]
-  type SimulateChannels (AvalonStream dom conf dataType) = 1
+  type SimulateBwdType (AvalonStream# dom conf dataType 0) = [AvalonStreamS2M 0]
+  type SimulateChannels (AvalonStream# dom conf dataType 0) = 1
 
   simToSigFwd _ = fromList_lazy
   simToSigBwd _ = fromList_lazy
@@ -201,8 +208,8 @@ instance
   , KnownAvalonStreamConfig conf
   , NFDataX dataType
   , KnownDomain dom ) =>
-  Drivable (AvalonStream dom conf dataType) where
-  type ExpectType (AvalonStream dom conf dataType)
+  Drivable (AvalonStream# dom conf dataType 0) where
+  type ExpectType (AvalonStream# dom conf dataType 0)
     = [AvalonStreamM2S conf dataType]
 
   toSimulateType Proxy = P.map Just
@@ -225,7 +232,7 @@ instance
   , Show dataType
   , Eq dataType
   , KnownDomain dom ) =>
-  Test (AvalonStream dom conf dataType) where
+  Test (AvalonStream# dom conf dataType 0) where
 
   expectToLengths Proxy = pure . P.length
   expectN Proxy options nExpected sampled
diff --git a/src/Protocols/Axi4/ReadAddress.hs b/src/Protocols/Axi4/ReadAddress.hs
index e17d7d1c..c6232e4b 100644
--- a/src/Protocols/Axi4/ReadAddress.hs
+++ b/src/Protocols/Axi4/ReadAddress.hs
@@ -124,16 +124,12 @@ type family ARKeepQos (conf :: Axi4ReadAddressConfig) where
   ARKeepQos ('Axi4ReadAddressConfig _ _ _ _ _ _ _ _ _ a) = a
 
 -- | AXI4 Read Address channel protocol
-data Axi4ReadAddress
+type Axi4ReadAddress
   (dom :: C.Domain)
   (conf :: Axi4ReadAddressConfig)
   (userType :: Type)
-
-instance Protocol (Axi4ReadAddress dom conf userType) where
-  type Fwd (Axi4ReadAddress dom conf userType) =
-    C.Signal dom (M2S_ReadAddress conf userType)
-  type Bwd (Axi4ReadAddress dom conf userType) =
-    C.Signal dom S2M_ReadAddress
+  =  C.Signal dom (M2S_ReadAddress conf userType)
+  >< C.Signal dom S2M_ReadAddress
 
 instance Backpressure (Axi4ReadAddress dom conf userType) where
   boolsToBwd _ = C.fromList_lazy . coerce
diff --git a/src/Protocols/Axi4/ReadData.hs b/src/Protocols/Axi4/ReadData.hs
index f52cce0a..a3aa92bf 100644
--- a/src/Protocols/Axi4/ReadData.hs
+++ b/src/Protocols/Axi4/ReadData.hs
@@ -55,17 +55,13 @@ type family RIdWidth (conf :: Axi4ReadDataConfig) where
   RIdWidth ('Axi4ReadDataConfig _ a) = a
 
 -- | AXI4 Read Data channel protocol
-data Axi4ReadData
+type Axi4ReadData
   (dom :: C.Domain)
   (conf :: Axi4ReadDataConfig)
   (userType :: Type)
   (dataType :: Type)
-
-instance Protocol (Axi4ReadData dom conf userType dataType) where
-  type Fwd (Axi4ReadData dom conf userType dataType) =
-    C.Signal dom (S2M_ReadData conf userType dataType)
-  type Bwd (Axi4ReadData dom conf userType dataType) =
-    C.Signal dom M2S_ReadData
+  =  C.Signal dom (S2M_ReadData conf userType dataType)
+  >< C.Signal dom M2S_ReadData
 
 instance Backpressure (Axi4ReadData dom conf userType dataType) where
   boolsToBwd _ = C.fromList_lazy . coerce
diff --git a/src/Protocols/Axi4/Stream.hs b/src/Protocols/Axi4/Stream.hs
index e399f53e..290d0a54 100644
--- a/src/Protocols/Axi4/Stream.hs
+++ b/src/Protocols/Axi4/Stream.hs
@@ -101,11 +101,9 @@ newtype Axi4StreamS2M = Axi4StreamS2M { _tready :: Bool }
   deriving (Generic, C.NFDataX, C.ShowX, Eq, NFData, Show, Bundle)
 
 -- | Type for AXI4 Stream protocol.
-data Axi4Stream (dom :: Domain) (conf :: Axi4StreamConfig) (userType :: Type)
-
-instance Protocol (Axi4Stream dom conf userType) where
-  type Fwd (Axi4Stream dom conf userType) = Signal dom (Maybe (Axi4StreamM2S conf userType))
-  type Bwd (Axi4Stream dom conf userType) = Signal dom Axi4StreamS2M
+type Axi4Stream (dom :: Domain) (conf :: Axi4StreamConfig) (userType :: Type)
+  =  Signal dom (Maybe (Axi4StreamM2S conf userType))
+  >< Signal dom Axi4StreamS2M
 
 instance Backpressure (Axi4Stream dom conf userType) where
   boolsToBwd _ = C.fromList_lazy . fmap Axi4StreamS2M
diff --git a/src/Protocols/Axi4/WriteAddress.hs b/src/Protocols/Axi4/WriteAddress.hs
index f6bbf8ac..cd18ebdb 100644
--- a/src/Protocols/Axi4/WriteAddress.hs
+++ b/src/Protocols/Axi4/WriteAddress.hs
@@ -124,16 +124,12 @@ type family AWKeepQos (c :: Axi4WriteAddressConfig) where
   AWKeepQos ('Axi4WriteAddressConfig _ _ _ _ _ _ _ _ _ a) = a
 
 -- | AXI4 Write Address channel protocol
-data Axi4WriteAddress
+type Axi4WriteAddress
   (dom :: C.Domain)
   (conf :: Axi4WriteAddressConfig)
   (userType :: Type)
-
-instance Protocol (Axi4WriteAddress dom conf userType) where
-  type Fwd (Axi4WriteAddress dom conf userType) =
-    C.Signal dom (M2S_WriteAddress conf userType)
-  type Bwd (Axi4WriteAddress dom conf userType) =
-    C.Signal dom S2M_WriteAddress
+  =  C.Signal dom (M2S_WriteAddress conf userType)
+  >< C.Signal dom S2M_WriteAddress
 
 instance Backpressure (Axi4WriteAddress dom conf userType) where
   boolsToBwd _ = C.fromList_lazy . coerce
diff --git a/src/Protocols/Axi4/WriteData.hs b/src/Protocols/Axi4/WriteData.hs
index 4803759b..718a56bd 100644
--- a/src/Protocols/Axi4/WriteData.hs
+++ b/src/Protocols/Axi4/WriteData.hs
@@ -55,16 +55,12 @@ type family WNBytes (conf :: Axi4WriteDataConfig) where
   WNBytes ('Axi4WriteDataConfig _ a) = a
 
 -- | AXI4 Write Data channel protocol
-data Axi4WriteData
+type Axi4WriteData
   (dom :: C.Domain)
   (conf :: Axi4WriteDataConfig)
   (userType :: Type)
-
-instance Protocol (Axi4WriteData dom conf userType) where
-  type Fwd (Axi4WriteData dom conf userType) =
-    C.Signal dom (M2S_WriteData conf userType)
-  type Bwd (Axi4WriteData dom conf userType) =
-    C.Signal dom S2M_WriteData
+  =  C.Signal dom (M2S_WriteData conf userType)
+  >< C.Signal dom S2M_WriteData
 
 instance Backpressure (Axi4WriteData dom conf userType) where
   boolsToBwd _ = C.fromList_lazy . coerce
diff --git a/src/Protocols/Axi4/WriteResponse.hs b/src/Protocols/Axi4/WriteResponse.hs
index d644b788..ccbfaade 100644
--- a/src/Protocols/Axi4/WriteResponse.hs
+++ b/src/Protocols/Axi4/WriteResponse.hs
@@ -53,16 +53,12 @@ type family BIdWidth (conf :: Axi4WriteResponseConfig) where
   BIdWidth ('Axi4WriteResponseConfig _ a) = a
 
 -- | AXI4 Read Data channel protocol
-data Axi4WriteResponse
+type Axi4WriteResponse
   (dom :: C.Domain)
   (conf :: Axi4WriteResponseConfig)
   (userType :: Type)
-
-instance Protocol (Axi4WriteResponse dom conf userType) where
-  type Fwd (Axi4WriteResponse dom conf userType) =
-    C.Signal dom (S2M_WriteResponse conf userType)
-  type Bwd (Axi4WriteResponse dom conf userType) =
-    C.Signal dom M2S_WriteResponse
+  =  C.Signal dom (S2M_WriteResponse conf userType)
+  >< C.Signal dom M2S_WriteResponse
 
 instance Backpressure (Axi4WriteResponse dom conf userType) where
   boolsToBwd _ = C.fromList_lazy . coerce
diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs
index 5b6f222d..c2981704 100644
--- a/src/Protocols/Df.hs
+++ b/src/Protocols/Df.hs
@@ -103,15 +103,11 @@ import           Protocols.Internal
 -- __N.B.__: For performance reasons 'Protocols.Data' is strict on
 -- its data field. That is, if 'Protocols.Data' is evaluated to WHNF,
 -- its fields will be evaluated to WHNF too.
-data Df (dom :: C.Domain) (a :: Type)
-
-instance Protocol (Df dom a) where
-  -- | Forward part of simple dataflow: @Signal dom (Data meta a)@
-  type Fwd (Df dom a) = Signal dom (Data a)
-
-  -- | Backward part of simple dataflow: @Signal dom Bool@
-  type Bwd (Df dom a) = Signal dom Ack
-
+type Df (dom :: C.Domain) (a :: Type)
+  =  Signal dom (Data a)
+     -- ^ Forward part of simple dataflow: @Signal dom (Data meta a)@
+  >< Signal dom Ack
+     -- ^ Backward part of simple dataflow: @Signal dom Bool@
 
 instance Backpressure (Df dom a) where
   boolsToBwd _ = C.fromList_lazy . coerce
@@ -229,11 +225,11 @@ const b = Circuit (P.const (Ack <$>
                   )
 
 -- | Drive a constant value composed of /a/.
-pure :: a -> Circuit () (Df dom a)
+pure :: a -> Circuit NC (Df dom a)
 pure a = Circuit (P.const ((), P.pure (Data a)))
 
 -- | Drive a constant value composed of /a/.
-void :: C.HiddenReset dom => Circuit (Df dom a) ()
+void :: C.HiddenReset dom => Circuit (Df dom a) NC
 void = Circuit (P.const (Ack <$>
 #if MIN_VERSION_clash_prelude(1,8,0)
                            C.unsafeToActiveLow C.hasReset
@@ -300,7 +296,7 @@ zipWith ::
   forall dom a b c.
   (a -> b -> c) ->
   Circuit
-    (Df dom a, Df dom b)
+    (I2 (Df dom a) (Df dom b))
     (Df dom c)
 zipWith f
   = Circuit (B.first C.unbundle . C.unbundle . fmap go . C.bundle . B.first C.bundle)
@@ -309,7 +305,7 @@ zipWith f
   go _ = ((Ack False, Ack False), NoData)
 
 -- | Like 'P.zip', but over two 'Df' streams.
-zip :: forall a b dom. Circuit (Df dom a, Df dom b) (Df dom (a, b))
+zip :: forall a b dom. Circuit (I2 (Df dom a) (Df dom b)) (Df dom (a, b))
 zip = zipWith (,)
 
 -- | Like 'P.partition', but over 'Df' streams
@@ -321,7 +317,7 @@ zip = zipWith (,)
 -- >>> B.bimap (take 3) (take 4) output
 -- ([7,9,11],[1,3,5,2])
 --
-partition :: forall dom a. (a -> Bool) -> Circuit (Df dom a) (Df dom a, Df dom a)
+partition :: forall dom a. (a -> Bool) -> Circuit (Df dom a) (I2 (Df dom a) (Df dom a))
 partition f
   = Circuit (B.second C.unbundle . C.unbundle . fmap go . C.bundle . B.second C.bundle)
  where
@@ -348,7 +344,7 @@ partition f
 --
 route ::
   forall n dom a. C.KnownNat n =>
-  Circuit (Df dom (C.Index n, a)) (C.Vec n (Df dom a))
+  Circuit (Df dom (C.Index n, a)) (IVec n (Df dom a))
 route
   = Circuit (B.second C.unbundle . C.unbundle . fmap go . C.bundle . B.second C.bundle)
  where
@@ -373,7 +369,7 @@ route
 select ::
   forall n dom a.
   C.KnownNat n =>
-  Circuit (C.Vec n (Df dom a), Df dom (C.Index n)) (Df dom a)
+  Circuit (I2 (IVec n (Df dom a)) (Df dom (C.Index n))) (Df dom a)
 select = selectUntil (P.const True)
 
 -- | Select /selectN/ samples from channel /n/.
@@ -393,7 +389,7 @@ selectN ::
   , C.KnownNat n
   ) =>
   Circuit
-    (C.Vec n (Df dom a), Df dom (C.Index n, C.Index selectN))
+    (I2 (IVec n (Df dom a)) (Df dom (C.Index n, C.Index selectN)))
     (Df dom a)
 selectN
   = Circuit
@@ -445,7 +441,7 @@ selectUntil ::
   C.KnownNat n =>
   (a -> Bool) ->
   Circuit
-    (C.Vec n (Df dom a), Df dom (C.Index n))
+    (I2 (IVec n (Df dom a)) (Df dom (C.Index n)))
     (Df dom a)
 selectUntil f
   = Circuit
@@ -471,7 +467,7 @@ selectUntil f
 fanout ::
   forall n dom a .
   (C.KnownNat n, C.HiddenClockResetEnable dom, 1 <= n) =>
-  Circuit (Df dom a) (C.Vec n (Df dom a))
+  Circuit (Df dom a) (IVec n (Df dom a))
 fanout = forceResetSanity |> goC
  where
   goC =
@@ -502,21 +498,21 @@ fanin ::
   forall n dom a .
   (C.KnownNat n, 1 <= n) =>
   (a -> a -> a) ->
-  Circuit (C.Vec n (Df dom a)) (Df dom a)
+  Circuit (IVec n (Df dom a)) (Df dom a)
 fanin f = bundleVec |> map (C.fold @(n C.- 1) f)
 
 -- | Merge data of multiple 'Df' streams using Monoid's '<>'.
 mfanin ::
   forall n dom a .
   (C.KnownNat n, Monoid a, 1 <= n) =>
-  Circuit (C.Vec n (Df dom a)) (Df dom a)
+  Circuit (IVec n (Df dom a)) (Df dom a)
 mfanin = fanin (<>)
 
 -- | Bundle a vector of 'Df' streams into one.
 bundleVec ::
   forall n dom a .
   (C.KnownNat n, 1 <= n) =>
-  Circuit (C.Vec n (Df dom a)) (Df dom (C.Vec n a))
+  Circuit (IVec n (Df dom a)) (Df dom (C.Vec n a))
 bundleVec
   = Circuit (B.first C.unbundle . C.unbundle . fmap go . C.bundle . B.first C.bundle)
  where
@@ -529,7 +525,7 @@ bundleVec
 unbundleVec ::
   forall n dom a .
   (C.KnownNat n, C.NFDataX a, C.HiddenClockResetEnable dom, 1 <= n) =>
-  Circuit (Df dom (C.Vec n a)) (C.Vec n (Df dom a))
+  Circuit (Df dom (C.Vec n a)) (IVec n (Df dom a))
 unbundleVec
   = Circuit (B.second C.unbundle . C.mealyB go initState . B.second C.bundle)
  where
@@ -557,7 +553,7 @@ unbundleVec
 roundrobin ::
   forall n dom a .
   (C.KnownNat n, C.HiddenClockResetEnable dom, 1 <= n) =>
-  Circuit (Df dom a) (C.Vec n (Df dom a))
+  Circuit (Df dom a) (IVec n (Df dom a))
 roundrobin
   = Circuit
   ( B.second C.unbundle
@@ -592,7 +588,7 @@ roundrobinCollect ::
   forall n dom a .
   (C.KnownNat n, C.HiddenClockResetEnable dom, 1 <= n) =>
   CollectMode ->
-  Circuit (C.Vec n (Df dom a)) (Df dom a)
+  Circuit (IVec n (Df dom a)) (Df dom a)
 roundrobinCollect NoSkip
   = Circuit (B.first C.unbundle . C.mealyB go minBound . B.first C.bundle)
  where
@@ -737,7 +733,7 @@ drive ::
   ( C.KnownDomain dom ) =>
   SimulationConfig ->
   [Maybe a] ->
-  Circuit () (Df dom a)
+  Circuit NC (Df dom a)
 drive SimulationConfig{resetCycles} s0 = Circuit $
     ((),)
   . C.fromList_lazy
@@ -762,7 +758,7 @@ sample ::
   forall dom b.
   ( C.KnownDomain dom ) =>
   SimulationConfig ->
-  Circuit () (Df dom b) ->
+  Circuit NC (Df dom b) ->
   [Maybe b]
 sample SimulationConfig{..} c =
     fmap dataToMaybe
diff --git a/src/Protocols/DfConv.hs b/src/Protocols/DfConv.hs
index 666360fa..bca354cd 100644
--- a/src/Protocols/DfConv.hs
+++ b/src/Protocols/DfConv.hs
@@ -82,6 +82,7 @@ import qualified Clash.Prelude as C
 import qualified Data.Bifunctor as B
 import           Data.Maybe (isJust)
 import           Data.Proxy (Proxy(..))
+import           Data.Type.Equality
 import           Data.Tuple (swap)
 import           GHC.Stack (HasCallStack)
 
@@ -106,7 +107,7 @@ import           Protocols.Internal
 -- using 'Df'. For pipelined protocols, which can carry both in the same cycle,
 -- the 'Circuit' should pass along the interesting parts but not the
 -- uninteresting parts.
-class (Protocol df) => DfConv df where
+class DfConv (df :: CircuitInterface) where
   -- | Domain that messages are being sent over. In general, it should be true that
   -- @Fwd df ~ Signal dom [something]@ and that @Bwd df ~ Signal dom [something]@.
   type Dom df :: Domain
@@ -135,7 +136,7 @@ class (Protocol df) => DfConv df where
   toDfCircuit :: (HiddenClockResetEnable (Dom df)) =>
     Proxy df ->
     Circuit
-      (Df (Dom df) (FwdPayload df), Reverse (Df (Dom df) (BwdPayload df)))
+      (I2 (Df (Dom df) (FwdPayload df)) (Reverse (Df (Dom df) (BwdPayload df))))
       df
 
   -- | 'toDfCircuit', but in reverse: the @df@ port is on the left side instead
@@ -144,7 +145,7 @@ class (Protocol df) => DfConv df where
     Proxy df ->
     Circuit
       df
-      (Df (Dom df) (FwdPayload df), Reverse (Df (Dom df) (BwdPayload df)))
+      (I2 (Df (Dom df) (FwdPayload df)) (Reverse (Df (Dom df) (BwdPayload df))))
 
   -- defaults
   type BwdPayload df = ()
@@ -157,13 +158,10 @@ class (Protocol df) => DfConv df where
 -- @otpMsg@, and 'State' machine function
 toDfCircuitHelper ::
   ( HiddenClockResetEnable dom
-  , Protocol df
-  , Bwd df ~ Unbundled dom inpMsg
-  , Fwd df ~ Unbundled dom otpMsg
   , NFDataX state
   , Bundle inpMsg
   , Bundle otpMsg ) =>
-  Proxy df ->
+  Proxy (Unbundled dom otpMsg >< Unbundled dom inpMsg) ->
   state ->
   otpMsg ->
   ( inpMsg ->
@@ -171,9 +169,9 @@ toDfCircuitHelper ::
     Maybe fwdPayload ->
     State state (otpMsg, Maybe bwdPayload, Bool)
     ) ->
-  Circuit ( Df dom fwdPayload
-          , Reverse (Df dom bwdPayload))
-          df
+  Circuit
+    (I2 (Df dom fwdPayload) (Reverse (Df dom bwdPayload)))
+    (Unbundled dom otpMsg >< Unbundled dom inpMsg)
 toDfCircuitHelper _ s0 blankOtp stateFn
   = Circuit
   $ (unbundle *** unbundle)
@@ -205,13 +203,10 @@ toDfCircuitHelper _ s0 blankOtp stateFn
 -- @otpMsg@, and 'State' machine function
 fromDfCircuitHelper ::
   ( HiddenClockResetEnable dom
-  , Protocol df
-  , Fwd df ~ Unbundled dom inpMsg
-  , Bwd df ~ Unbundled dom otpMsg
   , NFDataX state
   , Bundle inpMsg
   , Bundle otpMsg ) =>
-  Proxy df ->
+  Proxy (Unbundled dom inpMsg >< Unbundled dom otpMsg) ->
   state ->
   otpMsg ->
   ( inpMsg ->
@@ -219,7 +214,9 @@ fromDfCircuitHelper ::
     Maybe bwdPayload ->
     State state (otpMsg, Maybe fwdPayload, Bool)
     ) ->
-  Circuit df (Df dom fwdPayload, Reverse (Df dom bwdPayload))
+  Circuit
+    (Unbundled dom inpMsg >< Unbundled dom otpMsg)
+    (I2 (Df dom fwdPayload) (Reverse (Df dom bwdPayload)))
 fromDfCircuitHelper df s0 blankOtp stateFn
   = mapCircuit id id swap swap
   $ reverseCircuit
@@ -231,22 +228,22 @@ fromDfCircuitHelper df s0 blankOtp stateFn
 
 -- Trivial DfConv instance for (Df, Reverse Df)
 
-instance DfConv (Df dom a, Reverse (Df dom b)) where
-  type Dom        (Df dom a, Reverse (Df dom b)) = dom
-  type BwdPayload (Df dom a, Reverse (Df dom b)) = b
-  type FwdPayload (Df dom a, Reverse (Df dom b)) = a
-  toDfCircuit _ = idC
-  fromDfCircuit _ = idC
+type DfReverseDf dom a b =
+     (Signal dom (Data a), Signal dom Ack)
+  >< (Signal dom Ack, Signal dom (Data b))
 
+_verifyDfReverseDf ::
+      DfReverseDf dom a b
+  :~: I2 (Df dom a) (Reverse (Df dom b))
+_verifyDfReverseDf = Refl
 
--- DfConv instance for Reverse
-
-instance (DfConv a) => DfConv (Reverse a) where
-  type Dom        (Reverse a) = Dom a
-  type BwdPayload (Reverse a) = FwdPayload a
-  type FwdPayload (Reverse a) = BwdPayload a
-  toDfCircuit _ = mapCircuit swap swap id id $ reverseCircuit $ fromDfCircuit (Proxy @a)
-  fromDfCircuit _ = mapCircuit id id swap swap $ reverseCircuit $ toDfCircuit (Proxy @a)
+instance DfConv (DfReverseDf dom a b)
+ where
+  type Dom        (DfReverseDf dom _ _) = dom
+  type BwdPayload (DfReverseDf _   _ b) = b
+  type FwdPayload (DfReverseDf _   a _) = a
+  toDfCircuit _ = idC
+  fromDfCircuit _ = idC
 
 
 -- DfConv instances for Df
@@ -259,9 +256,37 @@ instance (NFDataX dat) => DfConv (Df dom dat) where
   fromDfCircuit _ = Circuit (uncurry f) where
     f a ~(b, _) = (b, (a, P.pure (Ack False)))
 
+instance (NFDataX dat) => DfConv (Signal dom Ack >< Signal dom (Data dat)) where
+  type Dom        (Signal dom Ack >< Signal dom (Data _)) = dom
+  type BwdPayload (Signal dom Ack >< Signal dom (Data dat)) = dat
+  toDfCircuit _ =
+      mapCircuit swap swap id id
+    $ reverseCircuit
+    $ fromDfCircuit (Proxy @(Df dom dat))
+  fromDfCircuit _ =
+      mapCircuit id id swap swap
+    $ reverseCircuit
+    $ toDfCircuit (Proxy @(Df dom dat))
 
 -- DfConv instances for Axi4
 
+type Axi4Write dom confAW userAW confW userW confB userB =
+  ( C.Signal dom (M2S_WriteAddress confAW userAW)
+  , C.Signal dom (M2S_WriteData confW userW)
+  , C.Signal dom M2S_WriteResponse
+  ) ><
+  ( C.Signal dom S2M_WriteAddress
+  , C.Signal dom S2M_WriteData
+  , C.Signal dom (S2M_WriteResponse confB userB)
+  )
+
+_verifyAxi4Write ::
+      Axi4Write dom confAW userAW confW userW confB userB
+  :~: I3 (Axi4WriteAddress dom confAW userAW)
+         (Axi4WriteData dom confW userW)
+         (Reverse (Axi4WriteResponse dom confB userB))
+_verifyAxi4Write = Refl
+
 -- Manager end (toDfCircuit) only allows for burst length of 1, will ignore the
 -- burst length you input. Subordinate end (fromDfCircuit) allows for any burst
 -- length.
@@ -272,32 +297,18 @@ instance
   , NFDataX userAW
   , NFDataX userB
   , AWIdWidth confAW ~ BIdWidth confB ) =>
-  DfConv
-    (Axi4WriteAddress dom confAW userAW,
-     Axi4WriteData dom confW userW,
-     Reverse (Axi4WriteResponse dom confB userB))
-    where
-
-  type Dom
-    (Axi4WriteAddress dom confAW userAW,
-     Axi4WriteData dom confW userW,
-     Reverse (Axi4WriteResponse dom confB userB))
-    = dom
+  DfConv (Axi4Write dom confAW userAW confW userW confB userB)
+   where
+  type Dom (Axi4Write dom _ _ _ _ _ _) = dom
 
-  type FwdPayload
-    (Axi4WriteAddress dom confAW userAW,
-     Axi4WriteData dom confW userW,
-     Reverse (Axi4WriteResponse dom confB userB))
+  type FwdPayload (Axi4Write _ confAW userAW confW userW _ _)
     = ( Axi4WriteAddressInfo confAW userAW
       , BurstLengthType (AWKeepBurstLength confAW)
       , BurstType (AWKeepBurst confAW)
       , StrictStrobeType (WNBytes confW) (WKeepStrobe confW)
       , userW)
 
-  type BwdPayload
-    (Axi4WriteAddress dom confAW userAW,
-     Axi4WriteData dom confW userW,
-     Reverse (Axi4WriteResponse dom confB userB))
+  type BwdPayload (Axi4Write _ _ _ _ _ confB userB)
     = (ResponseType (BKeepResponse confB), userB)
 
   -- MANAGER PORT
@@ -402,30 +413,35 @@ instance
       when dfAckOut $ put (a, Nothing)
       P.pure (respVal, dfAckOut)
 
+type Axi4Read dom confAR dataAR confR userR dat =
+  ( C.Signal dom (M2S_ReadAddress confAR dataAR)
+  , C.Signal dom M2S_ReadData
+  ) ><
+  ( C.Signal dom S2M_ReadAddress
+  , C.Signal dom (S2M_ReadData confR userR dat)
+  )
+
+_verifyAxi4Read ::
+      Axi4Read dom confAR dataAR confR userR dat
+  :~: I2 (Axi4ReadAddress dom confAR dataAR)
+         (Reverse (Axi4ReadData dom confR userR dat))
+_verifyAxi4Read = Refl
+
 instance
   ( KnownAxi4ReadAddressConfig confAR
   , KnownAxi4ReadDataConfig confR
   , NFDataX userR
   , NFDataX dat
   , ARIdWidth confAR ~ RIdWidth confR ) =>
-  DfConv
-    (Axi4ReadAddress dom confAR dataAR,
-     Reverse (Axi4ReadData dom confR userR dat))
+  DfConv (Axi4Read dom confAR dataAR confR userR dat)
     where
 
-  type Dom
-    (Axi4ReadAddress dom confAR dataAR,
-     Reverse (Axi4ReadData dom confR userR dat))
-     = dom
+  type Dom (Axi4Read dom _ _ _ _ _) = dom
 
-  type BwdPayload
-    (Axi4ReadAddress dom confAR dataAR,
-     Reverse (Axi4ReadData dom confR userR dat))
+  type BwdPayload (Axi4Read _ _ _ confR userR dat)
      = (dat, userR, ResponseType (RKeepResponse confR))
 
-  type FwdPayload
-    (Axi4ReadAddress dom confAR dataAR,
-     Reverse (Axi4ReadData dom confR userR dat))
+  type FwdPayload (Axi4Read _ confAR dataAR _ _ _)
      = Axi4ReadAddressInfo confAR dataAR
 
   -- MANAGER PORT
@@ -519,9 +535,9 @@ vecToDfConv ::
   HiddenClockResetEnable (Dom df) =>
   KnownNat n =>
   Proxy df ->
-  Circuit ( Vec n (Df (Dom df) (FwdPayload df))
-          , Vec n (Reverse (Df (Dom df) (BwdPayload df))))
-          (Vec n df)
+  Circuit (I2 (IVec n (Df (Dom df) (FwdPayload df)))
+              (IVec n (Reverse (Df (Dom df) (BwdPayload df)))))
+          (IVec n df)
 vecToDfConv proxy = mapCircuit (uncurry C.zip) unzip id id $ vecCircuits
                   $ repeat $ toDfCircuit proxy
 
@@ -531,9 +547,9 @@ vecFromDfConv ::
   HiddenClockResetEnable (Dom df) =>
   KnownNat n =>
   Proxy df ->
-  Circuit ( Vec n df )
-          ( Vec n (Df (Dom df) (FwdPayload df))
-          , Vec n (Reverse (Df (Dom df) (BwdPayload df))))
+  Circuit (IVec n df)
+          (I2 (IVec n (Df (Dom df) (FwdPayload df)))
+              (IVec n (Reverse (Df (Dom df) (BwdPayload df)))))
 vecFromDfConv proxy = mapCircuit id id unzip (uncurry C.zip) $ vecCircuits
                     $ repeat $ fromDfCircuit proxy
 
@@ -545,12 +561,14 @@ tupToDfConv ::
   , HiddenClockResetEnable (Dom dfA) ) =>
   (Proxy dfA, Proxy dfB) ->
   Circuit
-    ( ( Df (Dom dfA) (FwdPayload dfA)
-      , Df (Dom dfB) (FwdPayload dfB) )
-    , ( Reverse (Df (Dom dfA) (BwdPayload dfA))
-      , Reverse (Df (Dom dfB) (BwdPayload dfB)) )
+    (I2 (I2 (Df (Dom dfA) (FwdPayload dfA))
+            (Df (Dom dfB) (FwdPayload dfB))
+        )
+        (I2 (Reverse (Df (Dom dfA) (BwdPayload dfA)))
+            (Reverse (Df (Dom dfB) (BwdPayload dfB)))
+        )
     )
-    (dfA, dfB)
+    (I2 dfA dfB)
 tupToDfConv (argsA, argsB)
   = mapCircuit f f id id
   $ tupCircuits (toDfCircuit argsA) (toDfCircuit argsB)
@@ -565,11 +583,13 @@ tupFromDfConv ::
   , HiddenClockResetEnable (Dom dfA) ) =>
   (Proxy dfA, Proxy dfB) ->
   Circuit
-    (dfA, dfB)
-    ( ( Df (Dom dfA) (FwdPayload dfA)
-      , Df (Dom dfB) (FwdPayload dfB) )
-    , ( Reverse (Df (Dom dfA) (BwdPayload dfA))
-      , Reverse (Df (Dom dfB) (BwdPayload dfB)) )
+    (I2 dfA dfB)
+    (I2 (I2 (Df (Dom dfA) (FwdPayload dfA))
+            (Df (Dom dfB) (FwdPayload dfB))
+        )
+        (I2 (Reverse (Df (Dom dfA) (BwdPayload dfA)))
+            (Reverse (Df (Dom dfB) (BwdPayload dfB)))
+        )
     )
 tupFromDfConv (argsA, argsB)
   = mapCircuit id id f f
@@ -578,7 +598,7 @@ tupFromDfConv (argsA, argsB)
   f ((a,b),(c,d)) = ((a,c),(b,d))
 
 -- | Circuit converting a pair of items into a @Vec 2@
-tupToVec :: Circuit (a,a) (Vec 2 a)
+tupToVec :: Circuit (I2 (fwd >< bwd) (fwd >< bwd)) (IVec 2 (fwd >< bwd))
 tupToVec = Circuit ((f *** g) . swap) where
   f :: Vec 2 p -> (p,p)
   f (x :> y :> Nil) = (x,y)
@@ -586,7 +606,7 @@ tupToVec = Circuit ((f *** g) . swap) where
   g (x,y) = x :> y :> Nil
 
 -- | Circuit converting a @Vec 2@ into a pair of items
-vecToTup :: Circuit (Vec 2 a) (a,a)
+vecToTup :: Circuit (IVec 2 (fwd >< bwd)) (I2 (fwd >< bwd) (fwd >< bwd))
 vecToTup = Circuit ((g *** f) . swap) where
   f :: Vec 2 p -> (p,p)
   f (x :> y :> Nil) = (x,y)
@@ -609,8 +629,13 @@ convert dfA dfB
   =  fromDfCircuit dfA
   |> toDfCircuit dfB
 
+-- | Specialized version of 'idC' for internal use only.
+idC' :: Circuit (Reverse (Df dom a)) (Reverse (Df dom a))
+idC' = idC
+
 -- | Like 'P.map'
 map ::
+  forall dfA dfB.
   ( DfConv dfA
   , DfConv dfB
   , BwdPayload dfA ~ BwdPayload dfB
@@ -622,7 +647,7 @@ map ::
   Circuit dfA dfB
 map dfA dfB f
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.map f) idC
+  |> tupCircuits (Df.map f) idC'
   |> toDfCircuit dfB
 
 -- | Like 'P.fst'
@@ -639,7 +664,7 @@ fst ::
   Circuit dfA dfB
 fst dfA dfB
   =  fromDfCircuit dfA
-  |> tupCircuits Df.fst idC
+  |> tupCircuits Df.fst idC'
   |> toDfCircuit dfB
 
 -- | Like 'P.fst'
@@ -656,7 +681,7 @@ snd ::
   Circuit dfA dfB
 snd dfA dfB
   =  fromDfCircuit dfA
-  |> tupCircuits Df.snd idC
+  |> tupCircuits Df.snd idC'
   |> toDfCircuit dfB
 
 -- | Like 'Data.Bifunctor.bimap'
@@ -676,7 +701,7 @@ bimap ::
   Circuit dfA dfB
 bimap dfA dfB f g
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.bimap f g) idC
+  |> tupCircuits (Df.bimap f g) idC'
   |> toDfCircuit dfB
 
 -- | Like 'Data.Bifunctor.first'
@@ -695,7 +720,7 @@ first ::
   Circuit dfA dfB
 first dfA dfB f
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.first f) idC
+  |> tupCircuits (Df.first f) idC'
   |> toDfCircuit dfB
 
 -- | Like 'Data.Bifunctor.second'
@@ -714,7 +739,7 @@ second ::
   Circuit dfA dfB
 second dfA dfB f
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.second f) idC
+  |> tupCircuits (Df.second f) idC'
   |> toDfCircuit dfB
 
 -- | Acknowledge but ignore data from LHS protocol. Send a static value /b/.
@@ -730,7 +755,7 @@ const ::
   Circuit dfA dfB
 const dfA dfB b
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.const b) idC
+  |> tupCircuits (Df.const b) idC'
   |> toDfCircuit dfB
 
 -- | Drive a constant value composed of /a/.
@@ -739,7 +764,7 @@ pure ::
   , HiddenClockResetEnable (Dom df) ) =>
   Proxy df ->
   FwdPayload df ->
-  Circuit () df
+  Circuit NC df
 pure df a
   =  Df.pure a
   |> dfToDfConvOtp df
@@ -749,7 +774,7 @@ void ::
   ( DfConv df
   , HiddenClockResetEnable (Dom df) ) =>
   Proxy df ->
-  Circuit df ()
+  Circuit df NC
 void df = dfToDfConvInp df
   |> Df.void
 
@@ -766,7 +791,7 @@ catMaybes ::
   Circuit dfA dfB
 catMaybes dfA dfB
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.catMaybes) idC
+  |> tupCircuits (Df.catMaybes) idC'
   |> toDfCircuit dfB
 
 -- | Like 'Data.Maybe.mapMaybe'
@@ -783,7 +808,7 @@ mapMaybe ::
   Circuit dfA dfB
 mapMaybe dfA dfB f
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.mapMaybe f) idC
+  |> tupCircuits (Df.mapMaybe f) idC'
   |> toDfCircuit dfB
 
 -- | Like 'P.filter'
@@ -800,7 +825,7 @@ filter ::
   Circuit dfA dfB
 filter dfA dfB f
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.filter f) idC
+  |> tupCircuits (Df.filter f) idC'
   |> toDfCircuit dfB
 
 -- | Like 'Data.Either.Combinators.mapLeft'
@@ -818,7 +843,7 @@ mapLeft ::
   Circuit dfA dfB
 mapLeft dfA dfB f
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.mapLeft f) idC
+  |> tupCircuits (Df.mapLeft f) idC'
   |> toDfCircuit dfB
 
 -- | Like 'Data.Either.Combinators.mapRight'
@@ -836,7 +861,7 @@ mapRight ::
   Circuit dfA dfB
 mapRight dfA dfB f
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.mapRight f) idC
+  |> tupCircuits (Df.mapRight f) idC'
   |> toDfCircuit dfB
 
 -- | Like 'Data.Either.either'
@@ -854,7 +879,7 @@ either ::
   Circuit dfA dfB
 either dfA dfB f g
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.either f g) idC
+  |> tupCircuits (Df.either f g) idC'
   |> toDfCircuit dfB
 
 -- | Like 'P.zipWith'. Any data not in /Payload/ is copied from stream A.
@@ -870,7 +895,7 @@ zipWith ::
   (Proxy dfA, Proxy dfB) ->
   Proxy dfC ->
   (FwdPayload dfA -> FwdPayload dfB -> FwdPayload dfC) ->
-  Circuit (dfA, dfB) dfC
+  Circuit (I2 dfA dfB) dfC
 zipWith dfAB dfC f
   =  tupFromDfConv dfAB
   |> coerceCircuit
@@ -892,7 +917,7 @@ zip ::
   , FwdPayload dfC ~ (FwdPayload dfA, FwdPayload dfB) ) =>
   (Proxy dfA, Proxy dfB) ->
   Proxy dfC ->
-  Circuit (dfA, dfB) dfC
+  Circuit (I2 dfA dfB) dfC
 zip dfAB dfC
   =  tupFromDfConv dfAB
   |> coerceCircuit
@@ -916,7 +941,7 @@ partition ::
   Proxy dfA ->
   (Proxy dfB, Proxy dfC) ->
   (FwdPayload dfA -> Bool) ->
-  Circuit dfA (dfB, dfC)
+  Circuit dfA (I2 dfB dfC)
 partition dfA dfBC f
   =  fromDfCircuit dfA
   |> coerceCircuit
@@ -937,7 +962,7 @@ route ::
   , 1 <= n ) =>
   Proxy dfA ->
   Proxy dfB ->
-  Circuit dfA (Vec n dfB)
+  Circuit dfA (IVec n dfB)
 route dfA dfB
   =  fromDfCircuit dfA
   |> coerceCircuit
@@ -946,11 +971,17 @@ route dfA dfB
      (reverseCircuit (Df.roundrobinCollect Df.Parallel)))
   |> vecToDfConv dfB
 
-selectHelperA :: Circuit ((a,b),(c,d)) ((a,c),(b,d))
+selectHelperA ::
+  Circuit
+    (I2 ((fa, fb) >< (ba, bb)) ((fc, fd) >< (bc, bd)))
+    (I2 ((fa, fc) >< (ba, bc)) ((fb, fd) >< (bb, bd)))
 selectHelperA = Circuit ((f *** f) . swap) where
   f ((a,b),(c,d)) = ((a,c),(b,d))
 
-selectHelperB :: Circuit (Vec (n+1) a) (Vec n a, a)
+selectHelperB ::
+  Circuit
+    (Vec (n+1) fwd >< Vec (n+1) bwd)
+    (I2 (Vec n fwd >< Vec n bwd) (fwd >< bwd))
 selectHelperB = Circuit ((f *** g) . swap) where
   f :: (Vec n q, q) -> Vec (n+1) q
   f (t, h) = h :> t
@@ -974,7 +1005,7 @@ select ::
   , KnownNat n ) =>
   (Proxy dfA, Proxy dfB) ->
   Proxy dfC ->
-  Circuit (Vec n dfA, dfB) dfC
+  Circuit (I2 (IVec n dfA) dfB) dfC
 select (dfA, dfB) dfC
   =  tupCircuits (vecFromDfConv dfA) (fromDfCircuit dfB)
   |> selectHelperA
@@ -1000,7 +1031,7 @@ selectN ::
   , KnownNat selectN ) =>
   (Proxy dfA, Proxy dfB) ->
   Proxy dfC ->
-  Circuit (Vec n dfA, dfB) dfC
+  Circuit (I2 (IVec n dfA) dfB) dfC
 selectN (dfA, dfB) dfC
   =  tupCircuits (vecFromDfConv dfA) (fromDfCircuit dfB)
   |> selectHelperA
@@ -1027,7 +1058,7 @@ selectUntil ::
   (Proxy dfA, Proxy dfB) ->
   Proxy dfC ->
   (FwdPayload dfA -> Bool) ->
-  Circuit (Vec n dfA, dfB) dfC
+  Circuit (I2 (IVec n dfA) dfB) dfC
 selectUntil (dfA, dfB) dfC f
   =  tupCircuits (vecFromDfConv dfA) (fromDfCircuit dfB)
   |> selectHelperA
@@ -1051,7 +1082,7 @@ fanout ::
   , numB ~ (decNumB + 1) ) =>
   Proxy dfA ->
   Proxy dfB ->
-  Circuit dfA (Vec numB dfB)
+  Circuit dfA (IVec numB dfB)
 fanout dfA dfB
   =  fromDfCircuit dfA
   |> coerceCircuit
@@ -1074,7 +1105,7 @@ fanin ::
   Proxy dfA ->
   Proxy dfB ->
   (FwdPayload dfA -> FwdPayload dfA -> FwdPayload dfA) ->
-  Circuit (Vec numA dfA) dfB
+  Circuit (IVec numA dfA) dfB
 fanin dfA dfB f
   =  vecFromDfConv dfA
   |> coerceCircuit
@@ -1097,7 +1128,7 @@ mfanin ::
   , numA ~ (decNumA + 1) ) =>
   Proxy dfA ->
   Proxy dfB ->
-  Circuit (Vec numA dfA) dfB
+  Circuit (IVec numA dfA) dfB
 mfanin dfA dfB
   =  vecFromDfConv dfA
   |> coerceCircuit
@@ -1118,7 +1149,7 @@ bundleVec ::
   , n ~ (decN + 1) ) =>
   Proxy dfA ->
   Proxy dfB ->
-  Circuit (Vec n dfA) dfB
+  Circuit (IVec n dfA) dfB
 bundleVec dfA dfB
   =  vecFromDfConv dfA
   |> coerceCircuit
@@ -1141,7 +1172,7 @@ unbundleVec ::
   , 1 <= n ) =>
   Proxy dfA ->
   Proxy dfB ->
-  Circuit dfA (Vec n dfB)
+  Circuit dfA (IVec n dfB)
 unbundleVec dfA dfB
   =  fromDfCircuit dfA
   |> coerceCircuit
@@ -1164,7 +1195,7 @@ roundrobin ::
   , n ~ (decN + 1) ) =>
   Proxy dfA ->
   Proxy dfB ->
-  Circuit dfA (Vec n dfB)
+  Circuit dfA (IVec n dfB)
 roundrobin dfA dfB
   =  fromDfCircuit dfA
   |> coerceCircuit
@@ -1187,7 +1218,7 @@ roundrobinCollect ::
   Proxy dfA ->
   Proxy dfB ->
   Df.CollectMode ->
-  Circuit (Vec n dfA) dfB
+  Circuit (IVec n dfA) dfB
 roundrobinCollect dfA dfB mode
   =  vecFromDfConv dfA
   |> coerceCircuit
@@ -1210,7 +1241,7 @@ registerFwd ::
   Circuit dfA dfB
 registerFwd dfA dfB
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.registerFwd) idC
+  |> tupCircuits (Df.registerFwd) idC'
   |> toDfCircuit dfB
 
 -- | Place register on /backward/ part of a circuit. This is implemented using
@@ -1228,7 +1259,7 @@ registerBwd ::
   Circuit dfA dfB
 registerBwd dfA dfB
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.registerBwd) idC
+  |> tupCircuits (Df.registerBwd) idC'
   |> toDfCircuit dfB
 
 -- | A fifo buffer with user-provided depth. Uses blockram to store data
@@ -1248,7 +1279,7 @@ fifo ::
   Circuit dfA dfB
 fifo dfA dfB fifoDepth
   =  fromDfCircuit dfA
-  |> tupCircuits (Df.fifo fifoDepth) idC
+  |> tupCircuits (Df.fifo fifoDepth) idC'
   |> toDfCircuit dfB where
 
 -- | Emit values given in list. Emits no data while reset is asserted. Not
@@ -1259,7 +1290,7 @@ drive ::
   Proxy dfA ->
   SimulationConfig ->
   [Maybe (FwdPayload dfA)] ->
-  Circuit () dfA
+  Circuit NC dfA
 drive dfA conf s0 = Df.drive conf s0 |> dfToDfConvOtp dfA
 
 -- | Sample protocol to a list of values. Drops values while reset is asserted.
@@ -1271,7 +1302,7 @@ sample ::
   , HiddenClockResetEnable (Dom dfB) ) =>
   Proxy dfB ->
   SimulationConfig ->
-  Circuit () dfB ->
+  Circuit NC dfB ->
   [Maybe (FwdPayload dfB)]
 sample dfB conf c = Df.sample conf (c |> dfToDfConvInp dfB)
 
@@ -1341,6 +1372,7 @@ simulate dfA dfB conf circ inputs = Df.simulate conf circ' inputs where
 -- (a list of acknowledges to provide), and a @[Data (BwdPayload dfB)]@ (a list
 -- of data values to feed in).
 dfConvTestBench ::
+  forall dfA dfB.
   ( DfConv dfA
   , DfConv dfB
   , NFDataX (BwdPayload dfB)
@@ -1358,22 +1390,22 @@ dfConvTestBench ::
     (Df (Dom dfB) (FwdPayload dfB))
 dfConvTestBench dfA dfB bwdAcks bwdPayload circ
   =  mapCircuit (, ()) P.fst P.fst (, ())
-  $  tupCircuits idC (ackCircuit dfA)
+  $  tupCircuits idC'' ackCircuit
   |> toDfCircuit dfA
   |> circ
   |> fromDfCircuit dfB
-  |> tupCircuits idC driveCircuit
+  |> tupCircuits idC'' driveCircuit
  where
-  ackCircuit ::
-    Proxy dfA ->
-    Circuit (Reverse ()) (Reverse (Df (Dom dfA) (BwdPayload dfA)))
-  ackCircuit _
-    = reverseCircuit
-    $ Circuit
-    $ P.const
-    ( boolsToBwd (Proxy @(Df _ _)) bwdAcks
-    , () )
-  driveCircuit = reverseCircuit (driveC def bwdPayload)
+  idC'' :: Circuit (Df dom a) (Df dom a)
+  idC'' = idC
+
+  ackCircuit = reverseCircuit
+    (Circuit (P.const (boolsToBwd (Proxy @(Df _ _)) bwdAcks, ()))
+      :: Circuit (Df (Dom dfA) (BwdPayload dfA)) NC)
+
+  driveCircuit = reverseCircuit
+    (driveC def bwdPayload
+       :: Circuit NC (Df (Dom dfB) (BwdPayload dfB)))
 
 -- | Given behavior along the forward channel, turn an arbitrary 'DfConv'
 -- circuit into an easily-testable 'Df' circuit representing the backward
@@ -1381,6 +1413,7 @@ dfConvTestBench dfA dfB bwdAcks bwdPayload circ
 -- @[Data (FwdPayload dfA)]@ (a list of data values to feed in), and a @[Bool]@
 -- (a list of acknowledges to provide).
 dfConvTestBenchRev ::
+  forall dfA dfB.
   ( DfConv dfA
   , DfConv dfB
   , NFDataX (FwdPayload dfA)
@@ -1399,16 +1432,15 @@ dfConvTestBenchRev ::
 dfConvTestBenchRev dfA dfB fwdPayload fwdAcks circ
   =  mapCircuit ((), ) P.snd P.snd ((), )
   $  reverseCircuit
-  $  tupCircuits driveCircuit idC
+  $  tupCircuits driveCircuit idC'
   |> toDfCircuit dfA
   |> circ
   |> fromDfCircuit dfB
-  |> tupCircuits (ackCircuit dfB) idC
+  |> tupCircuits ackCircuit idC'
  where
+  ackCircuit :: Circuit (Df (Dom dfB) (FwdPayload dfB)) NC
+  ackCircuit =
+    Circuit (P.const (boolsToBwd (Proxy @(Df _ _)) fwdAcks, ()))
+
+  driveCircuit :: Circuit NC (Df (Dom dfA) (FwdPayload dfA))
   driveCircuit = driveC def fwdPayload
-  ackCircuit :: Proxy dfB -> Circuit (Df (Dom dfB) (FwdPayload dfB)) ()
-  ackCircuit _
-    = Circuit
-    $ P.const
-    ( boolsToBwd (Proxy @(Df _ _)) fwdAcks
-    , () )
diff --git a/src/Protocols/Hedgehog/Internal.hs b/src/Protocols/Hedgehog/Internal.hs
index 2344d529..4ea1c814 100644
--- a/src/Protocols/Hedgehog/Internal.hs
+++ b/src/Protocols/Hedgehog/Internal.hs
@@ -161,12 +161,13 @@ instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where
 
 instance
   ( Test a
+  , a ~ (fwd >< bwd)
   , C.KnownNat n
   , 1 <= (n * SimulateChannels a)
-  , 1 <= n ) => Test (C.Vec n a) where
+  , 1 <= n ) => Test (C.Vec n fwd >< C.Vec n bwd) where
   expectToLengths ::
-    Proxy (C.Vec n a) ->
-    ExpectType (C.Vec n a) ->
+    Proxy (IVec n a) ->
+    ExpectType (IVec n a) ->
     C.Vec (n * SimulateChannels a) Int
   expectToLengths Proxy =
     C.concatMap (expectToLengths (Proxy @a))
@@ -174,7 +175,7 @@ instance
   expectN ::
     forall m.
     (HasCallStack, H.MonadTest m) =>
-    Proxy (C.Vec n a) ->
+    Proxy (IVec n a) ->
     ExpectOptions ->
     C.Vec (n * SimulateChannels a) Int ->
     C.Vec n (SimulateFwdType a) ->
@@ -188,9 +189,11 @@ instance
 
 instance
   ( Test a, Test b
-  , 1 <= (SimulateChannels a + SimulateChannels b) ) => Test (a, b) where
+  , a ~ (fa >< ba), b ~ (fb >< bb)
+  , 1 <= (SimulateChannels a + SimulateChannels b)
+  ) => Test ((fa, fb) >< (ba, bb)) where
   expectToLengths ::
-    Proxy (a, b) ->
+    Proxy (I2 a b) ->
     (ExpectType a, ExpectType b) ->
     C.Vec (SimulateChannels a + SimulateChannels b) Int
   expectToLengths Proxy (t1, t2) =
@@ -199,7 +202,7 @@ instance
   expectN ::
     forall m.
     (HasCallStack, H.MonadTest m) =>
-    Proxy (a, b) ->
+    Proxy (I2 a b) ->
     ExpectOptions ->
     C.Vec (SimulateChannels a + SimulateChannels b) Int ->
     (SimulateFwdType a, SimulateFwdType b) ->
diff --git a/src/Protocols/Internal.hs b/src/Protocols/Internal.hs
index d5dbf5ab..534fadd0 100644
--- a/src/Protocols/Internal.hs
+++ b/src/Protocols/Internal.hs
@@ -14,6 +14,7 @@ Internal module to prevent hs-boot files (breaks Haddock)
 
 module Protocols.Internal where
 
+import qualified Control.Category as Cat
 import           Control.DeepSeq (NFData)
 import           Data.Hashable (Hashable)
 import           Data.Maybe (fromMaybe)
@@ -21,7 +22,7 @@ import           Data.Proxy
 import           GHC.Base (Any)
 import           Prelude hiding (map, const)
 
-import           Clash.Prelude (Signal, type (+), type (*))
+import           Clash.Prelude (Signal, type (+), type (*), Nat)
 import qualified Clash.Prelude as C
 import qualified Clash.Explicit.Prelude as CE
 
@@ -148,9 +149,48 @@ import           GHC.Generics (Generic)
 --
 --   2. It eliminates the need for manually routing acknowledgement lines
 --
-newtype Circuit a b =
+newtype Circuit (a :: CircuitInterface) (b :: CircuitInterface) =
   Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) )
 
+instance Cat.Category Circuit where
+  id = Circuit swap
+  c2 . c1 = c1 |> c2
+
+type CircuitInterface = (Type, Type)
+
+infixl ><
+type (><) a b = '(a, b)
+
+type family Fwd (a :: CircuitInterface) :: Type  where
+  Fwd (x >< _) = x
+
+type family Bwd (a :: CircuitInterface) :: Type  where
+  Bwd (_ >< x) = x
+
+type NC = (() >< ())
+
+type I0 = (() >< ())
+
+type I1
+  (a :: CircuitInterface)
+  = a
+
+type I2
+  (a :: CircuitInterface)
+  (b :: CircuitInterface)
+  = (Fwd a, Fwd b) >< (Bwd a, Bwd b)
+
+type I3
+  (a :: CircuitInterface)
+  (b :: CircuitInterface)
+  (c :: CircuitInterface)
+  = (Fwd a, Fwd b, Fwd c) >< (Bwd a, Bwd b, Bwd c)
+
+type IVec
+  (n :: Nat)
+  (a :: CircuitInterface)
+  = (C.Vec n (Fwd a) >< C.Vec n (Bwd a))
+
 -- | Protocol-agnostic acknowledgement
 newtype Ack = Ack Bool
   deriving (Generic, C.NFDataX, Show, C.Bundle)
@@ -167,41 +207,6 @@ data CSignal dom a = CSignal (Signal dom a)
 instance Default a => Default (CSignal dom a) where
   def = CSignal def
 
--- | A protocol describes the in- and outputs of one side of a 'Circuit'.
-class Protocol a where
-  -- | Sender to receiver type family. See 'Circuit' for an explanation on the
-  -- existence of 'Fwd'.
-  type Fwd (a :: Type)
-
-  -- | Receiver to sender type family. See 'Circuit' for an explanation on the
-  -- existence of 'Bwd'.
-  type Bwd (a :: Type)
-
-instance Protocol () where
-  type Fwd () = ()
-  type Bwd () = ()
-
-instance Protocol (a, b) where
-  type Fwd (a, b) = (Fwd a, Fwd b)
-  type Bwd (a, b) = (Bwd a, Bwd b)
-
-instance Protocol (a, b, c) where
-  type Fwd (a, b, c) = (Fwd a, Fwd b, Fwd c)
-  type Bwd (a, b, c) = (Bwd a, Bwd b, Bwd c)
-
-instance Protocol (a, b, c, d) where
-  type Fwd (a, b, c, d) = (Fwd a, Fwd b, Fwd c, Fwd d)
-  type Bwd (a, b, c, d) = (Bwd a, Bwd b, Bwd c, Bwd d)
-
-instance C.KnownNat n => Protocol (C.Vec n a) where
-  type Fwd (C.Vec n a) = C.Vec n (Fwd a)
-  type Bwd (C.Vec n a) = C.Vec n (Bwd a)
-
--- XXX: Type families with Signals on LHS are currently broken on Clash:
-instance Protocol (CSignal dom a) where
-  type Fwd (CSignal dom a) = CSignal dom a
-  type Bwd (CSignal dom a) = CSignal dom ()
-
 -- | Left-to-right circuit composition.
 --
 -- @
@@ -232,28 +237,49 @@ infixr 1 |>
     (r2sAb, s2rBc)
 
 -- | Conversion from booleans to protocol specific acknowledgement values.
-class Protocol a => Backpressure a where
+class Backpressure (a :: CircuitInterface) where
   -- | Interpret list of booleans as a list of acknowledgements at every cycle.
   -- Implementations don't have to account for finite lists.
   boolsToBwd :: Proxy a -> [Bool] -> Bwd a
 
-instance Backpressure () where
+instance Backpressure (a >< ()) where
   boolsToBwd _ _ = ()
 
-instance (Backpressure a, Backpressure b) => Backpressure (a, b) where
-  boolsToBwd _ bs = (boolsToBwd (Proxy @a) bs, boolsToBwd (Proxy @b) bs)
-
-instance (Backpressure a, Backpressure b, Backpressure c) => Backpressure (a, b, c) where
+instance
+  ( Backpressure (f0 >< b0)
+  , Backpressure (f1 >< b1)
+  ) =>
+    Backpressure ((f0, f1) >< (b0, b1))
+ where
   boolsToBwd _ bs =
-    ( boolsToBwd (Proxy @a) bs
-    , boolsToBwd (Proxy @b) bs
-    , boolsToBwd (Proxy @c) bs )
-
-instance (C.KnownNat n, Backpressure a) => Backpressure (C.Vec n a) where
-  boolsToBwd _ bs = C.repeat (boolsToBwd (Proxy @a) bs)
+    ( boolsToBwd (Proxy @(f0 >< b0)) bs
+    , boolsToBwd (Proxy @(f1 >< b1)) bs
+    )
+
+instance
+  ( Backpressure (f0 >< b0)
+  , Backpressure (f1 >< b1)
+  , Backpressure (f2 >< b2)
+  ) =>
+    Backpressure ((f0, f1, f2) >< (b0, b1, b2))
+ where
+  boolsToBwd _ bs =
+    ( boolsToBwd (Proxy @(f0 >< b0)) bs
+    , boolsToBwd (Proxy @(f1 >< b1)) bs
+    , boolsToBwd (Proxy @(f2 >< b2)) bs
+    )
+
+instance
+  ( C.KnownNat n
+  , Backpressure (fwd >< bwd)
+  ) =>
+    Backpressure (C.Vec n fwd >< C.Vec n bwd)
+ where
+  boolsToBwd _ bs = C.repeat (boolsToBwd (Proxy @(fwd >< bwd)) bs)
 
-instance Backpressure (CSignal dom a) where
-  boolsToBwd _ _ = CSignal (pure ())
+instance Backpressure (CSignal dom a >< CSignal dom ())
+ where
+  boolsToBwd _ _ = CSignal $ pure ()
 
 -- | Right-to-left circuit composition.
 --
@@ -312,7 +338,7 @@ idC = Circuit swap
 repeatC ::
   forall n a b.
   Circuit a b ->
-  Circuit (C.Vec n a) (C.Vec n b)
+  Circuit (IVec n a) (IVec n b)
 repeatC (Circuit f) =
   Circuit (C.unzip . C.map f . uncurry C.zip)
 
@@ -322,7 +348,9 @@ prod2C ::
   forall a c b d.
   Circuit a b ->
   Circuit c d ->
-  Circuit (a, c) (b, d)
+  Circuit
+    ((Fwd a, Fwd c) >< (Bwd a, Bwd c))
+    ((Fwd b, Fwd d) >< (Bwd b, Bwd d))
 prod2C (Circuit a) (Circuit c) =
   Circuit (\((aFwd, cFwd), (bBwd, dBwd)) ->
     let
@@ -426,13 +454,13 @@ class (C.KnownNat (SimulateChannels a), Backpressure a, Simulate a) => Drivable
   driveC ::
     SimulationConfig ->
     SimulateFwdType a ->
-    Circuit () a
+    Circuit NC a
 
   -- | Sample a circuit that is trivially drivable. Use 'driveC'  to create
   -- such a circuit. Related: 'simulateC'.
   sampleC ::
     SimulationConfig ->
-    Circuit () a ->
+    Circuit NC a ->
     SimulateFwdType a
 
 
@@ -444,7 +472,7 @@ class (C.KnownNat (SimulateChannels a), Backpressure a, Simulate a) => Drivable
 -- The 'simulateCircuit' function can thus receive the necessary simulation types, convert
 -- them to types on the 'Signal' level, pass those signals to the circuit, and convert the
 -- result of the circuit back to the simulation types giving the final result.
-class (C.KnownNat (SimulateChannels a), Protocol a) => Simulate a where
+class C.KnownNat (SimulateChannels a) => Simulate (a :: CircuitInterface) where
   -- | The type that a test must provide to the 'simulateCircuit' function in the forward direction.
   -- Usually this is some sort of list.
   type SimulateFwdType a :: Type
@@ -487,10 +515,10 @@ class (C.KnownNat (SimulateChannels a), Protocol a) => Simulate a where
     Circuit a a
 
 
-instance Simulate () where
-  type SimulateFwdType () = ()
-  type SimulateBwdType () = ()
-  type SimulateChannels () = 0
+instance Simulate NC where
+  type SimulateFwdType NC = ()
+  type SimulateBwdType NC = ()
+  type SimulateChannels NC = 0
 
   simToSigFwd _ = id
   simToSigBwd _ = id
@@ -499,8 +527,9 @@ instance Simulate () where
 
   stallC _ _ = idC
 
-instance Drivable () where
-  type ExpectType () = ()
+
+instance Drivable NC where
+  type ExpectType NC = ()
 
   toSimulateType Proxy () = ()
   fromSimulateType Proxy () = ()
@@ -508,22 +537,49 @@ instance Drivable () where
   driveC _ _ = idC
   sampleC _  _ = ()
 
+instance
+  ( Simulate (f0 >< b0)
+  , Simulate (f1 >< b1)
+  ) =>
+    Simulate ((f0, f1) >< (b0, b1)) where
+  type SimulateFwdType ((f0, f1) >< (b0, b1)) =
+    (SimulateFwdType (f0 >< b0), SimulateFwdType (f1 >< b1))
+
+  type SimulateBwdType ((f0, f1) >< (b0, b1)) =
+    (SimulateBwdType (f0 >< b0), SimulateBwdType (f1 >< b1))
+
+  type SimulateChannels ((f0, f1) >< (b0, b1)) =
+    SimulateChannels (f0 >< b0) + SimulateChannels (f1 >< b1)
+
+  simToSigFwd Proxy (fwdsA, fwdsB) =
+    ( simToSigFwd (Proxy @(f0 >< b0)) fwdsA
+    , simToSigFwd (Proxy @(f1 >< b1)) fwdsB
+    )
 
-instance (Simulate a, Simulate b) => Simulate (a, b) where
-  type SimulateFwdType (a, b) = (SimulateFwdType a, SimulateFwdType b)
-  type SimulateBwdType (a, b) = (SimulateBwdType a, SimulateBwdType b)
-  type SimulateChannels (a, b) = SimulateChannels a + SimulateChannels b
+  simToSigBwd Proxy (bwdsA, bwdsB) =
+    ( simToSigBwd (Proxy @(f0 >< b0)) bwdsA
+    , simToSigBwd (Proxy @(f1 >< b1)) bwdsB
+    )
 
-  simToSigFwd Proxy (fwdsA, fwdsB) = (simToSigFwd (Proxy @a) fwdsA, simToSigFwd (Proxy @b) fwdsB)
-  simToSigBwd Proxy (bwdsA, bwdsB) = (simToSigBwd (Proxy @a) bwdsA, simToSigBwd (Proxy @b) bwdsB)
-  sigToSimFwd Proxy (fwdSigA, fwdSigB) = (sigToSimFwd (Proxy @a) fwdSigA, sigToSimFwd (Proxy @b) fwdSigB)
-  sigToSimBwd Proxy (bwdSigA, bwdSigB) = (sigToSimBwd (Proxy @a) bwdSigA, sigToSimBwd (Proxy @b) bwdSigB)
+  sigToSimFwd Proxy (fwdSigA, fwdSigB) =
+    ( sigToSimFwd (Proxy @(f0 >< b0)) fwdSigA
+    , sigToSimFwd (Proxy @(f1 >< b1)) fwdSigB
+    )
+
+  sigToSimBwd Proxy (bwdSigA, bwdSigB) =
+    ( sigToSimBwd (Proxy @(f0 >< b0)) bwdSigA
+    , sigToSimBwd (Proxy @(f1 >< b1)) bwdSigB
+    )
 
   stallC conf stalls =
     let
-      (stallsL, stallsR) = C.splitAtI @(SimulateChannels a) @(SimulateChannels b) stalls
-      Circuit stalledL = stallC @a conf stallsL
-      Circuit stalledR = stallC @b conf stallsR
+      (stallsL, stallsR) =
+        C.splitAtI
+          @(SimulateChannels (f0 >< b0))
+          @(SimulateChannels (f1 >< b1))
+          stalls
+      Circuit stalledL = stallC @(f0 >< b0) conf stallsL
+      Circuit stalledR = stallC @(f1 >< b1) conf stallsR
     in
       Circuit $ \((fwdL0, fwdR0), (bwdL0, bwdR0)) ->
         let
@@ -532,73 +588,104 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where
         in
           ((fwdL1, fwdR1), (bwdL1, bwdR1))
 
-instance (Drivable a, Drivable b) => Drivable (a, b) where
-  type ExpectType (a, b) = (ExpectType a, ExpectType b)
+instance
+  ( Drivable (f0 >< b0)
+  , Drivable (f1 >< b1)
+  ) =>
+    Drivable ((f0, f1) >< (b0, b1))
+ where
+  type ExpectType ((f0, f1) >< (b0, b1)) =
+    ( ExpectType (f0 >< b0)
+    , ExpectType (f1 >< b1)
+    )
 
   toSimulateType Proxy (t1, t2) =
-    ( toSimulateType (Proxy @a) t1
-    , toSimulateType (Proxy @b) t2 )
+    ( toSimulateType (Proxy @(f0 >< b0)) t1
+    , toSimulateType (Proxy @(f1 >< b1)) t2 )
 
   fromSimulateType Proxy (t1, t2) =
-    ( fromSimulateType (Proxy @a) t1
-    , fromSimulateType (Proxy @b) t2 )
+    ( fromSimulateType (Proxy @(f0 >< b0)) t1
+    , fromSimulateType (Proxy @(f1 >< b1)) t2 )
 
   driveC conf (fwd1, fwd2) =
-    let (Circuit f1, Circuit f2) = (driveC @a conf fwd1, driveC @b conf fwd2) in
-    Circuit (\(_, ~(bwd1, bwd2)) -> ((), (snd (f1 ((), bwd1)), snd (f2 ((), bwd2)))))
+    let
+      (Circuit f1, Circuit f2) =
+        ( driveC @(f0 >< b0) conf fwd1
+        , driveC @(f1 >< b1) conf fwd2
+        )
+     in
+      Circuit $ \(_, ~(bwd1, bwd2)) ->
+        ( (), ( snd (f1 ((), bwd1))
+              , snd (f2 ((), bwd2))
+              )
+        )
 
   sampleC conf (Circuit f) =
     let
       bools = replicate (resetCycles conf) False <> repeat True
-      (_, (fwd1, fwd2)) = f ((), (boolsToBwd (Proxy @a) bools, boolsToBwd (Proxy @b) bools))
+      (_, (fwd1, fwd2)) =
+        f ((), ( boolsToBwd (Proxy @(f0 >< b0)) bools
+               , boolsToBwd (Proxy @(f1 >< b1)) bools
+               )
+          )
     in
-      ( sampleC @a conf (Circuit $ \_ -> ((), fwd1))
-      , sampleC @b conf (Circuit $ \_ -> ((), fwd2)) )
+      ( sampleC @(f0 >< b0) conf (Circuit $ \_ -> ((), fwd1))
+      , sampleC @(f1 >< b1) conf (Circuit $ \_ -> ((), fwd2)) )
 
 
 -- TODO TemplateHaskell?
 -- instance SimulateType (a, b, c)
 -- instance SimulateType (a, b, c, d)
 
-instance (CE.KnownNat n, Simulate a) => Simulate (C.Vec n a) where
-  type SimulateFwdType (C.Vec n a) = C.Vec n (SimulateFwdType a)
-  type SimulateBwdType (C.Vec n a) = C.Vec n (SimulateBwdType a)
-  type SimulateChannels (C.Vec n a) = n * SimulateChannels a
+instance (CE.KnownNat n, Simulate (fwd >< bwd)) =>
+  Simulate (C.Vec n fwd >< C.Vec n bwd)
+ where
+  type SimulateFwdType (C.Vec n fwd >< C.Vec n bwd) =
+    C.Vec n (SimulateFwdType (fwd >< bwd))
+
+  type SimulateBwdType (C.Vec n fwd >< C.Vec n bwd) =
+    C.Vec n (SimulateBwdType (fwd >< bwd))
 
-  simToSigFwd Proxy = C.map (simToSigFwd (Proxy @a))
-  simToSigBwd Proxy = C.map (simToSigBwd (Proxy @a))
-  sigToSimFwd Proxy = C.map (sigToSimFwd (Proxy @a))
-  sigToSimBwd Proxy = C.map (sigToSimBwd (Proxy @a))
+  type SimulateChannels (C.Vec n fwd >< C.Vec n bwd) =
+    n * SimulateChannels (fwd >< bwd)
+
+  simToSigFwd Proxy = C.map (simToSigFwd (Proxy @(fwd >< bwd)))
+  simToSigBwd Proxy = C.map (simToSigBwd (Proxy @(fwd >< bwd)))
+  sigToSimFwd Proxy = C.map (sigToSimFwd (Proxy @(fwd >< bwd)))
+  sigToSimBwd Proxy = C.map (sigToSimBwd (Proxy @(fwd >< bwd)))
 
   stallC conf stalls0 =
     let
-      stalls1 = C.unconcatI @n @(SimulateChannels a) stalls0
-      stalled = C.map (toSignals . stallC @a conf) stalls1
+      stalls1 = C.unconcatI @n @(SimulateChannels (fwd >< bwd)) stalls0
+      stalled = C.map (toSignals . stallC @(fwd >< bwd) conf) stalls1
     in
       Circuit $ \(fwds, bwds) -> C.unzip (C.zipWith ($) stalled (C.zip fwds bwds))
 
-instance (C.KnownNat n, Drivable a) => Drivable (C.Vec n a) where
-  type ExpectType (C.Vec n a) = C.Vec n (ExpectType a)
+instance (C.KnownNat n, Drivable (fwd >< bwd)) =>
+  Drivable (C.Vec n fwd >< C.Vec n bwd)
+ where
+  type ExpectType (C.Vec n fwd >< C.Vec n bwd) =
+    C.Vec n (ExpectType (fwd >< bwd))
 
-  toSimulateType Proxy = C.map (toSimulateType (Proxy @a))
-  fromSimulateType Proxy = C.map (fromSimulateType (Proxy @a))
+  toSimulateType Proxy = C.map (toSimulateType (Proxy @(fwd >< bwd)))
+  fromSimulateType Proxy = C.map (fromSimulateType (Proxy @(fwd >< bwd)))
 
   driveC conf fwds =
-    let circuits = C.map (($ ()) . curry . (toSignals @_ @a) . driveC conf) fwds in
+    let circuits = C.map (($ ()) . curry . (toSignals @_ @(fwd >< bwd)) . driveC conf) fwds in
     Circuit (\(_, bwds) -> ((), C.map snd (C.zipWith ($) circuits bwds)))
 
   sampleC conf (Circuit f) =
     let
       bools = replicate (resetCycles conf) False <> repeat True
-      (_, fwds) = f ((), (C.repeat (boolsToBwd (Proxy @a) bools)))
+      (_, fwds) = f ((), (C.repeat (boolsToBwd (Proxy @(fwd >< bwd)) bools)))
     in
-      C.map (\fwd -> sampleC @a conf (Circuit $ \_ -> ((), fwd))) fwds
+      C.map (\fwd -> sampleC @(fwd >< bwd) conf (Circuit $ \_ -> ((), fwd))) fwds
 
 
-instance (C.KnownDomain dom) => Simulate (CSignal dom a) where
-  type SimulateFwdType (CSignal dom a) = [a]
-  type SimulateBwdType (CSignal dom a) = ()
-  type SimulateChannels (CSignal dom a) = 1
+instance (C.KnownDomain dom) => Simulate (CSignal dom a >< CSignal dom ()) where
+  type SimulateFwdType (CSignal dom a >< CSignal dom ()) = [a]
+  type SimulateBwdType (CSignal dom a >< CSignal dom ()) = ()
+  type SimulateChannels (CSignal dom a >< CSignal dom ()) = 1
 
   simToSigFwd Proxy list = CSignal (C.fromList_lazy list)
   simToSigBwd Proxy () = def
@@ -610,8 +697,10 @@ instance (C.KnownDomain dom) => Simulate (CSignal dom a) where
 instance Default (CSignal dom (Const () a)) where
   def = CSignal (pure (Const ()))
 
-instance (C.NFDataX a, C.ShowX a, Show a, C.KnownDomain dom) => Drivable (CSignal dom a) where
-  type ExpectType (CSignal dom a) = [a]
+instance (C.NFDataX a, C.ShowX a, Show a, C.KnownDomain dom) =>
+  Drivable (CSignal dom a >< CSignal dom ())
+ where
+  type ExpectType (CSignal dom a >< CSignal dom ()) = [a]
 
   toSimulateType Proxy = id
   fromSimulateType Proxy = id
@@ -625,7 +714,6 @@ instance (C.NFDataX a, C.ShowX a, Show a, C.KnownDomain dom) => Drivable (CSigna
     let sampled = CE.sample_lazy ((\(CSignal s) -> s) (snd (f ((), def)))) in
     if ignoreReset then drop resetCycles sampled else sampled
 
-
 -- | Simulate a circuit. Includes samples while reset is asserted.
 -- Not synthesizable.
 --
@@ -803,14 +891,9 @@ keepTypeFalse = Proxy
 fromKeepTypeTrue :: KeepType 'True t -> t
 fromKeepTypeTrue = runIdentity
 
--- | Protocol to reverse a circuit.
--- 'Fwd' becomes 'Bwd' and vice versa.
--- No changes are made otherwise.
-data Reverse a
-
-instance Protocol a => Protocol (Reverse a) where
-  type Fwd (Reverse a) = Bwd a
-  type Bwd (Reverse a) = Fwd a
+-- | Reverse a circuit. 'Fwd' becomes 'Bwd' and vice versa. No
+-- changes are made otherwise.
+type Reverse a = Bwd a >< Fwd a
 
 -- | Apply 'Reverse' both sides of a circuit, and then switch them.
 -- Input and output of the underlying circuit are the same,
@@ -832,12 +915,12 @@ mapCircuit ia oa ob ib (Circuit f) = Circuit ((oa *** ob) . f . (ia *** ib))
 
 -- | "Bundle" together a 'C.Vec' of 'Circuit's into a 'Circuit' with 'C.Vec' input and output.
 -- The 'Circuit's all run in parallel.
-vecCircuits :: (C.KnownNat n) => C.Vec n (Circuit a b) -> Circuit (C.Vec n a) (C.Vec n b)
+vecCircuits :: (C.KnownNat n) => C.Vec n (Circuit a b) -> Circuit (IVec n a) (IVec n b)
 vecCircuits fs = Circuit (\inps -> C.unzip $ f <$> fs <*> uncurry C.zip inps) where
   f (Circuit ff) x = ff x
 
 -- | "Bundle" together a pair of 'Circuit's into a 'Circuit' with two inputs and outputs.
 -- The 'Circuit's run in parallel.
-tupCircuits :: Circuit a b -> Circuit c d -> Circuit (a,c) (b,d)
+tupCircuits :: Circuit a b -> Circuit c d -> Circuit (I2 a c) (I2 b d)
 tupCircuits (Circuit f) (Circuit g) = Circuit (reorder . (f *** g) . reorder) where
   reorder ~(~(a,b),~(c,d)) = ((a,c),(b,d))
diff --git a/src/Protocols/Wishbone.hs b/src/Protocols/Wishbone.hs
index d466eb17..168fdfba 100644
--- a/src/Protocols/Wishbone.hs
+++ b/src/Protocols/Wishbone.hs
@@ -192,19 +192,14 @@ data WishboneMode
   deriving (C.Generic, Show, Eq)
 
 -- | The Wishbone protocol (http://cdn.opencores.org/downloads/wbspec_b4.pdf)
-data
+type
   Wishbone
     (dom :: C.Domain)
     (mode :: WishboneMode)
     (addressWidth :: Nat)
     (userType :: Type)
-
-instance Protocol (Wishbone dom mode addressWidth dat) where
-  type
-    Fwd (Wishbone dom mode addressWidth dat) =
-      Signal dom (WishboneM2S addressWidth (C.BitSize dat `DivRU` 8) dat)
-
-  type Bwd (Wishbone dom mode addressWidth dat) = Signal dom (WishboneS2M dat)
+  =  Signal dom (WishboneM2S addressWidth (C.BitSize userType `DivRU` 8) userType)
+  >< Signal dom (WishboneS2M userType)
 
 -- | Construct "default" Wishbone M2S signals
 emptyWishboneM2S ::
diff --git a/src/Protocols/Wishbone/Standard.hs b/src/Protocols/Wishbone/Standard.hs
index 7e0a4c42..a5ba7448 100644
--- a/src/Protocols/Wishbone/Standard.hs
+++ b/src/Protocols/Wishbone/Standard.hs
@@ -24,7 +24,7 @@ roundrobin ::
   ) =>
   Circuit
     (Wishbone dom 'Standard addressWidth a)
-    (Vec n (Wishbone dom 'Standard addressWidth a))
+    (IVec n (Wishbone dom 'Standard addressWidth a))
 roundrobin = Circuit $ \(m2s, s2ms) -> B.first head $ fn (singleton m2s, s2ms)
  where
   Circuit fn = sharedBus selectFn
@@ -53,8 +53,8 @@ sharedBus ::
     Signal dom (Index n, Index m)
   ) ->
   Circuit
-    (Vec n (Wishbone dom 'Standard addressWidth a))
-    (Vec m (Wishbone dom 'Standard addressWidth a))
+    (IVec n (Wishbone dom 'Standard addressWidth a))
+    (IVec m (Wishbone dom 'Standard addressWidth a))
 sharedBus selectFn = Circuit go
  where
   go (bundle -> m2ss0, bundle -> s2ms0) = (unbundle s2ms1, unbundle m2ss1)
@@ -83,10 +83,10 @@ crossbarSwitch ::
     KnownNat (BitSize a)
   ) =>
   Circuit
-    ( CSignal dom (Vec n (Index m)), -- route
-      Vec n (Wishbone dom 'Standard addressWidth a) -- masters
+    (I2 (CSignal dom (Vec n (Index m)) >< CSignal dom ()) -- route
+        (IVec n (Wishbone dom 'Standard addressWidth a)) -- masters
     )
-    (Vec m (Wishbone dom 'Standard addressWidth a)) -- slaves
+    (IVec m (Wishbone dom 'Standard addressWidth a)) -- slaves
 crossbarSwitch = Circuit go
  where
   go ((CSignal route, bundle -> m2ss0), bundle -> s2ms0) =
@@ -123,7 +123,7 @@ memoryWb ::
     Default a
   ) =>
   (Signal dom (BitVector addressWidth) -> Signal dom (Maybe (BitVector addressWidth, a)) -> Signal dom a) ->
-  Circuit (Wishbone dom 'Standard addressWidth a) ()
+  Circuit (Wishbone dom 'Standard addressWidth a) NC
 memoryWb ram = Circuit go
  where
   go (m2s, ()) = (mux inCycle s2m1 (pure emptyWishboneS2M), ())
diff --git a/src/Protocols/Wishbone/Standard/Hedgehog.hs b/src/Protocols/Wishbone/Standard/Hedgehog.hs
index aaf7a508..a010406d 100644
--- a/src/Protocols/Wishbone/Standard/Hedgehog.hs
+++ b/src/Protocols/Wishbone/Standard/Hedgehog.hs
@@ -304,7 +304,7 @@ driveStandard ::
   ExpectOptions ->
   -- | Requests to send out
   [(WishboneMasterRequest addressWidth a, Int)] ->
-  Circuit () (Wishbone dom 'Standard addressWidth a)
+  Circuit NC (Wishbone dom 'Standard addressWidth a)
 driveStandard ExpectOptions {..} requests =
   Circuit $
     ((),)
@@ -449,7 +449,7 @@ wishbonePropWithModel ::
   --   Return an error message 'Left' or the updated state 'Right'
   (WishboneMasterRequest addressWidth a -> WishboneS2M a -> st -> Either String st) ->
   -- | The circuit to run the test against.
-  Circuit (Wishbone dom 'Standard addressWidth a) () ->
+  Circuit (Wishbone dom 'Standard addressWidth a) NC ->
   -- | Inputs to the circuit and model
   H.Gen [WishboneMasterRequest addressWidth a] ->
   -- | Initial state of the model
@@ -493,8 +493,8 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = do
 observeComposedWishboneCircuit ::
   (KnownDomain dom) =>
   Maybe Int ->
-  Circuit () (Wishbone dom mode addressWidth a) ->
-  Circuit (Wishbone dom mode addressWidth a) () ->
+  Circuit NC (Wishbone dom mode addressWidth a) ->
+  Circuit (Wishbone dom mode addressWidth a) NC ->
   ( [WishboneM2S addressWidth (BitSize a `DivRU` 8) a],
     [WishboneS2M a]
   )
diff --git a/tests/Tests/Protocols/Axi4.hs b/tests/Tests/Protocols/Axi4.hs
index 2c61fe4f..be15c213 100644
--- a/tests/Tests/Protocols/Axi4.hs
+++ b/tests/Tests/Protocols/Axi4.hs
@@ -69,12 +69,12 @@ prop_axi4_convert_write_id =
  where
   ckt :: (C.HiddenClockResetEnable dom) =>
    Circuit
-    (Axi4WriteAddress dom ConfAW Int,
-     Axi4WriteData dom ConfW Int,
-     Reverse (Axi4WriteResponse dom ConfB Int))
-    (Axi4WriteAddress dom ConfAW Int,
-     Axi4WriteData dom ConfW Int,
-     Reverse (Axi4WriteResponse dom ConfB Int))
+    (I3 (Axi4WriteAddress dom ConfAW Int)
+        (Axi4WriteData dom ConfW Int)
+        (Reverse (Axi4WriteResponse dom ConfB Int)))
+    (I3 (Axi4WriteAddress dom ConfAW Int)
+        (Axi4WriteData dom ConfW Int)
+        (Reverse (Axi4WriteResponse dom ConfB Int)))
   ckt = DfConv.convert Proxy Proxy
 
   genInfo =   (,,,,)
@@ -126,12 +126,12 @@ prop_axi4_convert_write_id_rev =
  where
   ckt :: (C.HiddenClockResetEnable dom) =>
    Circuit
-    (Axi4WriteAddress dom ConfAW Int,
-     Axi4WriteData dom ConfW Int,
-     Reverse (Axi4WriteResponse dom ConfB Int))
-    (Axi4WriteAddress dom ConfAW Int,
-     Axi4WriteData dom ConfW Int,
-     Reverse (Axi4WriteResponse dom ConfB Int))
+    (I3 (Axi4WriteAddress dom ConfAW Int)
+        (Axi4WriteData dom ConfW Int)
+        (Reverse (Axi4WriteResponse dom ConfB Int)))
+    (I3 (Axi4WriteAddress dom ConfAW Int)
+        (Axi4WriteData dom ConfW Int)
+        (Reverse (Axi4WriteResponse dom ConfB Int)))
   ckt = DfConv.convert Proxy Proxy
 
   genInfo = (,) <$> genResp <*> DfTest.genSmallInt
@@ -175,10 +175,10 @@ prop_axi4_convert_read_id =
  where
   ckt :: (C.HiddenClockResetEnable dom) =>
    Circuit
-   (Axi4ReadAddress dom ConfAR Int,
-    Reverse (Axi4ReadData dom ConfR Int Int))
-   (Axi4ReadAddress dom ConfAR Int,
-    Reverse (Axi4ReadData dom ConfR Int Int))
+     (I2 (Axi4ReadAddress dom ConfAR Int)
+         (Reverse (Axi4ReadData dom ConfR Int Int)))
+     (I2 (Axi4ReadAddress dom ConfAR Int)
+         (Reverse (Axi4ReadData dom ConfR Int Int)))
   ckt = DfConv.convert Proxy Proxy
 
   genInfo
@@ -222,10 +222,10 @@ prop_axi4_convert_read_id_rev =
  where
   ckt :: (C.HiddenClockResetEnable dom) =>
    Circuit
-   (Axi4ReadAddress dom ConfAR Int,
-    Reverse (Axi4ReadData dom ConfR Int Int))
-   (Axi4ReadAddress dom ConfAR Int,
-    Reverse (Axi4ReadData dom ConfR Int Int))
+     (I2 (Axi4ReadAddress dom ConfAR Int)
+         (Reverse (Axi4ReadData dom ConfR Int Int)))
+     (I2 (Axi4ReadAddress dom ConfAR Int)
+         (Reverse (Axi4ReadData dom ConfR Int Int)))
   ckt = DfConv.convert Proxy Proxy
 
   genInfo
diff --git a/tests/Tests/Protocols/DfConv.hs b/tests/Tests/Protocols/DfConv.hs
index 6931b3a9..14b35634 100644
--- a/tests/Tests/Protocols/DfConv.hs
+++ b/tests/Tests/Protocols/DfConv.hs
@@ -80,8 +80,11 @@ prop_df_zipwith_add =
     (uncurry (zipWith (+)))
     (C.withClockResetEnable @C.System C.clockGen C.resetGen C.enableGen ckt)
   where
-  ckt :: (C.HiddenClockResetEnable dom) => Circuit (Df dom Int, Df dom Int) (Df dom Int)
-  ckt = DfConv.zipWith (Proxy, Proxy) Proxy (+)
+  ckt ::
+    forall dom.
+    (C.HiddenClockResetEnable dom) =>
+    Circuit (I2 (Df dom Int) (Df dom Int)) (Df dom Int)
+  ckt = DfConv.zipWith (Proxy @(Df dom Int), Proxy @(Df dom Int)) Proxy (+)
 
 prop_df_fanout1 :: Property
 prop_df_fanout1 =
@@ -92,8 +95,11 @@ prop_df_fanout1 =
     (C.exposeClockResetEnable C.repeat)
     (C.exposeClockResetEnable ckt)
   where
-  ckt :: (C.HiddenClockResetEnable dom) => Circuit (Df dom Int) (C.Vec 1 (Df dom Int))
-  ckt = DfConv.fanout Proxy Proxy
+  ckt ::
+    forall dom.
+    (C.HiddenClockResetEnable dom) =>
+    Circuit (Df dom Int) (IVec 1 (Df dom Int))
+  ckt = DfConv.fanout Proxy (Proxy @(Df dom Int))
 
 prop_df_fanout2 :: Property
 prop_df_fanout2 =
@@ -104,8 +110,11 @@ prop_df_fanout2 =
     (C.exposeClockResetEnable C.repeat)
     (C.exposeClockResetEnable ckt)
   where
-  ckt :: (C.HiddenClockResetEnable dom) => Circuit (Df dom Int) (C.Vec 2 (Df dom Int))
-  ckt = DfConv.fanout Proxy Proxy
+  ckt ::
+    forall dom.
+    (C.HiddenClockResetEnable dom) =>
+    Circuit (Df dom Int) (IVec 2 (Df dom Int))
+  ckt = DfConv.fanout Proxy (Proxy @(Df dom Int))
 
 prop_df_fanout7 :: Property
 prop_df_fanout7 =
@@ -116,8 +125,11 @@ prop_df_fanout7 =
     (C.exposeClockResetEnable C.repeat)
     (C.exposeClockResetEnable ckt)
   where
-  ckt :: (C.HiddenClockResetEnable dom) => Circuit (Df dom Int) (C.Vec 7 (Df dom Int))
-  ckt = DfConv.fanout Proxy Proxy
+  ckt ::
+    forall dom.
+    (C.HiddenClockResetEnable dom) =>
+    Circuit (Df dom Int) (IVec 7 (Df dom Int))
+  ckt = DfConv.fanout Proxy (Proxy @(Df dom Int))
 
 prop_df_partition :: Property
 prop_df_partition =
@@ -128,8 +140,11 @@ prop_df_partition =
     (C.exposeClockResetEnable $ partition (>5))
     (C.exposeClockResetEnable ckt)
   where
-  ckt :: (C.HiddenClockResetEnable dom) => Circuit (Df dom Int) (Df dom Int, Df dom Int)
-  ckt = DfConv.partition Proxy (Proxy, Proxy) (> 5)
+  ckt ::
+    forall dom.
+    (C.HiddenClockResetEnable dom) =>
+    Circuit (Df dom Int) (I2 (Df dom Int) (Df dom Int))
+  ckt = DfConv.partition Proxy (Proxy @(Df dom Int), Proxy @(Df dom Int)) (> 5)
 
 prop_df_fanin :: Property
 prop_df_fanin =
@@ -140,8 +155,11 @@ prop_df_fanin =
     (C.exposeClockResetEnable $ map sum . transpose . C.toList)
     (C.exposeClockResetEnable ckt)
   where
-  ckt :: (C.HiddenClockResetEnable dom) => Circuit (C.Vec 3 (Df dom Int)) (Df dom Int)
-  ckt = DfConv.fanin Proxy Proxy (+)
+  ckt ::
+    forall dom.
+    (C.HiddenClockResetEnable dom) =>
+    Circuit (IVec 3 (Df dom Int)) (Df dom Int)
+  ckt = DfConv.fanin (Proxy @(Df dom Int)) Proxy (+)
 
 prop_df_fifo_id :: Property
 prop_df_fifo_id = propWithModelSingleDomain
@@ -163,7 +181,10 @@ prop_select =
     (snd . uncurry (mapAccumL goModel))
     (C.withClockResetEnable @C.System C.clockGen C.resetGen C.enableGen ckt)
  where
-  ckt :: (C.HiddenClockResetEnable dom) => Circuit (C.Vec 3 (Df dom Int), Df dom (C.Index 3)) (Df dom Int)
+  ckt :: (C.HiddenClockResetEnable dom) =>
+    Circuit
+      (I2 (IVec 3 (Df dom Int)) (Df dom (C.Index 3)))
+      (Df dom Int)
   ckt = DfConv.select (Proxy @(Df _ Int), (Proxy @(Df _ (C.Index 3)))) (Proxy @(Df _ Int))
 
   goModel :: C.Vec 3 [Int] -> C.Index 3 -> (C.Vec 3 [Int], Int)
@@ -203,8 +224,8 @@ prop_test_bench_id =
  where
   ckt :: (C.HiddenClockResetEnable dom) =>
    Circuit
-   (Df dom Int, Reverse (Df dom Int))
-   (Df dom Int, Reverse (Df dom Int))
+     (I2 (Df dom Int) (Reverse (Df dom Int)))
+     (I2 (Df dom Int) (Reverse (Df dom Int)))
   ckt = DfConv.convert Proxy Proxy
 
 prop_test_bench_rev_id :: Property
@@ -219,8 +240,8 @@ prop_test_bench_rev_id =
  where
   ckt :: (C.HiddenClockResetEnable dom) =>
    Circuit
-   (Df dom Int, Reverse (Df dom Int))
-   (Df dom Int, Reverse (Df dom Int))
+     (I2 (Df dom Int) (Reverse (Df dom Int)))
+     (I2 (Df dom Int) (Reverse (Df dom Int)))
   ckt = DfConv.convert Proxy Proxy
 
 
diff --git a/tests/Tests/Protocols/Plugin.hs b/tests/Tests/Protocols/Plugin.hs
index bf279f09..30100dcb 100644
--- a/tests/Tests/Protocols/Plugin.hs
+++ b/tests/Tests/Protocols/Plugin.hs
@@ -16,14 +16,14 @@ import qualified Protocols.Df as Df
 
 -- | Simply swap two streams. Note that the 'circuit' is a magic keyword the
 -- 'Protocols.Plugin' looks for in order to do its work.
-swapC :: Circuit (a, b) (b, a)
+swapC :: Circuit ((fa, fb) >< (ba, bb)) ((fb, fa) >< (bb, ba))
 swapC = circuit $ \(a, b) -> (b, a)
 
 
 -- | Put 'registerFwd' on both 'Df' input streams.
 registerBoth ::
   (C.NFDataX a, C.NFDataX b, C.HiddenClockResetEnable dom) =>
-  Circuit (Df dom a, Df dom b) (Df dom a, Df dom b)
+  Circuit (I2 (Df dom a) (Df dom b)) (I2 (Df dom a) (Df dom b))
 registerBoth = circuit $ \(a, b) -> do
   -- We route /a/ to into a 'registerFwd'. Note that this takes care of routing
   -- both the /forward/ and /backward/ parts, even though it seems that it only
@@ -41,7 +41,7 @@ registerBoth = circuit $ \(a, b) -> do
 -- | Fanout a stream and interact with some of the result streams.
 fanOutThenRegisterMiddle ::
   C.HiddenClockResetEnable dom =>
-  Circuit (Df dom Int) (Df dom Int, Df dom Int, Df dom Int)
+  Circuit (Df dom Int) (I3 (Df dom Int) (Df dom Int) (Df dom Int))
 fanOutThenRegisterMiddle = circuit $ \a -> do
   -- List notation can be used to specify a Vec. In this instance, fanout will
   -- infer that it needs to produce a 'Vec 3 Int'.
@@ -59,7 +59,7 @@ fanOutThenRegisterMiddle = circuit $ \a -> do
 
 
 -- | Forget the /left/ part of a tuple of 'Df' streams
-forgetLeft :: Circuit (Df dom a, Df dom b) (Df dom b)
+forgetLeft :: Circuit (I2 (Df dom a) (Df dom b)) (Df dom b)
 forgetLeft = circuit $ \(a, b) -> do
   -- We can use an underscore to indicate that we'd like to throw away any
   -- data from stream 'a'. For 'Df' like protocols, a constant acknowledgement
@@ -70,7 +70,7 @@ forgetLeft = circuit $ \(a, b) -> do
 
 
 -- | Forget the /left/ part of a tuple of 'Df' streams.
-forgetLeft2 :: Circuit (Df dom a, Df dom b) (Df dom b)
+forgetLeft2 :: Circuit (I2 (Df dom a) (Df dom b)) (Df dom b)
 forgetLeft2 =
   -- If we know right from the start that'd we'd like to ignore an incoming
   -- stream, we can simply mark it with an underscore.
@@ -78,7 +78,7 @@ forgetLeft2 =
 
 
 -- | Convert a 2-vector into a 2-tuple
-unvec :: Circuit (C.Vec 2 a) (a, a)
+unvec :: Circuit (C.Vec 2 fwd >< C.Vec 2 bwd) ((fwd, fwd) >< (bwd, bwd))
 unvec =
   -- We don't always need /do/ notation
   circuit \[x,y] -> (x, y)
diff --git a/tests/Tests/Protocols/Wishbone.hs b/tests/Tests/Protocols/Wishbone.hs
index 1998dc3c..c194d208 100644
--- a/tests/Tests/Protocols/Wishbone.hs
+++ b/tests/Tests/Protocols/Wishbone.hs
@@ -59,7 +59,7 @@ genWbTransferPair genA = liftA2 (,) (genWishboneTransfer genA) genSmallInt
 addrReadIdWb ::
   forall dom addressWidth.
   (KnownNat addressWidth) =>
-  Circuit (Wishbone dom 'Standard addressWidth (BitVector addressWidth)) ()
+  Circuit (Wishbone dom 'Standard addressWidth (BitVector addressWidth)) NC
 addrReadIdWb = Circuit go
   where
     go (m2s, ()) = (reply <$> m2s, ())
@@ -156,7 +156,7 @@ prop_memoryWb_model = property $
 -- Helpers
 --
 
-(|>>) :: Circuit () b -> Circuit b () -> (Fwd b, Bwd b)
+(|>>) :: Circuit NC b -> Circuit b NC -> (Fwd b, Bwd b)
 Circuit aFn |>> Circuit bFn = (s2rAb, r2sBc)
   where
     ~((), s2rAb) = aFn ((), r2sBc)
@@ -165,8 +165,8 @@ Circuit aFn |>> Circuit bFn = (s2rAb, r2sBc)
 evaluateUnitCircuit ::
   (KnownDomain dom, KnownNat (BitSize a), KnownNat addressWidth, NFDataX a) =>
   Int ->
-  Circuit () (Wishbone dom 'Standard addressWidth a) ->
-  Circuit (Wishbone dom 'Standard addressWidth a) () ->
+  Circuit NC (Wishbone dom 'Standard addressWidth a) ->
+  Circuit (Wishbone dom 'Standard addressWidth a) NC ->
   Int
 evaluateUnitCircuit n a b =
   let (bundle -> signals) = a |>> b
@@ -260,7 +260,7 @@ prop_specViolation_lenient = property $ do
   assert $ isLeft res
   where
     -- a circuit that terminates a cycle with more than one termination signal
-    invalidCircuit :: Circuit (Wishbone dom 'Standard 8 (BitVector 8)) ()
+    invalidCircuit :: Circuit (Wishbone dom 'Standard 8 (BitVector 8)) NC
     invalidCircuit = Circuit go
       where
         go (m2s, ()) = (reply <$> m2s, ())