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

[maximebuyse]

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

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

struct B(u8);

impl a::A for B {}

Open this code snippet in the playground

Currently this doesn't lax-check because a::A is not exported outside module a.

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> {...}

[franziskuskiefer]

@maximebuyse please improve the example to actually use the trait.

[maximebuyse]

@maximebuyse please improve the example to actually use the trait.

Done

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

[W95Psp]

Still a problem

[maximebuyse]

This seems to be fixed in f*, I think we can have the include again for traits 🥳