Respect VWord/VSeq invariants in parmap implementation (#1579)

Previously, `parmap` could incorrectly return a `VWord` when the element type
was not `Bit`, and it could also return a `VSeq` when the element type was
`Bit`. This changes the implementation of `parmap` to use the `mkSeq` smart
constructor, which properly chooses what sort of `GenValue` to return depending
on the element type.

Fixes #1578.

CHANGES.md

@@ -12,6 +12,8 @@
 * Fixed #1455, making anything in scope of the functor in scope at the REPL as
   well when an instantiation of the functor is loaded and focused,
   design choice (3) on the ticket.  In particular, the prelude will be in scope.
+* Fix #1578, which caused `parmap` to crash when evaluated on certain types of
+  sequences.
 
 
 # 3.0.0 -- 2023-06-26

src/Cryptol/Eval/Generic.hs

@@ -1877,22 +1877,23 @@ randomV sym ty seed =
 parmapV :: Backend sym => sym -> Prim sym
 parmapV sym =
   PTyPoly \_a ->
-  PTyPoly \_b ->
-  PFinPoly \_n ->
+  PTyPoly \b ->
+  PFinPoly \n ->
   PFun \f ->
   PFun \xs ->
   PPrim
     do f' <- fromVFun sym <$> f
        xs' <- xs
-       case xs' of
-          VWord n w ->
-            do let m = asBitsMap sym w
-               m' <- sparkParMap sym (\x -> f' (VBit <$> x)) n m
-               VWord n <$> (bitmapWordVal sym n (fromVBit <$> m'))
-          VSeq n m ->
-            VSeq n <$> sparkParMap sym f' n m
-
-          _ -> panic "parmapV" ["expected sequence!"]
+       m <-
+         case xs' of
+           VWord _n w ->
+             let m = asBitsMap sym w in
+             sparkParMap sym (\x -> f' (VBit <$> x)) n m
+           VSeq _n m ->
+             sparkParMap sym f' n m
+
+           _ -> panic "parmapV" ["expected finite sequence!"]
+       mkSeq sym (Nat n) b m
 
 
 sparkParMap ::

tests/issues/T1578.icry

@@ -0,0 +1,2 @@
+parmap (\_ -> True) [0, 1] > 0b00
+parmap (\_ -> ()) 0b00 == [(), ()]

tests/issues/T1578.icry.stdout

@@ -0,0 +1,3 @@
+Loading module Cryptol
+True
+True