Blackbox Error Caused by Simple map

[paddytheplaster]

Hi again,

Clash, version 1.0.1 (using clash-lib, version: 1.0.1) gives me the following error when synthesising (Clash -> vhdl):

Clash.Netlist.BlackBox(233): No blackbox found for: Data.Singletons.TypeLits.Internal.$fSingI->^@#@$_f.
Did you forget to include directories containing primitives? You can use '-i/my/prim/dir' to achieve this.

Compiling the following triggers the error. If I change the RHS of the equation to minBound, the error disappears.

f :: forall (n :: Nat) (d :: Nat)
  .  (KnownNat n,KnownNat d,1 <= n,1 <= d)
  => SNat n
  -> SNat d
  -> BitVector ((d*n)^2)
f _ _ = v2bv $ map (\_ -> low) (repeat False :: Vec ((d*n)^2) Bool)
{- f _ _ = minBound -- is grand -}

Any suggestions?

TIA for your help.

Regards,

Paddy

[paddytheplaster]

If I pass an 'SNat n' and 'SNat d' as extra parameters and compute the size of the 'Vec' and use 'indices', instaed of 'indicesI', the problem doesn't show any more.

Regards,

Paddy

[rowanG077]

I don't think it's caused by the map. I think it's triggering due to (d*n)^2 not being normalized.

Adding a constraint that computes the size of the Vec doesn't trigger the error while some other ways to write the same function triggers it.

import Clash.Prelude

triggered1 :: forall (n :: Nat) (d :: Nat)
  .  ( KnownNat n,KnownNat d,1 <= n,1 <= d)
  => SNat n
  -> SNat d
  -> BitVector ((d*n)^2)
triggered1 _ _ = v2bv $ map (\_ -> low) (repeat False :: Vec ((d*n)^2) Bool)

triggered2 :: forall (n :: Nat) (d :: Nat)
  .  ( KnownNat n,KnownNat d,1 <= n,1 <= d)
  => SNat n
  -> SNat d
  -> BitVector ((d*n)^2)
triggered2 _ _ = pack (repeat False :: Vec ((d*n)^2) Bool)

triggered3 :: forall (n :: Nat) (d :: Nat)
  .  ( KnownNat n,KnownNat d,1 <= n,1 <= d)
  => SNat n
  -> SNat d
  -> BitVector ((d*n)^2)
triggered3 _ _ = 0

notTriggered1
  :: forall (n :: Nat) (d :: Nat) (s :: Nat)
  .  ( KnownNat n,KnownNat d, KnownNat s, 1 <= n,1 <= d, s ~ ((d*n)^2))
  => SNat n
  -> SNat d
  -> BitVector s
notTriggered1 _ _ = v2bv $ map (\_ -> low) (repeat False :: Vec s Bool)

notTriggered2 :: forall (n :: Nat) (d :: Nat)
  .  ( KnownNat n,KnownNat d,1 <= n,1 <= d)
  => SNat n
  -> SNat d
  -> BitVector ((d*n)^2)
notTriggered2 _ _ = minBound

topEntity :: Signal System (BitVector 16)
topEntity = pure $ triggered3 (SNat @2) (SNat @2)

Compiling with -fclash-compile-ultra also fixes the issue for triggered1 and triggered2 cases but not for triggered3.

[paddytheplaster]

Thanks Rowan,

Nice analysis.

Is this '-fclash-compile-ultra' flasg documented anywhere?

Regards,

Paddy

[rowanG077]

It's not documented anywhere currently. I think #961 will document it. But be aware that this flag can increase the time to compile considerably.

[leonschoorl]

As @rowanG077 said: this is caused by the ^ in the length of the Vec.

Clash tries to evaluate the ^ with:

clash-compiler/clash-ghc/src-ghc/Clash/GHC/Evaluator.hs

Lines 1088 to 1092 in 9a57643

	-- XXX: Very fragile. /$s^_f/ is a specialized version of ^_f. That means that
	-- it is type applied to some specific type.
	"Data.Singletons.TypeLits.Internal.$s^_f"
	| Just (i,j) <- naturalLiterals args
	-> reduce (Literal (NaturalLiteral (i ^ j)))

And as the comment says this is "Very fragile", because we're matching on some generated name for some internal function.
And now it seems this name has changed, with ghc-8.6 it's called: $fSingI->^@#@$_f
And with ghc-8.8 it changed again to: %^_f