Type error in generated BPL

[msaaltink]

use prover::prover::{ensures, forall, requires};
use prover::vector_iter::{sum_range};


#[ext(pure)]
fun equal_range<T: copy+drop>(u: &vector<T>, v: &vector<T>, i:u64, j: u64): bool {
    forall!(|k| equal_in_range(u, v, i, j, *k))
}

#[ext(pure)]
fun equal_in_range<T: copy+drop>(u: &vector<T>, v: &vector<T>, i:u64, j: u64, k: u64): bool {
    k < i || k >= j || k >= u.length() || k >= v.length() || u[k] == v[k]
}

#[spec(prove, focus)]
fun sum_equal_test(u: &vector<u64>, v: &vector<u64>, i:u64, j: u64) {
    requires(i < u.length() && i <= v.length());
    requires(j < u.length() && j <= v.length());
    requires(equal_range(u, v, i, j));
    ensures(sum_range(u, i, j) == sum_range(v, i, j));
}

gives

~/bin/sui-prover 
✅ funs_abort_check
🔄 playground::sum_equal_test_Check
[internal] boogie exited with compilation errors:
output/playground::sum_equal_test_Check.bpl(5308,128): Error: invalid type for argument 4 in application of $0_playground_equal_in_range'u64'$pure: Vec int (expected: int)
output/playground::sum_equal_test_Check.bpl(5332,119): Error: invalid type for argument 4 in application of $0_playground_equal_in_range'u64'$pure: Vec int (expected: int)
2 type checking errors detected in output/playground::sum_equal_test_Check.bpl

Looking at the BPL, we have

// fun playgound::equal_range<u64> [baseline] at ./sources/playgound.move:481:1+132
function {:inline} $0_playgound_equal_range'u64'$pure(_$t0: Vec (int), _$t1: Vec (int), _$t2: int, _$t3: int) returns ($ret0: bool)
{
    (var $t5 := (forall x: Vec (int) :: $IsValid'vec'u64''(x) ==> $0_playgound_equal_in_range'u64'$pure(_$t0, _$t1, _$t2, _$t3, x));
    $t5)
}

with the definition

function {:inline} $0_playgound_equal_in_range'u64'$pure(_$t0: Vec (int), _$t1: Vec (int), _$t2: int, _$t3: int, _$t4: int) returns ($ret0: bool)
  { ... }

and a clear type mismatch. What happened?

[msaaltink]

I just tried making the definitions not generic, and get the same error. So that makes a simpler example.

#[ext(pure)]
fun equal_range(u: &vector<u64>, v: &vector<u64>, i:u64, j: u64): bool {
    forall!(|k| equal_in_range(u, v, i, j, *k))
}

#[ext(pure)]
fun equal_in_range(u: &vector<u64>, v: &vector<u64>, i:u64, j: u64, k: u64): bool {
    k < i || k >= j || k >= u.length() || k >= v.length() || u[k] == v[k]
}

[msaaltink]

However, if the parameter k is moved to the front of equal_in_range, the problem goes away.