Panic: Unexpeceted numeric constraint

[weaversa]

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

[RyanGlScott]

This program contains a type error, as it is applying inf (of kind #) to an argument, which isn't well formed. A valid version of this program would be:

f : {n} [n] -> [n+1]
f x
  | (fin n)    => x # [False]
  | (n == inf) => x

I'm not yet clear on why Cryptol panics on the invalid inf n constraint instead of emitting an ordinary type error. Note that inf isn't essential to triggering the panic, as the following program also panics:

f : {n} [n] -> [n+1]
f x
  | (fin n) => x # [False]
  | (n) => x

[RyanGlScott]

Some investigation reveals that this is really the same issue as was reported in https://github.com/GaloisInc/cryptol/issues/1593, except that in this example, a guard contains a type error rather than a invalid (but otherwise well-typed) constraint. The fix proposed in https://github.com/GaloisInc/cryptol/issues/1593#issuecomment-1936031295 also fixes this issue, although I'm unclear if that is the right way to go about fixing this issue. (@yav, I'd be interested to hear your thoughts on this.)

[yav]

@RyanGlScott aborting if there are errors seems reasonable to me. I guess we could also add a haveErrors :: InferM Bool function and just skip the exhaustiveness checking instead of aborting entirely, but I am not sure if it is needed.

[weaversa]

In case you didn't notice, it may be worthwhile to change "Unexpeceted" -> "Unexpected".

[RyanGlScott]

Ah, quite right. I've added a separate commit to #1695 that fixes this typo.