"Other error: divide by zero" on input file

[kleinreact]

I get some

<no location info>: error:
    Other error:
    divide by zero

if I compile the code attached below with clash Top.hs --verilog -fclash-spec-limit=100. Simulation of the topEntity works fine. It also works, if I replace the 26 in topEntity by 25 or any smaller value. Unfortunately, I could not come up with a smaller reproducer so far.

Reproducer: Top.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}
module Top where

import Clash.Prelude

import Control.Monad
import Data.Constraint
import Data.Proxy
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeLits.KnownNat
import Unsafe.Coerce

topEntity ::
  HiddenClockResetEnable System =>
  Signal System Bool
topEntity
  = toSignal
  $ distributeStages (SNat @26) False (repeat @64 id)
  $ fromSignal
  $ pure True

-- | Evenly distributes @d@ registers between @n@ combinational
-- computations. The registers are all initialized with the provided
-- initial value. The introduced delay is tracked using 'DSignal'.
distributeStages ::
  forall (d :: Nat) (n :: Nat) (a :: Type).
  (KnownNat n, NFDataX a) =>
  SNat d ->
  a ->
  Vec n (a -> a) ->
  forall (dom :: Domain) (k :: Nat).
  (KnownDomain dom, HiddenClockResetEnable dom) =>
  DSignal dom k a ->
  DSignal dom (k + d) a
distributeStages d@SNat x = distributeStages' d0 d
 where
  distributeStages' ::
    forall (m :: Nat) (i :: Nat) (r :: Nat).
    (KnownNat m, NFDataX a) =>
    SNat i -> SNat r ->
    Vec m (a -> a) ->
    forall (dom :: Domain) (k :: Nat).
    (KnownDomain dom, HiddenClockResetEnable dom) =>
    DSignal dom k a ->
    DSignal dom (k + r) a
  distributeStages' i@SNat r@SNat cs = case toUNat @m SNat of
    UZero   -> delayedI x
    USucc _ -> case toUNat r of
      UZero   -> fmap (head cs)
               . distributeStages' (succSNat i) r (tail cs)
      USucc _ | Dict <- atMostOnePerStage @m @d @i
              , Dict <- leTrans @(DistributedStages m d i) @1 @(r - 1 + 1)
              -> delayedI @(DistributedStages m d i) x
               . fmap (head cs)
               . distributeStages'
                   (succSNat i)
                   (SNat @(r - DistributedStages m d i))
                   (tail cs)

  -- We never distribute more than one register per stage. The
  -- property trivially holds, as the only possible return values of
  -- 'DistributedStages' are zero or one.
  atMostOnePerStage :: forall x y z. Dict (DistributedStages x y z <= 1)
  atMostOnePerStage = unsafeCoerce (Dict :: Dict (0 <= 0))

  -- We don't use any dictionaries of 'Data.Constraint.Nat', as they suffer
  -- from https://github.com/clash-lang/clash-compiler/issues/2376
  leTrans :: forall x y z. (y <= z, x <= y) => Dict (x <= z)
  leTrans = unsafeCoerce (Dict :: Dict (0 <= 0))

-- | A type family for calculating the positions at which we need to
-- put a register in front, if we like to evenly distribute m
-- registers between a chain of n circuit blocks, where m < n.
-- Unfortunately, there are a lot of repetitions, as we don't 
-- have let bindings in type families. See the 'KnownNat3'
-- instance below for a more readable version.
type DistributedStages :: Nat -> Nat -> Nat -> Nat
type family DistributedStages n d i where
  DistributedStages _ 0 _ = 0
  DistributedStages n d i =
    If (n <=? d)
      1
      ( If (  1 <=? i
              -- ^ we don't place a register before the first element
           && If (i <=? Mod n (d + 1) * (Div n (d + 1) + 1))
                 -- ^ distribute the hangover blocks to the first r chains
                (Mod i (Div n (d + 1) + 1) == 0)
                (Mod
                   (i - Mod n (d + 1) * (Div n (d + 1) + 1))
                   (Div n (d + 1)) == 0)
           )
          1 0
      )

instance
  (KnownNat n, KnownNat m, KnownNat i) =>
  KnownNat3 $(nameToSymbol ''DistributedStages) n m i
 where
  natSing3 =
    let
      n = natToNatural @n
      m = natToNatural @m
      i = natToNatural @i
      r = f n m i
    in
      SNatKn r
   where
    f :: Nat -> Nat -> Nat -> Nat
    f n m i
      | n == 0 = 0
      | n <= m = 1
      | otherwise =
          let k = n `div` (m + 1)
              r = n `mod` (m + 1)
              b = (k + 1) * r
           in if 1 <= i &&
                   if i <= b
                   then mod i (k + 1) == 0
                   else mod (i - b) k == 0
              then 1
              else 0
  {-# INLINE natSing3 #-}

-- | Some quick test code for seeing the 'DistributedStages' type 
-- family in action. This is only for those who like to understand
-- the code. It is not required for reproducing the bug.
placeRegister :: Nat -> Nat -> IO ()
placeRegister n m = do
  print (k, r, b)
  putStrLn "---"
  forM_ chain $ \(i, c) -> do
    when c $ putStrLn "[R]"
    putStr " "
    print i
 where
  -- minimum size of chained blocks without a register in between
  k = n `div` (m + 1)
  -- number of hangover blocks
  r = n `mod` (m + 1)
  -- add-one-more range bound
  b = (k + 1) * r

  chain
    | m <= 0    = ( , False) <$> [0..n-1]
    | m >= n    = (0, False) : (( , True) <$> [1..n-1])
    | otherwise =
        [ (i, i > 0 && cond)
        | i <- [0..n-1]
        , let cond = if i <= b
                     then i `mod` (k + 1) == 0
                     else (i - b) `mod` k == 0
        ]

Also thanks to @leonschoorl for figuring out that there is no error when compiling Clash with GHC 9.10. This at least gives a workaround.