Coinductive auto-trait treatment is questionably sound

[RalfJung]

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

[theemathas]

However, what else could the safety obligation possibly be...?

"In order to disprove that MyCell implements Sync, one must prove that there's some non-circular reason that where MyCell: Sync doesn't hold."

Does this work? Or does it play poorly with non-auto traits or with lifetimes?

[RalfJung]

I don't know what you mean by this. But I noticed you used negation, which I don't think will work. The one framework we have that can express non-trivial safety guarantees (RustBelt) is based on a logic where the Law of Excluded Middle does not hold. Contraposition as a logical principle (P → Q being equivalent to ¬Q → ¬P) is not valid in such logics.

[RalfJung]

Also see the Zulip discussion

[RalfJung]

I thought about this some more during the last days, and I think I can now explain how I would expect this to work. I have no idea how feasible that would be to actually implement though. :)

One core question one has to answer when doing coinduction is: what exactly counts as "progress"? Coinduction allows loops, as long as at least one step on the loop makes "progress".

The semantics @lcnr described to me basically amount to: any impl counts as "progress".

The semantics I expected is that impls are in some way marked with whether they are considered to make "progress" or not. The implicit auto trait impls are considered to make "progress", but when I manually write an impl like the one above, that one is not considered to make "progress". The reason it is sound for the implicit impls to make "progress" is that they reduce the question from one about the type to one about the fields, which will only be recursive if the type itself is recursive, i.e., we can do coinduction along the recursive structure of the type and carry along a corresponding coinductive proof of the auto trait. Put differently, any finite unrolling of the recursive type will have a corresponding finite unrolling of the auto trait proof. That, to me, is the key soundness property: actually infinitely recursive values do not exist; every value just needs to unroll the type finitely often, and then there should be a corresponding finite proof of the trait that works for this specific value.

[theemathas]

actually infinitely recursive values do not exist

What about reference cycles?

[RalfJung]

Hm, fair. In that case, I would consider any finite "prefix" of "unrolling" the value -- after all, a program can (in finite time) only inspect a finite part of the infinitely unrolled value.