Traits cannot be imported by their original module when they are part of a bundle

[maximebuyse]

Example:

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

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

Open this code snippet in the playground

If we have include Playground.Bundle {t_A as t_A} in Playground.A.fst, F* complains with something like: Definition Playground.Bundle.__proj__Mkt_A__item__v_Self cannot be found`.

For now the solution to avoid this error is to remove this include but this doesn't work if the trait is used outside the bundle. This probably needs a fix in F*

[maximebuyse]

This problem is not limited to traits, the same happens with parametric structs (like struct Foo<const N: usize> {...}