PartialEq, PartialOrd: update and synchronize handling of transitive chains

[RalfJung]

It was brought up in https://internals.rust-lang.org/t/total-equality-relations-as-std-eq-rhs/19232 that we currently have a gap in our PartialEq rules, which this PR aims to close:

For example, with PartialEq's conditions you may have a = b = c = d ≠ a (where a and c are of type A, b and d are of type B).

The second commit fixes #87067 by updating PartialOrd to handle the requirements the same way PartialEq does.

[rustbot]

r? @m-ou-se

(rustbot has picked a reviewer for you, use r? to override)

[RalfJung]

There was another comment posed here that seemingly got removed again, starting with

As mentioned in the IRLO thread, this property is impossible to enforce for chains of 4 types or more because while everybody enforces the property, you will get violations from combinations of independent crates.

Note that when considering semver-compatible evolution of crates, this is already the case today. The alpha/beta example in the docs doesn't need the new "chain" part of transitivity, it already works on today's published docs.

(Generally please don't remove comments, that kind of rewriting of history makes discussions very confused to follow later, or to follow the email notification chain. Just edit or post a 2nd reply to explain why you changed your mind.)

[dtolnay]

We discussed this PR in today's T-libs-api meeting and were skeptical that the new content (neither the clarification on transitivity nor the new paragraph regarding cross-crate impls) would have a practical consequence on people writing more correct PartialEq impls.

My personal view: I can see that the existing definition is not bulletproof, but if I imagine a hypothetical bulletproof definition or something in that direction (such as this PR), it is not obvious to me that a PartialEq impl which does not conform to the new definition is more likely to mean the impl is wrong or the new definition is bad. This significantly reduces my interest in pinning down a more precise definition of what makes a PartialEq impl correct. I think the intended use for PartialEq conveyed by the current docs, and the remaining wiggle room for impls, is pretty good.

[RalfJung]

So, the docs are ambiguous but there is no intent to fix them? That's the worst possible outcome. :( It runs a high risk of people interpreting the docs in different ways without even realizing that they are deliberately ambiguous. Note that these questions about transitivity come up for real, see e.g. here and here. The current documentation is not answering the questions people have.

[RalfJung]

I have removed the new paragraph about dealing with the multi-crate situation. Now all this PR does is un-do a likely accidental side-effect of #81198: before that PR, it was the case that if A: PartialEq<B> and B: PartialEq<C> and C: PartialEq<D> and A: PartialEq<D> all hold, then if a == b == c == d, we have a == d. After #81198, that was no longer required. I found no discussion indicating that this was deliberate, and it seems like a property that we would want, so I propose that we revert this accidental change and require this property again.

It is true that this transitivity requirement cannot be upheld on a per-crate level. However, that is already the case for the transitivity requirement that we have documented right now. In other words, the docs are already somewhat aspirational when it comes to multi-crate situations. Therefore I think we really should document that, ideally, this property holds for longer chains as well.

#118108 does the same thing for PartialOrd. There, the equivalent of #81198 has not been applied yet, so we don't have to revert any prior changes. I think it would be a mistake to lose the transitive-chain property on <, so I made #118108 preserve that property. So another way to think of this PR here is as restoring consistency between PartialEq and PartialOrd.

Re-nominating due to the changed PR contents and the new information (this un-does a likely accidental change, bringing us closer to how things were documented before 2021, rather than introducing something completely new).

[m-ou-se]

What about this situation?

i32 == JsonValue == f64 == CborValue

In json, there is no distinction between integers and floats. Having both a PartialEq<i32> and PartialEq<f64> impl for JsonValue such that the same value can be both == 1 and == 1.0 makes perfect sense.

In cbor, there is a distinction between integers and floats. Having both a PartialEq<i32> and PartialEq<f64> impl for CborValue such that the a value can be == 1 but not == 1.0 makes perfect sense.

But that allows for:

• 1i32 == JsonValue::number(1), and
• JsonValue::number(1) == 1.0f64, and
• 1.0f64 == CborValue::float(1.0), and
• 1i32 != CborValue::float(1.0).

Which would break the proposed chaining rule.

Does that mean there's a problem with one of the PartialEq implementations in this example, or with the proposed rule?

[RalfJung]

Similar problems already arise with the rule as documented today: assuming both JsonValue and CborValue can be compared with both i32 and i64 (and assuming CborValue are inequal whenever the type differs). Now imagine we wanted to add a i32 == i64 impl in the standard library. It would be impossible since no matter which impl we add, it conflicts with one of those types.

Arguably libraries shouldn't "connect" two outside-the-crate types by equality that are not already connected. The moment they do, they are defining a notion of equality on a pair of types they do not control, and different libraries could define conflicting notions of equality.

So, I don't have a solution to this issue, but it's not an issue introduced by this PR. The issue was introduced by #81198.

[m-ou-se]

@RalfJung Some additional thoughts on that issue:

If JsonValue only had PartialEq implementations in one direction (that is: JsonValue == i32 and JsonValue == f32, but not i32 == JsonValue), then the rule is technically not broken.

The rule is about a == b && b == c, but not a == b && c == b.

Does that mean that a JsonValue that "connects" i32 and f32 only one one side is fine? Or do you think that the transitive rule should also apply with swapped operands to ==?

[joshtriplett]

Suggested change

	/// This must also work for longer chains, such as when `A: PartialEq<B>`, `B: PartialEq<C>`,
	/// This should also work for longer chains, such as when `A: PartialEq<B>`, `B: PartialEq<C>`,

Attempting to account for the state of the ecosystem, here.

[RalfJung]

Should the "must" above this enumeration also become a "should"? Or do you intentionally make a difference between the "basic" transitivity case and the cases involving longer chains (or symmetry, as per Mara's point)?

[joshtriplett]

@RalfJung It's possible that the other "must"s here should also become "should"s, in practice, though longer chains are more likely to fail these properties. De facto, the ecosystem is going to continue to provide impls that don't satisfy all of these properties, and as a result, code can't have any definitive reliance on these properties. "should" acknowledges that these properties are more on the "try not to confuse the humans reading your code" side than the "allow computers to reason about your code" side.

[RalfJung]

as a result, code can't have any definitive reliance on these properties

We already document that "Violating these requirements is a logic error. The behavior resulting from a logic error is not specified, but users of the trait must ensure that such logic errors do not result in undefined behavior. This means that unsafe code must not rely on the correctness of these methods." In other words, we already expect a certain amount of resilience against these properties being violated.

I guess the open question is whether

• we make this "must" and violating them is therefore declared a bug (albeit one that can, at worst, cause panics or logic misbehavior, not UB)
• we make this "should" and... well I guess I am not sure what that would mean? Is now the code that relies (to the extent permitted by the docs) on the property the one that is buggy? Or is the conclusion that sometimes things just don't compose and we don't want to take a stance on where the bug lies in that case?

My personal preference would be to make this a "must" in both cases. But I could live with a "should" as well. Until we have explicit RFC-style policies for what "must" and "should" mean, this is all a bit fuzzy anyway.

[dtolnay]

In other words, we already expect a certain amount of resilience against these properties being violated.

💯

In my opinion "must", together with the existing documentation that violating is a logic error, captures the right intent better than changing to "should".

[RalfJung]

@m-ou-se Hm, that is a good question. Before #81198, if we had A == B and C == B, we could use the symmetry rule to deduce that B == C must exist, and then use transitivity to deduce that A == C must exist and have the transitive behavior.

So it would only be consistent to allow the transitive-chain rule to also use allow using comparisons "backwards", i.e. to require that if A == B and C == B and A == C all exist then they must be consistent.

[m-ou-se]

So it would only be consistent to allow the transitive-chain rule to also use allow using comparisons "backwards", i.e. to require that if A == B and C == B and A == C all exist then they must be consistent.

I agree, but that would mean that it'd be wrong to have both JsonValue == bool and JsonValue == i32, by the "don't connect out-of-crate types" rule you mentioned.

I don't think that is something we can go forward with. It is very common for an enum to be PartialEq for different possible contained types. It happens a lot in the ecosystem already.

[rfcbot]

The final comment period, with a disposition to merge, as per the review above, is now complete.

As the automated representative of the governance process, I would like to thank the author for their work and everyone else who contributed.

This will be merged soon.

[RalfJung]

@dtolnay can I take your starting the FCP process as "r=me once FCP finishes"?

[dtolnay]

@bors r+

[bors]

📌 Commit 61d1ebe has been approved by dtolnay

It is now in the queue for this repository.

[bors]

🌲 The tree is currently closed for pull requests below priority 100. This pull request will be tested once the tree is reopened.