clash-prelude-0.11.2 fails to build with ghc-typelits-natnormalise-0.5.5

[juhp]

When building for LTS-9:

src/CLaSH/Promoted/Nat.hs:371:20: error:
    • Could not deduce: ((2 * (n1 - 1)) + 1) ~ n
      from the context: (n + 1) ~ (2 * n1)
        bound by a pattern with constructor:
                   B0 :: forall (n :: Nat). BNat n -> BNat (2 * n),
                 in an equation for ‘predBNat’
        at src/CLaSH/Promoted/Nat.hs:371:11-14
      ‘n’ is a rigid type variable bound by
        the type signature for:
          predBNat :: forall (n :: Nat). BNat (n + 1) -> BNat n
        at src/CLaSH/Promoted/Nat.hs:367:13
      Expected type: BNat n
        Actual type: BNat ((2 * (n1 - 1)) + 1)
    • In the expression: B1 (go x)
      In an equation for ‘predBNat’:
          predBNat (B0 x)
            = B1 (go x)
            where
                go :: BNat m -> BNat (m - 1)
                go (B1 a)
                  = case stripZeros a of {
                      BT -> BT
                      a' -> B0 a' }
                go (B0 a) = B1 (go a)
                go BT = error "impossible: 0 ~ 0 - 1"
    • Relevant bindings include
        x :: BNat n1 (bound at src/CLaSH/Promoted/Nat.hs:371:14)
        predBNat :: BNat (n + 1) -> BNat n
          (bound at src/CLaSH/Promoted/Nat.hs:368:1)

[christiaanb]

Thanks for the report. That's a regression in ghc-typelits-natnormalise. I've uploaded version 0.5.6 of ghc-typelits-natnormalise to hackage which fixes the bug; with version 0.5.6, clash-prelude compiles again.