Coinductive auto-trait treatment is questionably sound

I had a great chat with @lcnr today and learned some new, fascinating things about our trait system. :)
In particular, I learned that we consider this impl as legitimate for coninductive reasoning:

unsafe impl Sync for MyCell where MyCell: Sync {}

This has the concerning consequence that MyCell becomes Sync. This is IMO a huge problem, since it entirely breaks every model I have seen of what the safety obligation attached with this unsafe impl should be. In my view (and, AFAIK, in the view of everyone working on verification for unsafe Rust), the above impl is obviously sound, as explained by a comment like

// SAFETY: It is obviously true that `MyCell: Sync` implies `MyCell: Sync`.

However, that impl is also the only piece of unsafe in this example. That means one of the following is true:

• What the trait solver does here is unsound.
• The safety obligation for unsafe impl Trait for Type where <bound> is different from "<bound> implies that Type satisfies the safety contract associated with Trait". However, what else could the safety obligation possibly be...?

IMO, this is a trait solver bug. The trait solver should only be allowed to apply coinductive reasoning when some form of "progress" has been made, i.e. when the obligation it is proving has become "smaller" by unfolding a recursive type at least once. However, given that there currently isn't any reasoning of this sort, this may be quite hard to actually achieve. Unfortunately, I don't know a plausible alternative -- if the trait solver is allowed to do corecursion with all (auto trait) impls, then what do I have to prove for my own unsafe impls to ensure that nonsense like this does not happen? It's kind of obvious in this example, but we'd need a general principle that guarantees that coinductive reasoning does not make up results out of thin air.

Cc @rust-lang/lang @rust-lang/types @digama0

Start by reproducing the linked Rust Playground example and reading the trait-solver treatment of coinductive auto-trait obligations. Trace how the recursive Sync obligation is accepted, then use the issue's soundness concern to define tests showing that coinduction cannot establish the unsafe impl without the required progress condition.