diff --git a/clash-protocols/src/Data/Constraint/Nat/Extra.hs b/clash-protocols/src/Data/Constraint/Nat/Extra.hs
index 77ae41ea..9af80935 100644
--- a/clash-protocols/src/Data/Constraint/Nat/Extra.hs
+++ b/clash-protocols/src/Data/Constraint/Nat/Extra.hs
@@ -19,7 +19,7 @@ cancelMulDiv :: forall a b. (1 <= b) => Dict (DivRU (a * b) b ~ a)
 cancelMulDiv = unsafeCoerce (Dict :: Dict (0 ~ 0))
 
 -- | if (1 <= b) then (Mod a b + 1 <= b)
-leModulusDivisor :: forall a b. 1 <= b => Dict (Mod a b + 1 <= b)
+leModulusDivisor :: forall a b. (1 <= b) => Dict (Mod a b + 1 <= b)
 leModulusDivisor = unsafeCoerce (Dict :: Dict (0 <= 0))
 
 -- | if (a <= 0) then (a ~ 0)
diff --git a/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs
index 1c1ef3a2..b45530e2 100644
--- a/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs
@@ -19,10 +19,10 @@ import Protocols
 import qualified Protocols.Df as Df
 import Protocols.PacketStream.Base
 
+import Data.Constraint (Dict (Dict))
+import Data.Constraint.Nat.Extra (leModulusDivisor, timesDivRu)
 import Data.Data ((:~:) (Refl))
 import Data.Maybe
-import Data.Constraint (Dict(Dict))
-import Data.Constraint.Nat.Extra (timesDivRu, leModulusDivisor)
 
 defaultByte :: BitVector 8
 defaultByte = 0x00
diff --git a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
index 9b751231..5f25aad9 100644
--- a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
@@ -19,10 +19,10 @@ import qualified Protocols.Df as Df
 import Protocols.PacketStream.Base
 
 import Clash.Sized.Vector.Extra (takeLe)
+import Data.Constraint (Dict (Dict))
+import Data.Constraint.Nat.Extra (leModulusDivisor, leZeroIsZero, strictlyPositiveDivRu)
 import Data.Maybe
 import Data.Maybe.Extra
-import Data.Constraint.Nat.Extra (leModulusDivisor, strictlyPositiveDivRu, leZeroIsZero)
-import Data.Constraint (Dict(Dict))
 
 defaultByte :: BitVector 8
 defaultByte = 0x00
diff --git a/clash-protocols/tests/Tests/Haxioms.hs b/clash-protocols/tests/Tests/Haxioms.hs
index 5820d6bc..68188c61 100644
--- a/clash-protocols/tests/Tests/Haxioms.hs
+++ b/clash-protocols/tests/Tests/Haxioms.hs
@@ -2,8 +2,8 @@
 
 module Tests.Haxioms where
 
-import Prelude
 import Numeric.Natural
+import Prelude
 
 import Hedgehog
 import qualified Hedgehog.Gen as Gen
@@ -14,9 +14,10 @@ import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit))
 import Test.Tasty.Hedgehog.Extra (testProperty)
 import Test.Tasty.TH (testGroupGenerator)
 
--- | Generate a 'Natural' greater than or equal to /n/. Can generate 'Natural's
--- up to /n+1000/. This should be enough, given that naturals in this module are
--- used in proofs.
+{- | Generate a 'Natural' greater than or equal to /n/. Can generate 'Natural's
+up to /n+1000/. This should be enough, given that naturals in this module are
+used in proofs.
+-}
 genNatural :: Natural -> Gen Natural
 genNatural min_ = Gen.integral (Range.linear min_ (1000 + min_))
 
@@ -27,64 +28,64 @@ divRU dividend divider =
     (n, 0) -> n
     (n, _) -> n + 1
 
--- | Test whether the following equation holds:
---
---     DivRU (a * b) b ~ a
---
--- Given:
---
---     1 <= b
---
--- Tests: 'Data.Constraint.Nat.Extra.cancelMulDiv'.
---
+{- | Test whether the following equation holds:
+
+    DivRU (a * b) b ~ a
+
+Given:
+
+    1 <= b
+
+Tests: 'Data.Constraint.Nat.Extra.cancelMulDiv'.
+-}
 prop_cancelMulDiv :: Property
 prop_cancelMulDiv = property $ do
   a <- forAll (genNatural 0)
   b <- forAll (genNatural 1)
   divRU (a * b) b === a
 
--- | Test whether the following equation holds:
---
---      Mod a b + 1 <= b
---
--- Given:
---
---      1 <= b
---
--- Tests: 'Data.Constraint.Nat.Extra.leModulusDivisor'.
---
+{- | Test whether the following equation holds:
+
+     Mod a b + 1 <= b
+
+Given:
+
+     1 <= b
+
+Tests: 'Data.Constraint.Nat.Extra.leModulusDivisor'.
+-}
 prop_leModulusDivisor :: Property
 prop_leModulusDivisor = property $ do
   a <- forAll (genNatural 0)
   b <- forAll (genNatural 1)
   assert (a `mod` b + 1 <= b)
 
--- | Test whether the following equation holds:
---
---     1 <= DivRU a b
---
--- Given:
---
---     1 <= a, 1 <= b
---
--- Tests: 'Data.Constraint.Nat.Extra.strictlyPositiveDivRu'.
---
+{- | Test whether the following equation holds:
+
+    1 <= DivRU a b
+
+Given:
+
+    1 <= a, 1 <= b
+
+Tests: 'Data.Constraint.Nat.Extra.strictlyPositiveDivRu'.
+-}
 prop_strictlyPositiveDivRu :: Property
 prop_strictlyPositiveDivRu = property $ do
   a <- forAll (genNatural 1)
   b <- forAll (genNatural 1)
   assert (1 <= divRU a b)
 
--- | Test whether the following equation holds:
---
---      b <= Div (b + (a - 1)) a * a
---
--- Given:
---
---      1 <= a
---
--- Tests: 'Data.Constraint.Nat.Extra.timesDivRU'.
---
+{- | Test whether the following equation holds:
+
+     b <= Div (b + (a - 1)) a * a
+
+Given:
+
+     1 <= a
+
+Tests: 'Data.Constraint.Nat.Extra.timesDivRU'.
+-}
 prop_timesDivRU :: Property
 prop_timesDivRU = property $ do
   a <- forAll (genNatural 1)