get_impl_paths/recursion-checking does not handle Sync/Send inference

[tjhance]

Consider this variation of the recently added test test_recursion_through_sync_impl_is_checked from 4ab656f:

trait Tr {
    proof fn tr_g() {
    }
}

struct Xinner<T, S> {
    rc: std::rc::Rc<u64>,
    t: T,
    s: S,
}

struct X<T, S> {
    inner: Xinner<T, S>,
}

#[verifier::external]
unsafe impl<T: Sync + Tr, S: Sync> Sync for Xinner<T, S> {
}


trait Sr {
    proof fn f() { }
}

struct Y<R> {
    r: R,
}

impl<W: Sync> Sr for Y<W> {
    proof fn f() { }
}


struct A1 { }

struct B1 { }

impl Tr for A1 {
    proof fn tr_g() {
        test();
    }
}

proof fn test() {
    let r = Y::<X<A1, B1>>::f();
}

The cycle has the dependency Xinner<T, S>: Sync --> X<T, S>: Sync which is not covered by get_impl_paths

[tjhance]

this might be okay appealing to the coinductiveness of Send/Sync? I'm not sure.

[Chris-Hawblitzel]

Not all cycles are unsound. For example, cycles through exec functions are sound and we don't need to report them as errors (unless we deliberately want to prohibit non-terminating exec functions). Mainly, we just need to guarantee termination of spec and proof functions.