Prelude.!!: index to large

[kleinreact]

The following

f :: forall n. SNat n -> Unsigned 4
f n@SNat = case compareSNat n (SNat @15) of
  SNatLE -> at @n @(16 - n - 1) SNat vec
  SNatGT -> 0
 where
  vec :: Vec 16 (Unsigned 4)
  vec = repeat 0

topEntity :: HiddenClockResetEnable System => Signal System (Unsigned 4)
topEntity = pure $ f d17

results in

<no location info>: error:
    Clash error call:
    Prelude.!!: index too large
    CallStack (from HasCallStack):
      error, called at libraries/ghc-internal/src/GHC/Internal/List.hs:1689:14 in ghc-internal:GHC.Internal.List
      tooLarge, called at libraries/ghc-internal/src/GHC/Internal/List.hs:1699:50 in ghc-internal:GHC.Internal.List
      !!, called at src-ghc/Clash/GHC/Evaluator/Primitive.hs:3833:61 in clash-ghc-1.9.0-inplace:Clash.GHC.Evaluator.Primitive

when compiling with --verilog.

[leonschoorl]

I don't understand how it got there, but it's calling whnf' on:

    splitAt @1 @(+ (- (- 16 17) 1) 1) @(Unsigned 4) (SNat @1 1)
      (Nil @0 @(Unsigned 4) _CO_)

which simplifies to

    splitAt @1 @(-1) @(Unsigned 4) (SNat @1 1)
      (Nil @0 @(Unsigned 4) _CO_)

Given

splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)

As the input Vec should be m+n long, and 1 + -1 = 0 that makes the Nil sort of type correct.
But it seems some transformations somewhere forgot the fact that Nats should always >= 0.

[leonschoorl]

That expression ^ is just the body of the first alternative of the case in f.

I would've expected clash would eliminate the case first, before evaluation the body of the unreachable alternative.

[christiaanb]

So here's what's going on:

1. The caseCon transformation does not reduce the following case-expression:

case Clash.Promoted.Nat.compareSNat[8214565720323788400][GlobalId]
       @17
       @15
       Clash.Promoted.Nat.Literals.d17[8214565720323788544][GlobalId]
       (Clash.Promoted.Nat.SNat[8214565720323789945]
          @15
          (GHC.Num.Natural.NS 15##)) of

Because the subject is neither a data-constructor nor a primitive (nor a global function which returns a "zero-number" type).

2. And the way the current transformation strategy works, is that Clash starts both transforming the subject and the alternatives of the case-expression

3. The compile-time evaluation rule for splitAt only looks at the first type argument, the m in

splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)

to determine how evaluation will proceed. When m is positive, it basically assumes that the Vec (m+n) a must be a Cons constructor, and tries to project out the head and the tail. This leads to the out-of-bounds error.

We should probably check whether the Vec (m+n) a is actually a Cons constructor, and return an error value when it's not.
Ultimately this error won't show up in the generated HDL, because on a second pass of the case-expression, the compareSNat d17 d15 will have reduced to an SNatGT constructor and the entire case-expression will then be eliminated by the caseCon transformation.