Add KnownNat constraint to BitPack

Eliminates the need to add `KnownNat (BitSize a)` in a lot of other
places.

CHANGELOG.md

@@ -22,6 +22,7 @@
   * Added `Clash.Class.AutoReg`. Improves the chances of synthesis tools inferring clock-gated registers, when used. See [#873](https://github.com/clash-lang/clash-compiler/pull/873).
   * `Clash.Magic.suffixNameP`, `Clash.Magic.suffixNameFromNatP`: enable prefixing of name suffixes
   * Added `Clash.Magic.noDeDup`: can be used to instruct Clash to /not/ share a function between multiple branches
+  * A `BitPack a` constraint now implies a `KnownNat (BitSize a)` constraint, so you won't have to add it manually anymore. See [#942](https://github.com/clash-lang/clash-compiler/pull/942).
 
 * New internal features:
   * [#918](https://github.com/clash-lang/clash-compiler/pull/935): Add X-Optimization to normalization passes

clash-prelude/clash-prelude.cabal

@@ -283,7 +283,7 @@ Library
                       deepseq                   >= 1.4.1.0 && < 1.5,
                       ghc-prim                  >= 0.5.1.0 && < 0.6,
                       ghc-typelits-extra        >= 0.3.1   && < 0.4,
-                      ghc-typelits-knownnat     >= 0.6     && < 0.8,
+                      ghc-typelits-knownnat     >= 0.7.1   && < 0.8,
                       ghc-typelits-natnormalise >= 0.6     && < 0.8,
                       hashable                  >= 1.2.1.0  && < 1.4,
                       half                      >= 0.2.2.3 && < 1.0,

clash-prelude/src/Clash/Class/BitPack.hs

@@ -71,7 +71,7 @@ import Clash.XException
 -}
 
 -- | Convert to and from a 'BitVector'
-class BitPack a where
+class KnownNat (BitSize a) => BitPack a where
   -- | Number of 'Clash.Sized.BitVector.Bit's needed to represents elements
   -- of type @a@
   --
@@ -281,7 +281,7 @@ instance BitPack () where
   pack   _ = minBound
   unpack _ = ()
 
-instance (KnownNat (BitSize a), KnownNat (BitSize b), BitPack a, BitPack b) =>
+instance (BitPack a, BitPack b) =>
     BitPack (a,b) where
   type BitSize (a,b) = BitSize a + BitSize b
   pack = let go (a,b) = pack a ++# pack b in packXWith go
@@ -388,23 +388,14 @@ instance GBitPack U1 where
 
 -- Instances derived using Generic
 instance ( BitPack a
-         , KnownNat (BitSize a)
          , BitPack b
-         , KnownNat (BitSize b)
          ) => BitPack (Either a b)
 
-instance ( BitPack a
-         , KnownNat (BitSize a)
-         ) => BitPack (Maybe a)
+instance BitPack a => BitPack (Maybe a)
 
 #if MIN_VERSION_base(4,12,0)
-instance ( BitPack a
-         , KnownNat (BitSize a)
-         ) => BitPack (Complex a)
-
-instance ( BitPack a
-         , KnownNat (BitSize a)
-         ) => BitPack (Down a)
+instance BitPack a => BitPack (Complex a)
+instance BitPack a => BitPack (Down a)
 #endif
 
 -- | Zero-extend a 'Bool'ean value to a 'BitVector' of the appropriate size.

clash-prelude/src/Clash/Examples.hs

@@ -157,10 +157,7 @@ oneHotCounter enable = s
     s = register 1 (mux enable (rotateL <$> s <*> 1) s)
 
 crcT
-  :: ( Bits a
-     , KnownNat (BitSize a)
-     , BitPack a
-     )
+  :: (Bits a, BitPack a)
   => a
   -> Bit
   -> a

clash-prelude/src/Clash/Prelude/BitIndex.hs

@@ -42,7 +42,7 @@ import Clash.Sized.Internal.BitVector (BitVector, Bit, index#, lsb#, msb#,
 -- >>> (7 :: Unsigned 6) ! 6
 -- *** Exception: (!): 6 is out of range [5..0]
 -- ...
-(!) :: (BitPack a, KnownNat (BitSize a), Enum i) => a -> i -> Bit
+(!) :: (BitPack a, Enum i) => a -> i -> Bit
 (!) v i = index# (pack v) (fromEnum i)
 
 {-# INLINE slice #-}
@@ -96,8 +96,7 @@ split v = split# (pack v)
 -- >>> replaceBit 6 0 (-5 :: Signed 6)
 -- *** Exception: replaceBit: 6 is out of range [5..0]
 -- ...
-replaceBit :: (BitPack a, KnownNat (BitSize a), Enum i) => i -> Bit -> a
-           -> a
+replaceBit :: (BitPack a, Enum i) => i -> Bit -> a -> a
 replaceBit i b v = unpack (replaceBit# (pack v) (fromEnum i) b)
 
 {-# INLINE setSlice #-}
@@ -134,7 +133,7 @@ setSlice m n w v = unpack (setSlice# (pack v) m n w)
 -- 00_0100
 -- >>> msb (4 :: Signed 6)
 -- 0
-msb :: (BitPack a, KnownNat (BitSize a)) => a -> Bit
+msb :: BitPack a => a -> Bit
 msb v = msb# (pack v)
 
 {-# INLINE lsb #-}

clash-prelude/src/Clash/Prelude/BitReduction.hs

@@ -13,8 +13,6 @@ Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 
 module Clash.Prelude.BitReduction where
 
-import GHC.TypeLits                   (KnownNat)
-
 import Clash.Class.BitPack            (BitPack (..))
 import Clash.Sized.Internal.BitVector (Bit, reduceAnd#, reduceOr#, reduceXor#)
 
@@ -39,7 +37,7 @@ import Clash.Sized.Internal.BitVector (Bit, reduceAnd#, reduceOr#, reduceXor#)
 --
 -- >>> reduceAnd (0 :: Unsigned 0)
 -- 1
-reduceAnd :: (BitPack a, KnownNat (BitSize a)) => a -> Bit
+reduceAnd :: BitPack a => a -> Bit
 reduceAnd v = reduceAnd# (pack v)
 
 {-# INLINE reduceOr #-}
@@ -58,7 +56,7 @@ reduceAnd v = reduceAnd# (pack v)
 --
 -- >>> reduceOr (0 :: Unsigned 0)
 -- 0
-reduceOr :: (BitPack a, KnownNat (BitSize a)) => a -> Bit
+reduceOr :: BitPack a => a -> Bit
 reduceOr v = reduceOr# (pack v)
 
 {-# INLINE reduceXor #-}
@@ -81,5 +79,5 @@ reduceOr v = reduceOr# (pack v)
 --
 -- >>> reduceXor (0 :: Unsigned 0)
 -- 0
-reduceXor :: (BitPack a, KnownNat (BitSize a)) => a -> Bit
+reduceXor :: BitPack a => a -> Bit
 reduceXor v = reduceXor# (pack v)

clash-prelude/src/Clash/Signal/BiSignal.hs

@@ -212,7 +212,6 @@ readFromBiSignal# (BiSignalIn ds s) =
 -- | Read the value from an __inout__ port
 readFromBiSignal
   :: ( HasCallStack
-     , KnownNat (BitSize a)
      , BitPack a)
   => BiSignalIn ds d (BitSize a)
   -- ^ A 'BiSignalIn' with a number of bits needed to represent /a/

clash-prelude/src/Clash/Signal/Trace.hs

@@ -147,7 +147,6 @@ traceMap# = unsafePerformIO (newIORef Map.empty)
 
 mkTrace
   :: HasCallStack
-  => KnownNat (BitSize a)
   => BitPack a
   => NFDataX a
   => Signal dom a
@@ -160,8 +159,7 @@ mkTrace signal = sample (unsafeToTup . pack <$> signal)
 -- was previously registered.
 traceSignal#
   :: forall dom a
-   . ( KnownNat (BitSize a)
-     , BitPack a
+   . ( BitPack a
      , NFDataX a
      , Typeable a )
   => IORef TraceMap
@@ -195,8 +193,7 @@ traceSignal# traceMap period traceName signal =
 -- an error.
 traceVecSignal#
   :: forall dom n a
-   . ( KnownNat (BitSize a)
-     , KnownNat n
+   . ( KnownNat n
      , BitPack a
      , NFDataX a
      , Typeable a )
@@ -226,7 +223,6 @@ traceVecSignal# traceMap period vecTraceName (unbundle -> vecSignal) =
 traceSignal
   :: forall dom  a
    . ( KnownDomain dom
-     , KnownNat (BitSize a)
      , BitPack a
      , NFDataX a
      , Typeable a )
@@ -250,8 +246,7 @@ traceSignal traceName signal =
 -- multiple clocks. Use 'traceSignal' when working with circuits that have
 -- multiple clocks.
 traceSignal1
-  :: ( KnownNat (BitSize a)
-     , BitPack a
+  :: ( BitPack a
      , NFDataX a
      , Typeable a )
   => String
@@ -273,7 +268,6 @@ traceSignal1 traceName signal =
 traceVecSignal
   :: forall dom a  n
    . ( KnownDomain dom
-     , KnownNat (BitSize a)
      , KnownNat n
      , BitPack a
      , NFDataX a
@@ -299,8 +293,7 @@ traceVecSignal traceName signal =
 -- multiple clocks. Use 'traceSignal' when working with circuits that have
 -- multiple clocks.
 traceVecSignal1
-  :: ( KnownNat (BitSize a)
-     , KnownNat n
+  :: ( KnownNat n
      , BitPack a
      , NFDataX a
      , Typeable a )

clash-prelude/src/Clash/Sized/Fixed.hs

@@ -39,6 +39,7 @@ BEWARE: rounding by truncation introduces a sign bias!
 
 {-# LANGUAGE Trustworthy #-}
 
+{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
 
@@ -437,7 +438,6 @@ type NumFixedC rep int frac
               (int + ((int + frac) + frac))
     , BitPack (rep ((int + int) + (frac + frac)))
     , Bits    (rep ((int + int) + (frac + frac)))
-    , KnownNat (BitSize (rep (int + frac)))
     , BitPack (rep (int + frac))
     , Enum    (rep (int + frac))
     , Bits    (rep (int + frac))

clash-prelude/src/Clash/Sized/RTree.hs

@@ -201,7 +201,7 @@ instance KnownNat d => Traversable (RTree d) where
                       (fmap LR . f)
                       (const (liftA2 BR))
 
-instance (KnownNat d, KnownNat (BitSize a), BitPack a) =>
+instance (KnownNat d, BitPack a) =>
   BitPack (RTree d a) where
   type BitSize (RTree d a) = (2^d) * (BitSize a)
   pack   = packXWith (pack . t2v)

clash-prelude/src/Clash/Sized/Vector.hs

@@ -2183,7 +2183,7 @@ smap f xs = reverse
                   Nil (reverse xs)
 {-# INLINE smap #-}
 
-instance (KnownNat n, KnownNat (BitSize a), BitPack a) => BitPack (Vec n a) where
+instance (KnownNat n, BitPack a) => BitPack (Vec n a) where
   type BitSize (Vec n a) = n * (BitSize a)
   pack   = packXWith (concatBitVector# . map pack)
   unpack = map unpack . unconcatBitVector#

nix/nixpkgs.nix

@@ -12,9 +12,8 @@ let
       overrides = self: super: {
         # External overrides
 
-        # Example:
-        # ghc-typelits-extra =
-        #  self.callCabal2nix "ghc-typelits-extra" sources.ghc-typelits-extra {};
+        ghc-typelits-knownnat =
+         self.callCabal2nix "ghc-typelits-knownnat" sources.ghc-typelits-knownnat {};
 
         # Internal overrides
         clash-lib = import ../clash-lib { inherit nixpkgs; };

nix/sources.json

@@ -34,5 +34,17 @@
         "type": "tarball",
         "url": "https://github.com/NixOS/nixpkgs-channels/archive/d5291756487d70bc336e33512a9baf9fa1788faf.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+    },
+    "ghc-typelits-knownnat": {
+        "branch": "master",
+        "description": "Derive KnownNat constraints from other KnownNat constraints",
+        "homepage": null,
+        "owner": "clash-lang",
+        "repo": "ghc-typelits-knownnat",
+        "rev": "cc73e761086e2d48acdf134b06ad3af47e115166",
+        "sha256": "151pd1bi9ynln2dm1rijz7cjp4f6jlrmcj6s6kwvgjl22rqb9b2h",
+        "type": "tarball",
+        "url": "https://github.com/clash-lang/ghc-typelits-knownnat/archive/cc73e761086e2d48acdf134b06ad3af47e115166.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
     }
 }

stack.yaml

@@ -9,4 +9,5 @@ packages:
 
 extra-deps:
 - ./clash-cosim
+- ghc-typelits-knownnat-0.7.1@sha256:52a647119137e572a957b62fd7a747448670c8f91138c26c48e1828a6ca7b6da,4708
 

tests/shouldwork/AutoReg/AutoReg.hs

@@ -22,25 +22,21 @@ import System.FilePath ((</>), takeDirectory)
 
 #ifndef OUTPUTTEST
 data Tup2 a b = MkTup2 { getA :: a, getB :: b } deriving (Generic,NFDataX)
-instance (BitPack a,BitPack b, KnownNat (BitSize a),KnownNat (BitSize b)) => BitPack (Tup2 a b)
+instance (BitPack a,BitPack b) => BitPack (Tup2 a b)
 deriveAutoReg ''Tup2
 
 
 data Tup3 a b c = MkTup3 { fieldA :: a, fieldB :: b, fieldC :: c } deriving (Generic,NFDataX)
-instance
-  ( BitPack a,BitPack b,BitPack c
-  , KnownNat (BitSize a), KnownNat (BitSize b), KnownNat (BitSize c)
-  )
-    => BitPack (Tup3 a b c)
+instance (BitPack a, BitPack b, BitPack c) => BitPack (Tup3 a b c)
 deriveAutoReg ''Tup3
 
 
 newtype OtherPair a b = OtherPair (Tup2 a b) deriving (Generic,NFDataX)
-instance (BitPack a,BitPack b, KnownNat (BitSize a),KnownNat (BitSize b)) => BitPack (OtherPair a b)
+instance (BitPack a, BitPack b) => BitPack (OtherPair a b)
 deriveAutoReg ''OtherPair
 
 data Tup2_ a b c = MkTup2_ a b deriving (Generic,NFDataX)
-instance (BitPack a,BitPack b, KnownNat (BitSize a),KnownNat (BitSize b)) => BitPack (Tup2_ a b c)
+instance (BitPack a, BitPack b) => BitPack (Tup2_ a b c)
 deriveAutoReg ''Tup2_
 -- NOTE: For some reason this deriveAutoReg ''Tup2_ creates invalid code when
 -- run by runghc-8.4.4 for the output test. (newer versions are ok)
@@ -50,15 +46,15 @@ data Concrete = BoolAndInt Bool Int8 deriving (Generic,NFDataX,BitPack)
 deriveAutoReg ''Concrete
 
 data InfixDataCon a b = a :-.- b deriving (Generic,NFDataX)
-instance (BitPack a,BitPack b,KnownNat (BitSize a),KnownNat (BitSize b)) => BitPack (InfixDataCon a b)
+instance (BitPack a, BitPack b) => BitPack (InfixDataCon a b)
 deriveAutoReg ''InfixDataCon
 
 
 test
   :: forall a dom n rest
    . ( HiddenClockResetEnable dom
      , AutoReg a, BitPack a
-     , KnownNat (BitSize a), KnownNat n, KnownNat rest
+     , KnownNat n, KnownNat rest
      , rest ~ (n-(BitSize a))
      )
   => Signal dom (BitVector n) -> Signal dom a

tests/shouldwork/BitVector/GenericBitPackTypes.hs

@@ -13,11 +13,7 @@ data FooProduct a b
   = FooProduct a b
     deriving Generic
 
-instance ( BitPack a
-         , BitPack b
-         , KnownNat (BitSize a)
-         , KnownNat (BitSize b)
-         ) => BitPack (FooProduct a b)
+instance (BitPack a, BitPack b) => BitPack (FooProduct a b)
 
 
 -- | Sum type
@@ -37,11 +33,7 @@ data FooSP1 a b
   | FooSP1_BA b a
     deriving (Generic)
 
-instance ( BitPack a
-         , BitPack b
-         , KnownNat (BitSize a)
-         , KnownNat (BitSize b)
-         ) => BitPack (FooSP1 a b)
+instance (BitPack a, BitPack b) => BitPack (FooSP1 a b)
 --
 -- | Foo sum-of-products non-aligned
 data FooSP2 a b
@@ -51,11 +43,7 @@ data FooSP2 a b
     deriving (Generic)
 
 
-instance ( BitPack a
-         , BitPack b
-         , KnownNat (BitSize a)
-         , KnownNat (BitSize b)
-         ) => BitPack (FooSP2 a b)
+instance (BitPack a, BitPack b) => BitPack (FooSP2 a b)
 
 -- Testsuite data (in separate module to circumvent TH stage restrictions):
 type U1 = Unsigned 3

tests/shouldwork/Numbers/NumConstantFolding_1.hs

@@ -147,7 +147,7 @@ cSaturatingNum = (r1a,r1b,r1c,r1d, r2a,r2b,r2c,r2d, r3a,r3b,r3c,r3d)
     r2d = satSub @n SatSymmetric (lit 22242) (lit 22243)
     r3d = satMul @n SatSymmetric (lit 22244) (lit 22245)
 
-cBitPack :: forall n. (Num n, BitPack n, KnownNat (BitSize n)) => _
+cBitPack :: forall n. (Num n, BitPack n) => _
 cBitPack = (r1,r2)
   where
     r1 = pack @n (lit 22250) + (lit 1000)
@@ -184,7 +184,7 @@ csGenericHaskell
     , cFiniteBits @n
     )
 
-csClashSpecific :: forall n. (Num n, BitPack n, KnownNat (BitSize n), ExtendingNum n n, SaturatingNum n) => _
+csClashSpecific :: forall n. (Num n, BitPack n, ExtendingNum n n, SaturatingNum n) => _
 csClashSpecific = (cBitPack @n, cExtendingNum @n @n, cSaturatingNum @n)