Tuple struct constructors are not always usable

[ROMemories]

It seems that tuple struct constructors are not usable in every context.

For instance, the following does not lax check:

struct Id(u8);

fn main() {
    let ids = [1u8].into_iter().map(Id);
}

view in hax playground

However, the following does:

struct Id(u8);

fn main() {
    let id = Id(1u8);
}

[W95Psp]

Thanks for your bug report! I need to investigate a bit, but this is definitely Id being imported incorrectly by the engine. In import_thir.ml, every identity is tagged with a kind, based on the context. Here, I suspect Id is seen as a function, whence it gets compiled to v_Id instead of Id.

It might be that we don't have enough context at THIR import: in this case, we might need to add more information and context in the frontend.