Cyclic dependency with trait impl

[franziskuskiefer]

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

    impl<T: Encode> Encode for Option<T> {
        fn encode() {
            T::encode();
        }
    }

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

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

Open this code snippet in the playground

[W95Psp]

The F* produced here refers to Playground.Encoder.f_encode when calling T::encode(). Instead we need to refer to the bundle.

[karthikbhargavan]

I believe the issue is that the recursive bundle includes the trait and its implementation whereas it should not.

[github-actions]

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.

[franziskuskiefer]

@maximebuyse will investigate when #1199 is merged.

[maximebuyse]

This was fixed by #1199. The reproducer still does not lax-check though, but I documented the problem (which is different) in #1283 (comment).