From 6dd26ef7a662641795b33ae17c19a2c30132d765 Mon Sep 17 00:00:00 2001
From: Martijn Bastiaan <martijn@qbaylogic.com>
Date: Wed, 7 Jan 2026 09:54:20 +0100
Subject: [PATCH] Workaround ghc-typelits-extra#68

See https://github.com/clash-lang/ghc-typelits-extra/issues/68

This currently breaks compiles over at `clash-cores`. See
https://github.com/clash-lang/clash-cores/pull/56.
---
 clash-protocols/src/Data/Constraint/Nat/Extra.hs         | 9 +++++++--
 .../src/Protocols/PacketStream/Packetizers.hs            | 4 +++-
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/clash-protocols/src/Data/Constraint/Nat/Extra.hs b/clash-protocols/src/Data/Constraint/Nat/Extra.hs
index 52d99a2d..0f868c96 100644
--- a/clash-protocols/src/Data/Constraint/Nat/Extra.hs
+++ b/clash-protocols/src/Data/Constraint/Nat/Extra.hs
@@ -17,8 +17,13 @@ leModulusDivisor :: forall a b. (1 <= b) => Dict (Mod a b + 1 <= b)
 leModulusDivisor = unsafeCoerce (Dict :: Dict (0 <= 0))
 
 -- | if (1 <= a) and (1 <= b) then (1 <= DivRU a b)
-strictlyPositiveDivRu :: forall a b. (1 <= a, 1 <= b) => Dict (1 <= DivRU a b)
-strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict (0 <= 0))
+strictlyPositiveDivRu ::
+  forall a b.
+  (1 <= a, 1 <= b) =>
+  -- | XXX: The 'Constraint' equality is there to work around
+  -- issue github.com/clash-lang/ghc-typelits-extra/issues/68.
+  Dict ((1 <= DivRU a b) ~ (() :: Constraint))
+strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict (() ~ ()))
 
 -- | if (1 <= a) then (b <= ceil(b/a) * a)
 leTimesDivRu :: forall a b. (1 <= a) => Dict (b <= a * DivRU b a)
diff --git a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
index f04c35c7..799fdc60 100644
--- a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
@@ -358,7 +358,9 @@ packetizeFromDfT ::
   (KnownNat headerBytes) =>
   (KnownNat dataWidth) =>
   (1 <= dataWidth) =>
-  (1 <= headerBytes `DivRU` dataWidth) =>
+  -- \| XXX: The 'Constraint' equality is there to work around
+  -- issue github.com/clash-lang/ghc-typelits-extra/issues/68.
+  ((1 <= headerBytes `DivRU` dataWidth) ~ (() :: Constraint)) =>
   ((dataWidth + 1) <= headerBytes) =>
   -- | Mapping from `Df` input to output `_meta`
   (a -> metaOut) ->