rust-lang/rust
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

go over invariants again :3

Browse Source 
Co-authored-by: Boxy <rust@boxyuwu.dev>
This commit is contained in:
lcnr
2025-07-16 21:29:16 +02:00
parent 8ec7e6fdee
commit 9ef3be2f86
1 changed files with 55 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

95
src/doc/rustc-dev-guide/src/solve/invariants.md
View File

@@ -11,10 +11,8 @@ It is important to know about the things you can assume while working on - and w
type system, so here's an incomplete and unofficial list of invariants of
the core type system:
- ✅: this invariant mostly holds, with some weird exceptions, you can rely on it outside
of these cases
- ❌: this invariant does not hold, either due to bugs or by design, you must not rely on
it for soundness or have to be incredibly careful when doing so
- ✅: this invariant mostly holds, with some weird exceptions or current bugs
- ❌: this invariant does not hold, and is unlikely to do so in the future; do not rely on it for soundness or have to be incredibly careful when doing so
### `wf(X)` implies `wf(normalize(X))` ✅
@@ -23,6 +21,8 @@ well-formed after normalizing said aliases. We rely on this as
otherwise we would have to re-check for well-formedness for these
types.
This currently does not hold due to a type system unsoundness: [#84533](https://github.com/rust-lang/rust/issues/84533).
### Structural equality modulo regions implies semantic equality ✅
If you have a some type and equate it to itself after replacing any regions with unique
@@ -36,7 +36,7 @@ If this invariant is broken MIR typeck ends up failing with an ICE.
TODO: this invariant is formulated in a weird way and needs to be elaborated.
Pretty much: I would like this check to only fail if there's a solver bug:
https://github.com/rust-lang/rust/blob/2ffeb4636b4ae376f716dc4378a7efb37632dc2d/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs#L391-L407
https://github.com/rust-lang/rust/blob/2ffeb4636b4ae376f716dc4378a7efb37632dc2d/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs#L391-L407 We should readd this check and see where it breaks :3
If we prove some goal/equate types/whatever, apply the resulting inference constraints,
and then redo the original action, the result should be the same.
@@ -73,30 +73,6 @@ Many of the currently known unsound issues end up relying on this invariant bein
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]
### The type system is complete ❌
The type system is not complete, it often adds unnecessary inference constraints, and errors
@@ -108,6 +84,37 @@ even though the goal could hold.
- preferring `ParamEnv` candidates over `Impl` candidates during candidate selection
in the trait solver
### Goals keep their result from HIR typeck afterwards ✅
Having a goal which succeeds during HIR typeck but fails when being reevaluated during MIR borrowck causes ICE, e.g. [#140211](https://github.com/rust-lang/rust/issues/140211).
Having a goal which succeeds during HIR typeck but fails after being instantiated is unsound, e.g. [#140212](https://github.com/rust-lang/rust/issues/140212).
It is interesting that we allow some incompleteness in the trait solver while still maintaining this limitation. It would be nice if there was a clear way to separate the "allowed incompleteness" from behavior which would break this invariant.
#### Normalization must not change results
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)
#### Goals may still overflow after instantiation
As they start to hit the recursion limit. We also have diverging aliases which are scuffed. It's unclear how these should be handled :3
### 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 unique methods and associated items.
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](https://github.com/rust-lang/rust/issues/57893)
#### The type system is complete during the implicit negative overlap check in coherence ✅
For more on overlap checking: [coherence]
@@ -121,18 +128,19 @@ 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 must not depend on lifetimes being different ✅
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`.
If a goal holds with lifetimes being different, it must also hold with these lifetimes being the same. We otherwise get post-monomorphization errors during codegen or unsoundness due to invalid vtables.
We could also just get inconsistent behavior when first proving a goal with different lifetimes which are later constrained to be equal.
### Trait solving in bodies must not depend on lifetimes being equal ✅
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.
This currently does not hold with the new solver: [trait-system-refactor-initiative#27](https://github.com/rust-lang/trait-system-refactor-initiative/issues/27).
### Removing ambiguity makes strictly more things compile ❌
@@ -146,9 +154,16 @@ changes, breaking existing projects.
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].
arguments. We can otherwise use their different `TypeId`s to impact trait selection.
[#57893]: https://github.com/rust-lang/rust/issues/57893
[#97156]: https://github.com/rust-lang/rust/issues/97156
[#114936]: https://github.com/rust-lang/rust/issues/114936
[coherence]: ../coherence.md
We lookup types using structural equality during codegen, but this shouldn't necessarily be unsound
- may result in redundant method codegen or backend type check errors?
- we also rely on it in CTFE assertions
### Semantically different types have different `TypeId`s ✅
Semantically different `'static` types need different `TypeId`s to avoid transmutes,
for example `for<'a> fn(&'a str)` vs `fn(&'static str)` must have a different `TypeId`.
[coherence]: ../coherence.md