Invariants of the Rust Type System (cont.)

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] ### The type system is complete ❌ The type system is not complete, it often adds unnecessary inference constraints, and errors even though the goal could hold. - method selection - opaque type inference - handling type outlives constraints - preferring `ParamEnv` candidates over `Impl` candidates during candidate selection in the trait solver #### The type system is complete during the implicit negative overlap check in coherence ✅ For more on overlap checking: [coherence] During the implicit negative overlap check in coherence we must never return *error* for goals which can be proven. This would allow for overlapping impls with potentially different associated items, breaking a bunch of other invariants. This invariant is currently broken in many different ways while actually something we rely on. We have to be careful as it is quite easy to break: - generalization of aliases - generalization during subtyping binders (luckily not exploitable in coherence) ### Trait solving must be (free) lifetime agnostic ✅ Trait solving during codegen should have the same result as during typeck. As we erase all free regions during codegen we must not rely on them during typeck. A noteworthy example is special behavior for `'static`. We also have to be careful with relying on equality of regions in the trait solver. This is fine for codegen, as we treat all erased regions as equal. We can however lose equality information from HIR to MIR typeck. The new solver "uniquifies regions" during canonicalization, canonicalizing `u32: Trait<'x, 'x>` as `exists<'0, '1> u32: Trait<'0, '1>`, to make it harder to rely on this property. ### Removing ambiguity makes strictly more things compile ❌ Ideally we *should* not rely on ambiguity for things to compile. Not doing that will cause future improvements to be breaking changes. Due to *incompleteness* this is not the case and improving inference can result in inference changes, breaking existing projects. ### Semantic equality implies structural equality ✅ Two types being equal in the type system must mean that they have the same `TypeId` after instantiating their generic parameters with concrete arguments. This currently does not hold: [#97156].

The discussion of Rust type system invariants continues. It covers the requirement for trait goals to be proven by a unique impl, while noting exceptions for marker traits, specialization, and trait object implementations. It then addresses the type system's incompleteness, which causes unnecessary inference constraints and errors. This is followed by the crucial completeness of the type system during implicit negative overlap checks in coherence. Further invariants discussed include trait solving being lifetime agnostic, ideally removing ambiguity to compile more things, and semantic equality implying structural equality.