Fix splitV when splitting empty sequence to type [inf][0]

Previously, `splitV` would assume that if you were splitting a value `val` into
something of type `[inf][each]`, then `val` must be a stream of type of `[inf *
each]` (i.e., of type `[inf]`). This is not true in the corner case where
`each` equals `0`, however. In that case, `val` is of type `[0]`, which is a
word, not a stream. As such, we need to ensure that we do not call `fromSeq` on
`val`, which crashes if `val` is not a stream or sequence.

Fixes #1749.

CHANGES.md

@@ -4,6 +4,9 @@
 
 ## Bug fixes
 
+* Fix a bug in which splitting a `[0]` value into type `[inf][0]` would panic.
+  ([#1749](https://github.com/GaloisInc/cryptol/issues/1749))
+
 ## New features
 
 # 3.2.0 -- 2024-08-20

src/Cryptol/Eval/Generic.hs

@@ -1079,14 +1079,27 @@ splitV sym parts each a val =
               lookupSeqMap xs (each * i + j)
 
     Inf
-      | isTBit a ->
+      -- The return type is [inf][each], (where each is non-zero) and `val` is
+      -- of type [inf * each], or [inf]. Therefore, `val` is a stream.
+      | isTBit a, each /= 0 ->
         do val' <- sDelay sym (fromSeq "splitV" =<< val)
            return $ VStream $ indexSeqMap $ \i ->
              VWord each <$> bitmapWordVal sym each (indexSeqMap $ \j ->
                let idx = i*each + toInteger j
                 in idx `seq` do
                        xs <- val'
                        fromVBit <$> lookupSeqMap xs idx)
+      -- The return type is [inf][0], and `val` is of type [inf * 0], or [0].
+      -- Therefore, `val` is a word. We need to special-case this, because the
+      -- case directly above this one will panic if `val` is not a stream due to
+      -- the use of `fromSeq` (#1749).
+      --
+      -- Because `val` is an empty sequence, there is no need to split it apart.
+      -- Instead, we can just return a stream with infinite copies of `val`.
+      | isTBit a, each == 0 ->
+        return $ VStream $ indexSeqMap $ \_i -> val
+      -- If `a` is not `Bit`, then `val` must be a sequence or a stream (and not
+      -- a word).
       | otherwise ->
         do val' <- sDelay sym (fromSeq "splitV" =<< val)
            return $ VStream $ indexSeqMap $ \i ->

tests/issues/issue1749.cry

@@ -0,0 +1,5 @@
+f : [0] -> [inf][0]
+f = split
+
+main : [0]
+main = (f []) @ 0

tests/issues/issue1749.icry

@@ -0,0 +1,2 @@
+:load issue1749.cry
+main

tests/issues/issue1749.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x0