Drop injectivity requirement of Bwd

src/Protocols/Df.hs

@@ -16,7 +16,7 @@ carries data, no metadata. For documentation see:
 
 module Protocols.Df
   ( -- * Types
-    Df, Data(..), Ack(..)
+    Df, Data(..)
 
     -- * Operations on Df like protocols
   , const, void, pure
@@ -65,7 +65,6 @@ import           Prelude hiding
 
 import           Data.Bifunctor (Bifunctor)
 import           Data.Coerce (coerce)
-import           Data.Default (Default)
 import           Data.Kind (Type)
 import qualified Data.Maybe as Maybe
 import           Data.Proxy
@@ -77,7 +76,7 @@ import           Clash.Signal.Internal (Signal)
 import qualified Clash.Prelude as C
 
 -- me
-import           Protocols.Internal hiding (Ack(..))
+import           Protocols.Internal
 import           Protocols.DfLike (DfLike)
 import qualified Protocols.DfLike as DfLike
 
@@ -98,11 +97,11 @@ 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 (Ack meta a)@
-  type Bwd (Df dom a) = Signal dom (Ack a)
+  -- | Backward part of simple dataflow: @Signal dom Bool@
+  type Bwd (Df dom a) = Signal dom Ack
 
 instance Backpressure (Df dom a) where
-  boolsToBwd = C.fromList_lazy . coerce
+  boolsToBwd _ = C.fromList_lazy . coerce
 
 -- | Data sent over forward channel of 'Df'. Note that this data type is strict
 -- on its data field.
@@ -135,14 +134,6 @@ dataToMaybe :: Data a -> Maybe a
 dataToMaybe NoData = Nothing
 dataToMaybe (Data a) = Just a
 
--- | Like 'Protocols.Df.Ack', but carrying phantom type variables to satisfy
--- 'Bwd's injectivity requirement.
-newtype Ack a = Ack Bool
-  deriving (Show)
-
-instance Default (Ack a) where
-  def = Ack True
-
 instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom a) where
   type SimulateType (Df dom a) = [Data a]
   type ExpectType (Df dom a) = [a]
@@ -158,7 +149,7 @@ instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom
 instance DfLike dom (Df dom) a where
   type Data (Df dom) a = Data a
   type Payload a = a
-  type Ack (Df dom) a = Ack a
+  type Ack (Df dom) a = Ack
 
   getPayload _ (Data a) = Just a
   getPayload _ NoData = Nothing

src/Protocols/DfLike.hs

