Import of name from bundle that doesn't exist

[maximebuyse]

This is a regression form #1199, here is a reproducer:

mod a {
    pub fn g(){super::b::h()}
    
    struct A();

    impl A {
        fn f() {
            struct Test(i32);
        }
    }
}
mod b {
    pub fn h(){super::a::g()}
}

Open this code snippet in the playground

F* laxing fails with: Definition Playground.Bundle.impl__f___0 cannot be found.
This is because of include Playground.Bundle {impl__f___0 as impl_A__f___0}
Here we have an alias for the ._0 accessor for the anonymous field in Test but Test is defined inside an impl methods which messes with the name.

[maximebuyse]

I think one way to solve that would be to completely remove aliases for _<n> accessors of tuple structs. It seems that this is ok and in a case like:

mod a {
    pub fn g(){super::b::h()}
    
    pub struct A(pub i32);

}
mod b {
    pub fn h(){super::a::g()}
}

fn f(x: a::A) -> i32 {
    x.0
}

Open this code snippet in the playground

Lax-checking still works without the include Playground.Bundle {_0 as _0} in Playground.A.fst.

@W95Psp Do you think this would be ok? And how can we identify a name that corresponds to one of these accessors?

[maximebuyse]

Other thing we should probably not produce aliases for: traits. Example:

mod encoder {
    trait Encode {
        fn encode();
    }

    pub fn foo(){
        super::user::something();
    }
}

mod user {
    pub fn something() {
        super::encoder::foo();
    }
}

Open this code snippet in the playground
Here we have include Playground.Bundle {t_Encode as t_Encode} which gives this laxing error: Definition Playground.Bundle.__proj__Mkt_Encode__item__v_Self cannot be found

[W95Psp]

I think that indeed not producing aliases for field names makes sense.
In dependencies.ml we can add another condition to the filter when we build up the aliases list, to know if a concrete ident points to a field, you can project its view (with https://hax.cryspen.com/engine/docs/hax-engine/Hax_engine/Concrete_ident/index.html#val-to_view), and then inspect the last segment of the relpath of the view.

However, for the traits, I think that's a problem in F*: currently, include ... {some_trait} detects that some_trait is a type definition and thus automatically includes all possible related names.
For now, we can filter them out, but we should file an issue on hax to fix it, and probably on F* as well (if we have a simple reproducer).