Panic: Unexpeceted numeric constraint #1693
Description
I'm feeling like this should work.
f : {n} [n] -> [n+1]
f x
| (fin n) => x # [False]
| (inf n) => x
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: pNegNumeric
Message: Unexpeceted numeric constraint:
?err
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.1.0.99-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/TypeCheck/Type.hs:967:9 in cryptol-3.1.0.99-inplace:Cryptol.TypeCheck.Type
%< ---------------------------------------------------
For context, I was trying to define Keccak's b2h function. Conceptually, it should work on both finite and infinite sequences.
/**
* The conversion function from hexadecimal strings to the SHA-3
* strings that they represent [FIPS-PUB-202 Section B.1].
*/
h2b : {n, m} (n <= 8 * m) => [m * 2 * 4] -> [n]
h2b H = take (join (map reverse Hs))
where
Hs = groupBy`{8} H : [m][8]
/**
* The conversion function from SHA-3 bit strings to the hexadecimal
* strings that represent them [FIPS-PUB-202 Section B.1].
*/
b2h : {n} (fin n) => [n] -> [n + n %^ 8]
b2h S = H
where
T = S # zero : [n + n %^ 8]
H = h2b`{m = n /^ (2 * 4)} T
vs. (roughly)
/**
* The conversion function from hexadecimal strings to the SHA-3
* strings that they represent [FIPS-PUB-202 Section B.1].
*/
h2b : {n, m} (n <= 8 * m) => [m * 2 * 4] -> [n]
h2b H = take (join (map reverse Hs))
where
Hs = groupBy`{8} H : [m][8]
/**
* The conversion function from SHA-3 bit strings to the hexadecimal
* strings that represent them [FIPS-PUB-202 Section B.1].
*/
b2h : {n} [n] -> [n + n %^ 8]
b2h S
| (fin n) => H
where
T = S # zero : [n + n %^ 8]
H = h2b`{m = n /^ (2 * 4)} T
| (inf n) => H
where
T = S : [n + n %^ 8]
H = h2b`{m = n /^ (2 * 4)} T