@@ -96,7 +96,7 @@ class ( Protocol (df a)
   type Payload a = (r :: Type) | r -> a
 
   -- | Acknowledgement data carried on backward channel
-  type Ack df a = (r :: Type) | r -> a
+  type Ack df a
 
   noData ::
     Proxy (df a) ->
@@ -108,6 +108,7 @@ class ( Protocol (df a)
     Maybe (Payload a)
 
   setPayload ::
+    HasCallStack =>
     DfLike dom df b =>
     Proxy (df a) ->
     Proxy (df b) ->

src/Protocols/Internal.hs

@@ -98,19 +98,16 @@ import           GHC.Generics (Generic)
 -- data. Similar to /Bool/ we define:
 --
 -- @
---   data Ack a = DfNack | Ack
+--   newtype Ack = Ack Bool
 -- @
 --
--- (For technical reasons[1] we need the type variable /a/ in this definition,
--- even though we don't use it on the right hand side.)
---
 -- With these three definitions we're ready to make an instance for /Fwd/ and
 -- /Bwd/:
 --
 -- @
 -- instance Protocol (Df dom a) where
 --   type Fwd (Df dom a) = Signal dom (Data a)
---   type Bwd (Df dom a) = Signal dom (Ack a)
+--   type Bwd (Df dom a) = Signal dom Ack
 -- @
 --
 -- Having defined all this, we can take a look at /Circuit/ once more: now
@@ -128,7 +125,7 @@ import           GHC.Generics (Generic)
 --  +------------------------>+           +------------------------->
 --                            |           |
 --                            |           |
---       Signal dom (Ack a)   |           |  Signal dom (Ack b)
+--       Signal dom Ack       |           |  Signal dom Ack
 --  <-------------------------+           +<------------------------+
 --                            |           |
 --                            +-----------+
@@ -141,27 +138,24 @@ import           GHC.Generics (Generic)
 --
 --   2. It eliminates the need for manually routing acknowledgement lines
 --
--- Footnotes:
---
--- 1. Fwd and Bwd are injective type families. I.e., something on
---    the right hand side of a type instance must uniquely identify the left
---    hand side and vice versa. This helps type inference and error messages
---    substantially, in exchange for a slight syntactical artifact. As a
---    result, any type variables on the left hand side must occur on the right
---    hand side too.
---
 newtype Circuit a b =
   Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) )
 
 -- | Protocol-agnostic acknowledgement
 newtype Ack = Ack Bool
   deriving (Generic, C.NFDataX)
 
+-- | Acknowledge. Used in circuit-notation plugin to drive ignore components.
+instance Default Ack where
+  def = Ack True
+
 -- | Circuit protocol with /CSignal dom a/ in its forward direction, and
 -- /CSignal dom ()/ in its backward direction. Convenient for exposing
 -- protocol internals.
 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
@@ -171,7 +165,7 @@ class Protocol a where
 
   -- | Receiver to sender type family. See 'Circuit' for an explanation on the
   -- existence of 'Bwd'.
-  type Bwd (a :: Type) = (r :: Type) | r -> a
+  type Bwd (a :: Type)
 
 instance Protocol () where
   type Fwd () = ()
@@ -196,7 +190,7 @@ instance C.KnownNat n => Protocol (C.Vec n a) where
 -- 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 (Const () a)
+  type Bwd (CSignal dom a) = CSignal dom ()
 
 -- | Left-to-right circuit composition.
 --
@@ -231,22 +225,25 @@ infixr 1 |>
 class Protocol a => Backpressure a where
   -- | Interpret list of booleans as a list of acknowledgements at every cycle.
   -- Implementations don't have to account for finite lists.
-  boolsToBwd :: [Bool] -> Bwd a
+  boolsToBwd :: Proxy a -> [Bool] -> Bwd a
 
 instance Backpressure () where
-  boolsToBwd _ = ()
+  boolsToBwd _ _ = ()
 
 instance (Backpressure a, Backpressure b) => Backpressure (a, b) where
-  boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs)
+  boolsToBwd _ bs = (boolsToBwd (Proxy @a) bs, boolsToBwd (Proxy @b) bs)
 
 instance (Backpressure a, Backpressure b, Backpressure c) => Backpressure (a, b, c) where
-  boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs, boolsToBwd bs)
+  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 bs)
+  boolsToBwd _ bs = C.repeat (boolsToBwd (Proxy @a) bs)
 
 instance Backpressure (CSignal dom a) where
-  boolsToBwd _ = CSignal (pure (Const ()))
+  boolsToBwd _ _ = CSignal (pure ())
 
 -- | Right-to-left circuit composition.
 --
@@ -480,7 +477,7 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where
   sampleC conf (Circuit f) =
     let
       bools = replicate (resetCycles conf) False <> repeat True
-      (_, (fwd1, fwd2)) = f ((), (boolsToBwd bools, boolsToBwd bools))
+      (_, (fwd1, fwd2)) = f ((), (boolsToBwd (Proxy @a) bools, boolsToBwd (Proxy @b) bools))
     in
       ( sampleC conf (Circuit $ \_ -> ((), fwd1))
       , sampleC conf (Circuit $ \_ -> ((), fwd2)) )
@@ -517,7 +514,7 @@ instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where
   sampleC conf (Circuit f) =
     let
       bools = replicate (resetCycles conf) False <> repeat True
-      (_, fwds) = f ((), (C.repeat (boolsToBwd bools)))
+      (_, fwds) = f ((), (C.repeat (boolsToBwd (Proxy @a) bools)))
     in
       C.map (\fwd -> sampleC conf (Circuit $ \_ -> ((), fwd))) fwds