Skip to content

Commit 43b956e

Browse files
lcnrlcnr
committed
rewrite requirements/invariants
1 parent 3735857 commit 43b956e

File tree

3 files changed

+141
-71
lines changed

3 files changed

+141
-71
lines changed

‎src/SUMMARY.md

+1
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,7 @@
124124
- [Goals and clauses](./traits/goals-and-clauses.md)
125125
- [Canonical queries](./traits/canonical-queries.md)
126126
- [Next-gen trait solving](./solve/trait-solving.md)
127+
- [Invariants of the type system](./solve/invariants.md)
127128
- [The solver](./solve/the-solver.md)
128129
- [Canonicalization](./solve/canonicalization.md)
129130
- [Coinduction](./solve/coinduction.md)

‎src/solve/invariants.md

+140
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
# Invariants of the type system
2+
3+
FIXME: This file talks about invariants of the type system as a whole, not only the solver
4+
5+
There are a lot of invariants - things the type system guarantees to be true at all times -
6+
which are desirable or expected from other languages and type systems. Unfortunately, quite
7+
a few of them do not hold in Rust right now. This is either a fundamental to its design or
8+
caused by bugs and something that may change in the future.
9+
10+
It is important to know about the things you can assume while working on - and with - the
11+
type system, so here's an incomplete and inofficial list of invariants of
12+
the core type system:
13+
14+
- ✅: this invariant mostly holds, with some weird exceptions, you can rely on it outside
15+
of these cases
16+
- ❌: this invariant does not hold, either due to bugs or by design, you must not rely on
17+
it for soundness or have to be incredibly careful when doing so
18+
19+
### `wf(X)` implies `wf(normalize(X))` ✅
20+
21+
If a type containing aliases is well-formed, it should also be
22+
well-formed after normalizing said aliases. We rely on this as
23+
otherwise we would have to re-check for well-formedness for these
24+
types.
25+
26+
This is invariantunfortunately broken for `<fndef as FnOnce<..>>::Output` due to implied bounds, resulting in [#114936].
27+
28+
### applying inference results from a goal does not change its result ❌
29+
30+
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
31+
32+
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.
33+
34+
This unfortunately does not hold - at least in the new solver - due to a few annoying reasons.
35+
36+
### The trait solver has to be *locally sound* ✅
37+
38+
This means that we must never return *success* for goals for which no `impl` exists. That would
39+
mean we assume a trait is implemented even though it is not, which is very likely to result in
40+
actual unsoundness. When using `where`-bounds to prove a goal, the `impl` will be provided by the
41+
user of the item.
42+
43+
This invariant only holds if we check region constraints. As we do not check region constraints
44+
during implicit negative overlap check in coherence, this invariant is broken there. As this check
45+
relies on *completeness* of the trait solver, it is not able to use the current region constraints
46+
check - `InferCtxt::resolve_regions` - as its handling of type outlives goals is incomplete.
47+
48+
### Normalization of semantically equal aliases empty environments results in a unique type ✅
49+
50+
Normalization for alias types/consts has to have a unique result. Otherwise we can easily
51+
implement transmute in safe code. Given the following function, we have to make sure that
52+
the input and output types always get normalized to the same concrete type.
53+
54+
```rust
55+
fn foo<T: Trait>(
56+
x: <T as Trait>::Assoc
57+
) -> <T as Trait>::Assoc {
58+
x
59+
}
60+
```
61+
62+
Many of the currently known unsound issues end up relying on this invariant being broken.
63+
It is however very difficult to imagine a sound type system without this invariant, so
64+
the issue is that the invariant is broken, not that we incorrectly rely on it.
65+
66+
### Generic goals and their instantiations have the same result ✅
67+
68+
Pretty much: If we successfully typecheck a generic function concrete instantiations
69+
of that function should also typeck. We should not get errors post-monomorphization.
70+
We can however get overflow errors at that point.
71+
72+
TODO: example for overflow error post-monomorpghization
73+
74+
This invariant is relied on to allow the normalization of generic aliases. Breaking
75+
it can easily result in unsoundness, e.g. [#57893](https://github.com/rust-lang/rust/issues/57893)
76+
77+
### Trait goals in empty environments are proven by a unique impl ✅
78+
79+
If a trait goal holds with an empty environment, there should be a unique `impl`,
80+
either user-defined or builtin, which is used to prove that goal. This is
81+
necessary to select a unique method. It
82+
83+
We do however break this invariant in few cases, some of which are due to bugs,
84+
some by design:
85+
- *marker traits* are allowed to overlap as they do not have associated items
86+
- *specialization* allows specializing impls to overlap with their parent
87+
- the builtin trait object trait implementation can overlap with a user-defined impl:
88+
[#57893]
89+
90+
### The type system is complete ❌
91+
92+
The type system is not complete, it often adds unnecessary inference constraints, and errors
93+
even though the goal could hold.
94+
95+
- method selection
96+
- opaque type inference
97+
- handling type outlives constraints
98+
- preferring `ParamEnv` candidates over `Impl` candidates during candidate selection
99+
in the trait solver
100+
101+
#### The type system is complete during the implicit negative overlap check in coherence ✅
102+
103+
During the implicit negative overlap check in coherence we must never return *error* for
104+
goals which can be proven. This would allow for overlapping impls with potentially different
105+
associated items, breaking a bunch of other invariants.
106+
107+
This invariant is currently broken in many different ways while actually something we rely on.
108+
We have to be careful as it is quite easy to break:
109+
- generalization of aliases
110+
- generalization during subtyping binders (luckily not exploitable in coherence)
111+
112+
### Trait solving must be (free) lifetime agnostic ✅
113+
114+
Trait solving during codegen should have the same result as during typeck. As we erase
115+
all free regions during codegen we must not rely on them during typeck. A noteworthy example
116+
is special behavior for `'static`.
117+
118+
We also have to be careful with relying on equality of regions in the trait solver.
119+
This is fine for codegen, as we treat all erased regions as equal. We can however
120+
lose equality information from HIR to MIR typeck.
121+
122+
The new solver "uniquifies regions" during canonicalization, canonicalizing `u32: Trait<'x, 'x>`
123+
as `exists<'0, '1> u32: Trait<'0, '1>`, to make it harder to rely on this property.
124+
125+
### Removing ambiguity makes strictly more things compile ❌
126+
127+
Ideally we *should* not rely on ambiguity for things to compile. Not doing that will cause future improvements to be breaking changes.
128+
129+
Due to *incompleteness* this is not the case and improving inference can result in inference
130+
changes, breaking existing projects.
131+
132+
### Semantic equality implies structural equality ✅
133+
134+
Two types being equal in the type system must mean that they have the
135+
same `TypeId` after instantiating their generic parameters with concrete
136+
arguments. This currently does not hold: [#97156].
137+
138+
[#57893]: https://github.com/rust-lang/rust/issues/57893
139+
[#97156]: https://github.com/rust-lang/rust/issues/97156
140+
[#114936]: https://github.com/rust-lang/rust/issues/114936

‎src/solve/trait-solving.md

-71
Original file line numberDiff line numberDiff line change
@@ -39,77 +39,6 @@ which does not have any nested goals. Therefore `Vec<T>: Clone` holds.
3939
The trait solver can either return success, ambiguity or an error as a [`CanonicalResponse`].
4040
For success and ambiguity it also returns constraints inference and region constraints.
4141

42-
## Requirements
43-
44-
Before we dive into the new solver lets first take the time to go through all of our requirements
45-
on the trait system. We can then use these to guide our design later on.
46-
47-
TODO: elaborate on these rules and get more precise about their meaning.
48-
Also add issues where each of these rules have been broken in the past
49-
(or still are).
50-
51-
### 1. The trait solver has to be *sound*
52-
53-
This means that we must never return *success* for goals for which no `impl` exists. That would
54-
simply be unsound by assuming a trait is implemented even though it is not. When using predicates
55-
from the `where`-bounds, the `impl` will be proved by the user of the item.
56-
57-
### 2. If type checker solves generic goal concrete instantiations of that goal have the same result
58-
59-
Pretty much: If we successfully typecheck a generic function concrete instantiations
60-
of that function should also typeck. We should not get errors post-monomorphization.
61-
We can however get overflow as in the following snippet:
62-
63-
```rust
64-
fn foo<T: Trait>(x: )
65-
```
66-
67-
### 3. Trait goals in empty environments are proven by a unique impl
68-
69-
If a trait goal holds with an empty environment, there is a unique `impl`,
70-
either user-defined or builtin, which is used to prove that goal.
71-
72-
This is necessary for codegen to select a unique method.
73-
An exception here are *marker traits* which are allowed to overlap.
74-
75-
### 4. Normalization in empty environments results in a unique type
76-
77-
Normalization for alias types/consts has a unique result. Otherwise we can easily implement
78-
transmute in safe code. Given the following function, we have to make sure that the input and
79-
output types always get normalized to the same concrete type.
80-
```rust
81-
fn foo<T: Trait>(
82-
x: <T as Trait>::Assoc
83-
) -> <T as Trait>::Assoc {
84-
x
85-
}
86-
```
87-
88-
### 5. During coherence trait solving has to be complete
89-
90-
During coherence we never return *error* for goals which can be proven. This allows overlapping
91-
impls which would break rule 3.
92-
93-
### 6. Trait solving must be (free) lifetime agnostic
94-
95-
Trait solving during codegen should have the same result as during typeck. As we erase
96-
all free regions during codegen we must not rely on them during typeck. A noteworthy example
97-
is special behavior for `'static`.
98-
99-
We also have to be careful with relying on equality of regions in the trait solver.
100-
This is fine for codegen, as we treat all erased regions as equal. We can however
101-
lose equality information from HIR to MIR typeck.
102-
103-
### 7. Removing ambiguity makes strictly more things compile
104-
105-
We *should* not rely on ambiguity for things to compile.
106-
Not doing that will cause future improvements to be breaking changes.
107-
108-
### 8. semantic equality implies structural equality
109-
110-
Two types being equal in the type system must mean that they have the same `TypeId`.
111-
112-
11342
[solve]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/index.html
11443
[`Goal`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/solve/struct.Goal.html
11544
[`Predicate`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.Predicate.html

0 commit comments

Comments
 (0)