Issue when using `testEquality`/`decideNat` in some contexts involving large `Nat`s

[diegodiv]

I faced an issue using testEquality with large (256 bits) Nats. I created a reproducer:

import Clash.Prelude hiding (SNat, Mod)
import Clash.Annotations.TH (makeTopEntity)

import Data.Type.Equality
import GHC.TypeLits (SNat)

type P = 2 ^ 256 - 2 ^ 224 + 2 ^ 192 + 2 ^ 96 - 1 -- any small-ish number would work (e.g. 300)

topEntity :: "hey" ::: Unsigned (CLog 2 P) -> "ho" ::: Index P
topEntity = f

f :: forall m. (KnownNat m, 1 <= m) => Unsigned (CLog 2 m) -> Index m
f =
 case testEquality (natSing :: SNat m) (natSing :: SNat P) of
  Just Refl -> g -- g @P would work
  Nothing   -> bitCoerce

g :: forall m. (KnownNat m, 1 <= m) => Unsigned (CLog 2 m) -> Index m
g =
  case testEquality (natSing :: SNat m) (natSing :: SNat P) of
    Just Refl -> h
    Nothing   -> bitCoerce

h :: forall m . (KnownNat m, 1 <= m) => Unsigned (CLog 2 m) -> Index m
h i = 1 + bitCoerce i

makeTopEntity 'topEntity

This snippet fails to synthesize with Clash.Netlist.BlackBox(343): No blackbox found for: GHC.Num.BigNat.bigNatEq#. Did you forget to include directories containing primitives? You can use '-i/my/prim/dir' to achieve this.

However, either having type P = 300 (e.g.) or replacing the call to g by g @P makes it synthesize - I assume that aggressively monomorphizing the code at call sites makes somehow testEquality (or its Core equivalent) disappear in the generated Core. Otherwise, if the Nat is small enough, it's treated as an Int which Clash can handle.