Complie Error: int(0) is not a subtype of int('n)

[KotorinMinami]

I've got this function. It takes a vector and grabs four consecutive bits from it, joining them up.

val from_vector : forall 'n 'm 'p, 'n > 0 & 'm > 0 & 'p >= 0 & 4 * 'p + 3 < 'n . (vector('n, bits('m)), int('p)) -> bits(4 * 'm)
function from_vector(v, i) = v[4 * i + 3] @ v[4 * i + 2] @ v[4 * i + 1] @ v[4 * i]

I need an enum to define how we get to the coordinates of the bits in the vector – we're calling them ORIGIN and ZERO.

enum index_state = {
    ORIGIN,
    ZERO,
}

The problem is, when I use a function to return the coordinates, if I use int as the return type,

val index_state_to_index : (index_state, int) -> int
function index_state_to_index(s, i) = match s {
    ORIGIN => i,
    ZERO => 0,
}

I get one error.

Type error:
test.sail:27.16-72:
27 |    let value = from_vector(vectors, index_state_to_index(get_state, 0));
   |                ^------------------------------------------------------^
   | Could not resolve quantifiers for from_vector
   | * (4 > 0 & (8 > 0 & ('ex286# >= 0 & ((4 * 'ex286#) + 3) < 4)))

If I use int('n) as the return type,

val index_state_to_index : forall 'n, 'n >= 0 . (index_state, int('n)) -> int('n)
function index_state_to_index(s, i) = match s {
    ORIGIN => i,
    ZERO => 0,
}

I get a different error.

Type error:
test1.sail:21.12-13:
21 |    ZERO => 0,
   |            ^
   | int(0) is not a subtype of int('n)
   | as 0 == 'n could not be proven

So, what's the deal with this forall? Why's it happening, and how do I get it to behave itself?

Here is the whole file:

default Order dec

$include <smt.sail>
$include <option.sail>
$include <arith.sail>
$include <string.sail>
$include <mapping.sail>
$include <vector_dec.sail>

val from_vector : forall 'n 'm 'p, 'n > 0 & 'm > 0 & 'p >= 0 & 4 * 'p + 3 < 'n . (vector('n, bits('m)), int('p)) -> bits(4 * 'm)
function from_vector(v, i) = v[4 * i + 3] @ v[4 * i + 2] @ v[4 * i + 1] @ v[4 * i]

enum index_state = {
    ORIGIN,
    ZERO,
}

val index_state_to_index : forall 'n, 'n >= 0 . (index_state, int('n)) -> int('n)
function index_state_to_index(s, i) = match s {
    ORIGIN => i,
    ZERO => 0,
}

function main() : unit -> unit = {
    let get_state : index_state = ORIGIN;
    let vectors : vector(4, bits(8)) = vector_init(0b00000000000000000000000000000000);
    let value = from_vector(vectors, index_state_to_index(get_state, 0));
}

[Alasdair]

Try the following changing the return type of index_state_to_index into range(0, 'n):

default Order dec

$include <smt.sail>
$include <option.sail>
$include <arith.sail>
$include <string.sail>
$include <mapping.sail>
$include <vector_dec.sail>

val from_vector : forall 'n 'm 'p, 'n > 0 & 'm > 0 & 'p >= 0 & 4 * 'p + 3 < 'n . (vector('n, bits('m)), int('p)) -> bits(4 * 'm)
function from_vector(v, i) = v[4 * i + 3] @ v[4 * i + 2] @ v[4 * i + 1] @ v[4 * i]

enum index_state = {
    ORIGIN,
    ZERO,
}

val index_state_to_index : forall 'n, 'n >= 0 . (index_state, int('n)) -> range(0, 'n)
function index_state_to_index(s, i) = match s {
    ORIGIN => i,
    ZERO => 0,
}

function main() : unit -> unit = {
    let get_state : index_state = ORIGIN;
    let vectors : vector(4, bits(8)) = vector_init(0b0000_0000);
    let value = from_vector(vectors, index_state_to_index(get_state, 0));
}

The reason (index_state, int) -> int doesn't work is the return type int is too weak to satisfy the constraint on from_vector, as it could be any integer including one that is outside the bounds needed to index v.

On the other hand, (index_state, int('n)) -> int('n) is too strong to type the index_state_to_index function, as it is saying that the return type is the same number as the second argument always, when it can be 0 in the ZERO case for any value given as the second argument.

range(0, 'n) is probably the simplest type that works, but you could be even more precise and write something like {'m, 'n == m | 'm == 0. int('m)}, to precisely capture an integer that is either 'n or 0.