Enforce informal properties of traits such as `PartialEq`

[varkor]

The trait PartialEq represents a partial equivalence — that is, a relation that is symmetric and transitive. However, Rust doesn't currently enforce these properties in any way. This means we get issues like this:

struct A;
struct B;

impl PartialEq<B> for A {
    fn eq(&self, _other: &B) -> bool {
        true
    }
}

fn main() {
    let a = A {};
    let b = B {};
    a == b; // Works
    b == a; // Error (B does not implement PartialEq<A>)
}

This is confusing, but it's usually not so much of an issue in user code, because it's easy to flip the operands. However, when attempting to write generic functions over these traits, you run into problems (for example in #46934).

At the very least there should be a lint warning/error for this. It'd be nice to have a generic solution for properties of traits, though that could come later. It'd be even nicer if the symmetric case for PartialEq, for instance, could be automatically implemented by Rust, though this could require quite a bit more machinery.

[alilleybrinker]

This question has come up a lot in the context of Haskell, and multiple ideas exist for how to enforce that typeclass/trait-associated "laws" are upheld. The conclusion has generally been that mechanisms to statically enforce compliance with these laws are too heavyweight to be worthwhile. There may be special case instances like the one you've provided where more limited analysis can support some helpful lints, but solving the issue in the general case is complex.

[varkor]

This isn't quite the same as typeclass laws in Haskell, in which you might want to check that an operation is associative, for example (which would be analogous to imposing rules on the methods declared by a trait). This is about properties of trait conformance, which we have all the information in the compiler for already, because they're assertions about concrete types, which already have to be resolved by the type system.
What I'm suggesting would not be powerful enough to check that <A as PartialEq<B>>::eq was actually in a symmetric correspondence with <B as PartialEq<A>>::eq — that's on the user to ensure.

[CAD97]

Something like the following works today to enforce this: (playground link)

trait Equal<Other>
where Other: Equal<Self>
{}

struct A {}
struct B {}

impl Equal<B> for A {}
impl Equal<A> for B {}

Removing either impl Equal causes the example to not compile.

If you wanted to provide automatic reflexive definitions, you might try:

impl <T1, T2> Equal<T1> for T2
where T1: Equal<T2>
{}

But this causes a duplicate impl Equal for whatever type you impl it for (as it gets one from the generic impl as well). But, this can be solved with specialization! (playground link)

trait Equal<Other>
where
    Other: ?Sized,
    Other: Equal<Self>,
{
    fn eq(&self, other: &Other) -> bool;
}

default impl <T1, T2> Equal<T1> for T2
where T1: Equal<T2>
{
    fn eq(&self, other: &T1) -> bool {
        other.eq(self)
    }
}

struct A {}
struct B {}

impl Equal<B> for A {
    fn eq(&self, b: &B) -> bool {
        true
    }
}

So the machinery exists, it's just a matter of why the lib team decided that PartialEq<Rhs> shouldn't enforce Rhs: PartialEq<Self>. It may just be that the auto-reflexive impl wasn't possible at the time.

I will repeat that this requirement, though not enforced by the type system, is stated in the informal description of the trait:

Note that these requirements mean that the trait itself must be implemented symmetrically and transitively: if T: PartialEq<U> and U: PartialEq<V> then U: PartialEq<T> and T: PartialEq<V>.

I do not think the type system can at this time enforce the transitive requirement.

---

Another option, which I don't like but include here for completeness, is to make the == syntax check for both PartialEq::eq(lhs, rhs) and PartialEq::eq(rhs, lhs).

[alilleybrinker]

@varkor, right I meant that the general case of wanting to enforce arbitrary trait laws is analogous to the problems faced in Haskell. You're right that for the particular issue you raise, a solution is available. I wasn't sure what level of result you were looking for.

[varkor]

@CAD97: Your example works in the Playground, but when I try to implement it similarly in cmp.rs, I get error[E0391]: unsupported cyclic reference between types/traits detected for the default impl. I'm not yet so familiar with specialisation, so I'm not sure how these two cases might be different. Do you have any ideas?

[CAD97]

@varkor Are you sure you haven't mixed PartialEq and Eq? E0391 seems to be only concerned with trait T1: T2 and trait T2: T1?

Other than that, I'm not sure. I haven't played too much with specialization yet myself, either.

[steveklabnik]

Triage: no changes i'm aware of

[Mark-Simulacrum]

cc #81198, #115386

My sense is that the current direction is rather the opposite (to remove these informal properties), rather than enforce them. Once those PRs land we should revisit this.