Use of parmap results in "not a word" error

[jpziegler]

I was trying out the experimental parmap function in a nightly Cryptol Docker image in the context of some recreational mathematics. Gist here:
https://gist.github.com/jpziegler/a3f0e8867edf92727dbd1451e4513d0e

Note that on line 31 I have replaced map (which works fine) with parmap.
https://gist.github.com/jpziegler/a3f0e8867edf92727dbd1451e4513d0e#file-ramsey_bug-cry-L31

The following invocation demonstrates the crash. However, most any invocation of the R function exhibits this behavior.

$ cryptol ramsey_bug.cry -c crash 
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  [Eval] fromVWord
  Message:   not a word
             cmpValue
             seq:93
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.0.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-3.0.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Value.hs:388:23 in cryptol-3.0.0.99-inplace:Cryptol.Eval.Value
%< ---------------------------------------------------

[RyanGlScott]

A smaller example of the issue:

crash = parmap (\_ -> True) [0, 1] > 0b00

$ cabal run exe:cryptol -- Bug.cry -c crash
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  8bc638e143f67fe24c924c06175241a3f0511eb7
  Branch:    master
  Location:  [Eval] fromVWord
  Message:   not a word
             cmpValue
             seq:2
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.0.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-3.0.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Value.hs:388:23 in cryptol-3.0.0.99-inplace:Cryptol.Eval.Value
%< ---------------------------------------------------

This another instance of Cryptol improperly upholding the invariant that all finite sequences of Bits should be represented as VWords. (See also #1437.) In the code that implements parmap, we see this:

cryptol/src/Cryptol/Eval/Generic.hs

Lines 1878 to 1893 in 8bc638e

	parmapV sym =
	PTyPoly \_a ->
	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

This code assumes that if parmap's sequence argument is a VSeq, then the output sequence will also be a VSeq. But this isn't the case when the output type _b is Bit, as in the example above. In that case, then the output sequence must be a VWord, not a VSeq. This means that the following patch suffices to fix the issue:

diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 461c4bc2..001a46da 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -1877,7 +1877,7 @@ randomV sym ty seed =
 parmapV :: Backend sym => sym -> Prim sym
 parmapV sym =
   PTyPoly \_a ->
-  PTyPoly \_b ->
+  PTyPoly \b ->
   PFinPoly \_n ->
   PFun \f ->
   PFun \xs ->
@@ -1889,8 +1889,9 @@ parmapV sym =
             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
+          VSeq n m -> do
+            m' <- sparkParMap sym f' n m
+            mkSeq sym (Nat n) b m'
 
           _ -> panic "parmapV" ["expected sequence!"]

The VWord case is similarly suspicious, as parmap can map a VWord to a VSeq if b is not equal to Bit.