Extraction error with `const` generics and hax attribute on a struct field

[ROMemories]

I'm hitting an error during F* extraction, when having a hax attribute on a struct field using a const generic.

Here is a reproducer (the actual attribute contents may not have much importance):

#[hax_lib::attributes]
struct Foo<const LEN: usize> {
    #[refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < indices.len(),
        || indices[i] as (usize) < 2
    )))]
    indices: [u8; LEN],
}

view in hax playground

The error message mentions error: [HAX0001] (FStar backend) something is not implemented yet. associated_refinement_in_type: zip two lists of different lenghts, but I can't clearly attribute this to the input Rust code.

If I move the const generic as a standalone const (e.g., const LEN: usize = 42;), F* extraction proceeds successfully. Likewise if I just comment out the hax attribute while keeping the const generic.

[W95Psp]

Thanks for your bug report! That's indeed a bug related to constants and struct refinements, I recall stumbling upon it quite some time ago.

From what I recall, the proc macro attributes sometimes remove const generics when it should not. I will try to investigate but I have no idea about when :/