Bump typelit plugins

cabal.project

@@ -15,7 +15,7 @@ write-ghc-environment-files: always
 -- index state, to go along with the cabal.project.freeze file. update the index
 -- state by running `cabal update` twice and looking at the index state it
 -- displays to you (as the second update will be a no-op)
-index-state: 2025-07-19T09:09:36Z
+index-state: 2025-10-24T02:09:22Z
 
 -- For some reason the `clash-testsuite` executable fails to run without
 -- this, as it cannot find the related library...
@@ -59,6 +59,11 @@ optional-packages:
 allow-newer:
   brick:base,
   brick:deepseq,
+  -- >>> temporarily added for testing purposes
+  ghc-typelits-knownnat,
+  ghc-typelits-natnormalise,
+  ghc-typelits-extra,
+  -- <<<
   hashable,
   hedgehog-fakedata:hedgehog,
   rewrite-inspector:binary,

clash-ghc/clash-ghc.cabal

@@ -170,9 +170,9 @@ library
 
                       clash-lib                 == 1.9.0,
                       clash-prelude             == 1.9.0,
-                      ghc-typelits-extra        >= 0.3.2    && < 0.5,
-                      ghc-typelits-knownnat     >= 0.6      && < 0.8,
-                      ghc-typelits-natnormalise >= 0.6      && < 0.8,
+                      ghc-typelits-extra        >= 0.3.2    && < 0.6,
+                      ghc-typelits-knownnat     >= 0.6      && < 0.9,
+                      ghc-typelits-natnormalise >= 0.6      && < 0.10,
                       deepseq                   >= 1.3.0.2  && < 1.6,
                       time                      >= 1.4.0.1  && < 1.15,
                       ghc-boot                  >= 8.10.0   && < 9.11,

clash-lib-hedgehog/clash-lib-hedgehog.cabal

@@ -52,8 +52,8 @@ library
     containers                >= 0.5.0.0 && < 0.8,
     data-binary-ieee754       >= 0.4.4   && < 0.6,
     fakedata                  >= 1.0.2   && < 1.1,
-    ghc-typelits-knownnat     >= 0.7.2   && < 0.8,
-    ghc-typelits-natnormalise >= 0.7.2   && < 0.8,
+    ghc-typelits-knownnat     >= 0.7.2   && < 0.9,
+    ghc-typelits-natnormalise >= 0.7.2   && < 0.10,
     hedgehog-fakedata         >= 0.0.1.4 && < 0.1,
     mmorph                    >= 1.1.5   && < 1.3,
     mtl                       >= 2.1.2   && < 2.4,

clash-prelude-hedgehog/clash-prelude-hedgehog.cabal

@@ -50,7 +50,7 @@ library
 
   build-depends:
     ghc-typelits-knownnat     >= 0.7.2   && < 0.8,
-    ghc-typelits-natnormalise >= 0.7.2   && < 0.8,
+    ghc-typelits-natnormalise >= 0.7.2   && < 0.10,
     text                      >= 1.2.2   && < 2.2,
 
     clash-prelude             == 1.9.0,

clash-prelude/clash-prelude.cabal

@@ -335,9 +335,11 @@ Library
                       distributive              >= 0.1     && < 1.0,
                       extra                     >= 1.6.17  && < 1.9,
                       ghc-prim                  >= 0.5.1.0 && < 0.13,
-                      ghc-typelits-extra        >= 0.4     && < 0.5,
-                      ghc-typelits-knownnat     >= 0.7.2   && < 0.8,
-                      ghc-typelits-natnormalise >= 0.7.2   && < 0.8,
+  -- >>> lower bounds temporarily increased for testing purposes
+                      ghc-typelits-extra        >= 0.5.1   && < 0.6,
+                      ghc-typelits-knownnat     >= 0.8.2   && < 0.9,
+                      ghc-typelits-natnormalise >= 0.9.1   && < 0.10,
+  -- <<<
                       hashable                  >= 1.2.1.0  && < 1.6,
                       half                      >= 0.2.2.3 && < 1.0,
                       infinite-list           ^>= 0.1,

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

@@ -2654,17 +2654,43 @@ dtfold :: forall p k a . KnownNat k
 dtfold _ f g = go (SNat :: SNat k)
   where
     go :: forall n . SNat n -> Vec (2^n) a -> (p @@ n)
+#if __GLASGOW_HASKELL__ >= 904 && __GLASGOW_HASKELL__ < 912
+    go sn = case toUNat sn of
+      UZero -> \case
+        Cons x Nil -> f x
+        Cons x (Cons _ _) -> f x
+      USucc _ -> \case
+        xs@(Cons _ (Cons _ _)) ->
+          let sn' :: SNat (n - 1)
+              sn'       = sn `subSNat` d1
+              (xsL,xsR) = splitAt (pow2SNat sn') xs
+          in  g sn' (go sn' xsL) (go sn' xsR)
+        -- the remaining cases are impossible cases, but GHC cannot
+        -- automatically detect them to be inaccesible. We need to
+        -- give additional evidence for proving them to be absurd.
+        Cons _ Nil -> case p0 sn of Dict -> case p1 sn of {}
+         where
+          p0 :: 1 <= m => SNat m -> Dict (2 <= 2^((m-1)+1))
+          p0 = const Dict
+          p1 :: 1 <= m => SNat m -> Dict (2^m ~ 2^((m-1)+1))
+          p1 = const Dict
+        Nil -> case p sn of {}
+         where
+          p :: SNat m -> Dict (1 <= 2^m)
+          p = const Dict
+#else
     go _  (x `Cons` Nil) = f x
     go sn xs@(Cons _ (Cons _ _)) =
       let sn' :: SNat (n - 1)
           sn'       = sn `subSNat` d1
           (xsL,xsR) = splitAt (pow2SNat sn') xs
       in  g sn' (go sn' xsL) (go sn' xsR)
-#if !MIN_VERSION_base(4,16,0) || MIN_VERSION_base(4,17,0)
+#if __GLASGOW_HASKELL__ != 902
     go _  Nil =
       case (const Dict :: forall m. Proxy m -> Dict (1 <= 2 ^ m)) (Proxy @n) of
         {}
 #endif
+#endif
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE dtfold #-}
 {-# ANN dtfold hasBlackBox #-}