Respect VWord/VSeq invariants in parmap implementation

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