Missing type ascription in match scrutinee with array indexing

[ROMemories]

While I would expect it to, the following snippet does not typecheck:

const FOO_SIZE: usize = 5;

const FOO: [u8; FOO_SIZE] = [0, 0, 0, 0, 0];

#[hax_lib::requires(i < FOO_SIZE)]
fn foo(i: usize) {
    let _ = match FOO[i] {
        0xff => 42,
        _ => 41,
    };
}

view on playground

However, when replacing the match with an if, it does, as expected:

const FOO_SIZE: usize = 5;

const FOO: [u8; FOO_SIZE] = [0, 0, 0, 0, 0];

#[hax_lib::requires(i < FOO_SIZE)]
fn foo(i: usize) {
    let _ = if FOO[i] == 0xff {
        42
    } else {
        41
    };
}

view on playground

It seems that the array indexing in the first case is missing a <: u8 type ascription, which gets generated only in the if case.

Is this some specific interaction between the match and array indexing, or just the symptom of something else?

Credits go to @chrysn for finding this.

[franziskuskiefer]

This appears to be related to #1170.

[karthikbhargavan]

Thanks, this is a good catch. It is indeed a missing ascription which is confusing the typeclass resolution in F*.
The error message could also be better.

[maximebuyse]

The ascriptions we insert are in nested function calls (which is what makes it works in the if case, and in let bindings. We should add an ascription for match scrutinees.