core::array::from_fn extracted with incorrect type parameter for closures returning references

[parrot7483]

When extracting Rust code that uses core::array::from_fn with a closure returning reference types (e.g., &[u8]), hax incorrectly generates the F* type parameter as a function type instead of the element type.

Expected F* extraction: Core_models.Array.from_fn #(t_Slice u8) N (fun i -> ...)
Actual F* extraction: Core_models.Array.from_fn #(usize -> t_Slice u8) N (fun i -> ...)

See this example:

const N: usize = 4;
const M: usize = 168;

fn main() {
    let data = [[0u8; M]; N];
    let slices: [&[u8]; N] = core::array::from_fn(|i| data[i].as_slice());
}

Open this code snippet in the playground

[maximebuyse]

Actually the F* extraction is a bit different: Core_models.Array.from_fn #(t_Slice u8) (mk_usize 4) #(usize -> t_Slice u8), the function type hint comes after N and the return type of the closure is still there before.

We made some changes recently so this is expected, but the lib has been modified accordingly. So if you use the same version for hax-lib and hax the extraction and what is expected by the definition of core::array::from_fn will match. The example you gave lax-checks on the playground thanks to that.