- [Invariants of the type system](./solve/invariants.md)

FIXME: This file talks about invariants of the type system as a whole, not only the solver

There are a lot of invariants - things the type system guarantees to be true at all times -

which are desirable or expected from other languages and type systems. Unfortunately, quite

a few of them do not hold in Rust right now. This is either a fundamental to its design or

caused by bugs and something that may change in the future.

It is important to know about the things you can assume while working on - and with - the

type system, so here's an incomplete and inofficial 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

If a type containing aliases is well-formed, it should also be

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 is unfortunately broken for `<fndef as FnOnce<..>>::Output` due to implied bounds,

resulting in [#114936].

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:

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.

This unfortunately does not hold - at least in the new solver - due to a few annoying reasons.

This means that we must never return *success* for goals for which no `impl` exists. That would

mean we assume a trait is implemented even though it is not, which is very likely to result in

actual unsoundness. When using `where`-bounds to prove a goal, the `impl` will be provided by the

user of the item.

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 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.

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.

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)

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. It

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:

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

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 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.

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.

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].

[#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

The entry-point of the solver is `InferCtxtEvalExt::evaluate_root_goal`. This

function sets up the root `EvalCtxt` and then calls `EvalCtxt::evaluate_goal`,

to actually enter the trait solver.

`EvalCtxt::evaluate_goal` handles [canonicalization](./canonicalization.md), caching,

overflow, and solver cycles. Once that is done, it creates a nested `EvalCtxt` with a

separate local `InferCtxt` and calls `EvalCtxt::compute_goal`, which is responsible for the

'actual solver behavior'. We match on the `PredicateKind`, delegating to a separate function

for each one.

For trait goals, such a `Vec<T>: Clone`, `EvalCtxt::compute_trait_goal` has

to collect all the possible ways this goal can be proven via

`EvalCtxt::assemble_and_evaluate_candidates`. Each candidate is handled in

a separate "probe", to not leak inference constraints to the other candidates.

We then try to merge the assembled candidates via `EvalCtxt::merge_candidates`.

To prove nested goals, we don't directly call `EvalCtxt::compute_goal`, but instead

add the goal to the `EvalCtxt` with `EvalCtxt::all_goal`. We then prove all nested

goals together in either `EvalCtxt::try_evaluate_added_goals` or

`EvalCtxt::evaluate_added_goals_and_make_canonical_response`. This allows us to handle

inference constraints from later goals.

E.g. if we have both `?x: Debug` and `(): ConstrainToU8<?x>` as nested goals,

then proving `?x: Debug` is initially ambiguous, but after proving `(): ConstrainToU8<?x>`

we constrain `?x` to `u8` and proving `u8: Debug` succeeds.

We lazily normalize types in the solver, so we always have to assume that any types

and constants are potentially unnormalized. This means that matching on `TyKind` can easily

be incorrect.

We handle normalization in two different ways. When proving `Trait` goals when normalizing

associated types, we separately assemble candidates depending on whether they structurally

match the self type. Candidates which match on the self type are handled in

`EvalCtxt::assemble_candidates_via_self_ty` which recurses via

`EvalCtxt::assemble_candidates_after_normalizing_self_ty`, which normalizes the self type

by one level. In all other cases we have to match on a `TyKind` we first use

`EvalCtxt::try_normalize_ty` to normalize the type as much as possible.

In case the goal is higher-ranked, e.g. `for<'a> F: FnOnce(&'a ())`, `EvalCtxt::compute_goal`

eagerly instantiates `'a` with a placeholder and then recursively proves

`F: FnOnce(&'!a ())` as a nested goal.

Some goals can be proven in multiple ways. In these cases we try each option in

a separate "probe" and then attempt to merge the resulting responses by using

`EvalCtxt::try_merge_responses`. If merging the responses fails, we use

`EvalCtxt::flounder` instead, returning ambiguity. For some goals, we try

incompletely prefer some choices over others in case `EvalCtxt::try_merge_responses`

fails.

The solver should be fairly self-contained. I hope that the above information provides a

good foundation when looking at the code itself. Please reach out on zulip if you get stuck

while doing so or there are some quirks and design decisions which were unclear and deserve

better comments or should be mentioned here.