Invariants of the Rust Type System (cont.)

This invariant only holds if we check region constraints. As we do not check region constraints during implicit negative overlap check in coherence, this invariant is broken there. As this check relies on *completeness* of the trait solver, it is not able to use the current region constraints check - `InferCtxt::resolve_regions` - as its handling of type outlives goals is incomplete. ### Normalization of semantically equal aliases in empty environments results in a unique type ✅ Normalization for alias types/consts has to have a unique result. Otherwise we can easily implement transmute in safe code. Given the following function, we have to make sure that the input and output types always get normalized to the same concrete type. ```rust fn foo<T: Trait>( x: <T as Trait>::Assoc ) -> <T as Trait>::Assoc { x } ``` Many of the currently known unsound issues end up relying on this invariant being broken. It is however very difficult to imagine a sound type system without this invariant, so the issue is that the invariant is broken, not that we incorrectly rely on it. ### Generic goals and their instantiations have the same result ✅ Pretty much: If we successfully typecheck a generic function concrete instantiations of that function should also typeck. We should not get errors post-monomorphization. We can however get overflow errors at that point. TODO: example for overflow error post-monomorphization This invariant is relied on to allow the normalization of generic aliases. Breaking it can easily result in unsoundness, e.g. [#57893](https://github.com/rust-lang/rust/issues/57893) ### Trait goals in empty environments are proven by a unique impl ✅ If a trait goal holds with an empty environment, there should be a unique `impl`, either user-defined or builtin, which is used to prove that goal. This is necessary to select a unique method. We do however break this invariant in few cases, some of which are due to bugs, some by design: - *marker traits* are allowed to overlap as they do not have associated items - *specialization* allows specializing impls to overlap with their parent - the builtin trait object trait implementation can overlap with a user-defined impl: [#57893]

This section continues discussing Rust type system invariants. It details how region constraint checks impact the uniqueness of normalization for semantically equal aliases. It then introduces the invariant that generic goals and their instantiations should have the same result, preventing errors post-monomorphization (except for overflow errors). Finally, it outlines the requirement for trait goals in empty environments to be proven by a unique impl, while also highlighting exceptions for marker traits, specialization, and trait object implementations.