SBV error: Prelude.foldr1: empty list

[msaaltink]

With these definitions:

choose: {n} (fin n) =>  [n] -> Maybe Integer
choose s = if s == zero then nothing else just 0

type Maybe a = (Bool, a)

nothing: {a} (Zero a) => Maybe a
nothing = (False, zero)

just: {a} a -> Maybe a
just x = (True, x)

member: {n, ix} (fin ix, fin n) => [ix] -> [n] -> Bit
member e s = (wide_s @ e) where
  wide_s = s # (zero:[2^^ix]) // so that too-large indexes are not in the set

property choose_just_member i s = (choose`{4} s == just i) ==>
     member (fromInteger`{[0]} i) s

the :prove command fails with

SBV error:
Prelude.foldr1: empty list

This seems to be related to the 0-bit integer value.

[brianhuffman]

Here's a minimized example:

property foo i (s : [1]) = s @ (fromInteger i : [0])

The fromInteger is essential to trigger the bug. This could probably be fixed either within SBV or on the Cryptol side. I think we just need to ensure that fromInteger at type [0] always returns a concrete (rather than symbolic) value.