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

[runiq]

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?

[jschievink]

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

[alice]

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