Why are the `Borrow` trait's invariants not enforced by the type system?

From How to understand the example of the Borrow trait in the Book?:

An important fact that isn’t explicitly mentioned in the book is this requirement from the Borrow documentation :

If you are implementing Borrow and both Self and Borrowed implement Hash , Eq , and/or Ord , they must produce the same result.

This isn’t enforced by the type system (so you can’t rely on it for memory safety), but it is a documented requirement for all implementers of the Borrow trait. This means that if you have a String and an &str you can hash both of them directly, without first converting them to have the same type.

Why are these invariants not enforced by the type system?

Those invariants can not be represented in the type system. They would require proving equivalence of arbitrary code, which is undecidable.


You can't have the compiler look inside two different functions and automatically verify that they do the same thing.