type mismatch in Cryptol.Eval.Concrete.toExpr

[msaaltink]

In this spec

type base t = { zero: t }

B: base Bool
B = { zero = False }

foo: {t,k} (fin k) => base t -> [k]t
foo B = repeat B.zero

bar: {t,k} (fin k, k>=1) => [k]t -> [k]t -> [k]t -> [k]t
bar p q m = p

baz: {k,t} (fin k, k >= 1) => [k]t -> [k]t -> [k]t
baz p q = q

property problem p =
  p != foo B ==> bar p (baz p 0x03) 0x03 == foo B

running :check problem crashes Cryptol:

Main> :check problem 
Using random testing.
problem 0x82 = False
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  c53f3cf1723235ad6b428e8b7be6b752823767a7
  Branch:    HEAD
  Location:  Cryptol.Eval.Concrete.toExpr
  Message:   type mismatch:
             [8]Cryptol::Bool
             130
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.9.0-IwOb2yTO6mD35k7fNx79Kk:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Eval/Concrete.hs:99:13 in cryptol-2.9.0-IwOb2yTO6mD35k7fNx79Kk:Cryptol.Eval.Concrete
%< --------------------------------------------------- 

[brianhuffman]

I think I found the problem: It's this line of code in function toExpr, which is supposed to produce a Cryptol AST corresponding to a value of the given type.

cryptol/src/Cryptol/Eval/Concrete.hs

Line 98 in 8f293e3

(TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do

I believe this example program leads to a situation where the value is a VWord, but the pattern TCon (TC TCBit) [] for the sequence element type doesn't match, because type Bit is hidden behind the type synonym Bool. (Note that changing Bool to Bit in the example program fixes the problem.)

To fix this, we should use the view patterns we have for types that use tNoUser to unfold type synonyms, following the advice in the comment above the function definition:

cryptol/src/Cryptol/Eval/Concrete.hs

Line 59 in 8f293e3

-- XXX: View patterns would probably clean up this definition a lot.

[brianhuffman]

I just want to point out that :exhaust problem triggers the same bug. This is important because I'd like to use this example as a regression test, but I can't use :check because it is non-deterministic and doesn't have reproducible output. So the regression test will use :exhaust instead.