---
title: "Coherence and trait solver"
tags: T-types, 2023-meetup-BRU, minutes
date: 2023-10-09
url: https://hackmd.io/ABcskdRCRj6WuE3TeX9zEQ
---

# Coherence and trait solver

Enabled with `-Ztrait-solver=next-coherence`, tracking issue: https://github.com/rust-lang/rust/issues/114862.

## Background

### What is the new solver

The new solver lives in [`rustc_trait_selection::solve`](https://github.com/rust-lang/rust/blob/master/compiler/rustc_trait_selection/src/solve/mod.rs) and will replace the existing *evaluate*, *fulfill*, and *project* implementation.

Goals:
- easier to understand and maintain, preventing bugs
- easier to extend going forward
- perrrrrf

For an overview, check out the `rustc-dev-guide`: https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html

### What is coherence and how does it work

Coherence makes sure that trait implementations do not overlap. It also prevents impls which currently do not overlap, but would overlap if an upstream crate were to add a backwards compatible impl.

At its core, it currently consists of two checks:

The [orphan check] validates that impls do not overlap with other impls we do not know about: either because they may be defined in a sibling crate, or because an upstream crate is allowed to add it without being considered a breaking change.

The [overlap check] validates that impls do not overlap with other impls we know about. This is done as follows:
- Instantiate the generic parameters of both impls with inference variables
- Equate the `TraitRef`s of both impls. If it fails there is no overlap.
- [implicit negative]: Check whether any of the instantiated `where`-bounds of one of the impls definitely do not hold when using the constraints from the previous step. If a `where`-bound does not hold, there is no overlap.
- *explicit negative (still unstable, ignored going forward)*: Check whether the any negated `where`-bounds can be proven, e.g. a `&mut u32: Clone` bound definitely does not hold as an explicit `impl<T> !Clone for &mut T` exists.

Because we check for failure to detect overlap, both when equating `TraitRef`s and in the implicit negative check, during coherence the trait solver must be complete.

The implicit negative check only considers goals to "definitely not hold" if they could not be implemented downstream, by a sibling, or upstream in a backwards compatible way. If the goal is is "unknowable", we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/fd80c02c168c2dfbb82c29d2617f524d2723205b/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L842-L846).

### How coherence is handled in the new solver

Whether we're in "intercrate" mode is part of the query input, in this mode we:
- do not incompletely prefer some candidates over others, to avoid unnecessary inference constraints
- add an ambiguous candidate if the current trait or `normalizes-to` goal is ambiguous
- trying to define/normalize an opaque type (TAIT) results in ambiguity

Apart from this the solver behaves exactly the same as outside of coherence. Unlike in the old solver, we do use the global cache.

## Expected impact of stabilization

There will be some breakage when switching to the new solver. We should be able to run both solvers during coherence for a while, emitting a future compat lint instead of an error if the old solver accepts more code.

### Handling projections lazily

Because of lazy normalization, we're better at handling projections containing bound variables.

It correctly detects overlap previously accepted: https://github.com/rust-lang/trait-system-refactor-initiative/issues/9#issuecomment-1750139524. This overlap was not unsound previously as the first impl is pretty much unusable with the old solver.

It is ended up fixing an previously unknown unsoundness ([#114061](https://github.com/rust-lang/rust/issues/114061)), found via crater: https://github.com/rust-lang/rust/pull/113991#issuecomment-1648811637.

Lazy normalization also forces us to improve generalization for aliases, fixing [#105787](https://github.com/rust-lang/rust/issues/105787) as well.

I do not believe that the improved projection handling also allows more code to pass coherence, as it should only remove incorrect errors.

nikomatsakis: Overall impact from crater run?

Errs: [17 failures](https://github.com/rust-lang/rust/pull/116357)

lqd: There were 10 in the last run...?

Errs: WHAT YOU LIE >:(

NM: Consider this variation of [#114061](https://github.com/rust-lang/rust/issues/114061):

// crate dep
trait IsUnit {}
impl IsUnit for () {}


pub trait WithAssoc<'a> {
    type Assoc;
}

// The two impls of `Trait` overlap
pub trait Trait {}
impl<T> Trait for T
where
    T: 'static,
    for<'a> T: WithAssoc<'a>,
    for<'a> Vec<<T as WithAssoc<'a>>::Assoc>: IsUnit, // <-- niko changed this line
    for<'a> Box<<T as WithAssoc<'a>>::Assoc>: IsUnit, // <-- what about this???
{
}
impl<T> Trait for Box<T> {}
// root crate
use dep::*;

struct Local;
impl WithAssoc<'_> for Box<Local> {
    type Assoc = ();
}

fn impls_trait<T: Trait>() {}

fn main() {
    impls_trait::<Box<Local>>();
}

NM: I'd like to review how/when we decide to insert ambiguity, in particular for the above example, the "is knowable" rule needs to observe that `Box<T::Assoc>: IsUnit` is *not* knowable, which is specific to `Box` being fundamental. Related to [#99554](https://github.com/rust-lang/rust/issues/99554).

### Inductive cycles are now ambiguous, not error

https://github.com/rust-lang/trait-system-refactor-initiative/issues/20

Inductive cycles in the new solver are now ambiguous, not error. This is actually not strictly necessary and could be changed to keep the current behavior, but desirable given our medium-term plan to change more things to be coinductive.

This breaks a single crate where a manual `PartialEq` impl overlaps with the derived one: https://github.com/kazatsuyu/interval-map/blob/a4a381b0db3c8f7ba5622c2c2edfbed886edd029/src/interval_map.rs#L88-L96.

NM: :shipit:

### Overflow is now non-fatal (unbreaking!)

https://github.com/rust-lang/trait-system-refactor-initiative/issues/67

Overflow in the trait solver has been changed to be non-fatal, allowing more code to pass.

### Leak check changes

_{we may want to talk about this when talking about higher-ranked region solving in general instead}

https://github.com/rust-lang/trait-system-refactor-initiative/issues/34 : because we erase universe information when canonicalizing query inputs, the leak check does not detect universe errors involving placeholders created outside of the canonical query. As we also call a nested query for higher-ranked goal, this makes the leak-check slightly weaker than before.

https://github.com/rust-lang/trait-system-refactor-initiative/issues/37 : We now always add `TypeOutlives` and `RegionOutlives` constraints during trait solving, meaning that these bounds may now be used by the leak check.

### Cycle checking now looks at projection goals while checking where-bounds

https://github.com/rust-lang/trait-system-refactor-initiative/issues/10

A small bug fix which shouldn't matter. It did not cause any crater breakage.

### `fn match_fresh_trait_refs` removal in new solver

https://github.com/rust-lang/trait-system-refactor-initiative/issues/56

This check sometimes incorrectly changed goals to be ambiguous in the old solver, its removal therefore allows slightly more code. This shouldn't matter.

## Remaining work until stabilization

All of these issues are also tracked in https://github.com/rust-lang/rust/issues/114862

Let's only talk about issues which are not straightforward for us to implement.

### Performance

A perf run with `-Ztrait-solver=next-coherence` enabled was neutral: https://github.com/rust-lang/rust/pull/113895#issuecomment-1648194519.

However `typenum` is still slower than with the old solver as it now ends up hitting non-fatal overflow in a branching path, resulting in some sort of exponential blowup.

### Overflow handling

The current approach is kind of arbitrary and can probably be improved. The core idea is to reduce the depth for nested goals the first time a nested goal causes overflow, to prevent a hang in the following example:

trait Trait {}

struct A<T: ?Sized>(*const T);
struct B<T: ?Sized>(*const T);

impl<T: ?Sized> Trait for T
where
    A<T>: Trait,
    B<T>: Trait,
{}

fn impls_trait<T: Trait>() {}

fn main() {
    impls_trait::<()>();
}

The core of the current impl is [`SearchGraph::allowed_depth_for_nested`]( https://github.com/rust-lang/rust/blob/d4ba2b4c7c938cf90c03a265cb31356537f608ad/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs#L147-L170).

I can think of 3 improvements here:
- currently the global cache stores the exact allowed depth for goals with resulted in overflow, only using the cache entry if the depth is an exact match. This is not strictly necessary and can be improved as long as we're careful. Improving this is fully backwards compatible.
- improve the algorithm in `SearchGraph::allowed_depth_for_nested` to reduce the allowed depth more quickly or in a more complex way. This can easily be a breaking change. Decreasing the remaining depth too quickly can change goals from success/error to overflow, causing code to stop compiling. While going the other way can result in performance regressions/defacto hangs of code which previously compiled fine.
- make it more difficult to accidentally cause exponential blowup by changing `alias-relate`

Conclusion

> Can we at least get something so that increasing fuel linearly only takes linearly more time and is strictly more "successful"? That would mean people could override the depth at root without as much fear.

### Improving `alias-relate`/normalization

https://github.com/rust-lang/trait-system-refactor-initiative/issues/68

We currently have exponential blowup in some cases due to lazy normalization, not sure whether we should discuss them right now.

## Future extensions

Coherence currently searches for failing goals by checking each goal separately. We could use a `FulfillmentCtxt` and simply check whether `select_where_possible` returns an error.

This allows far more code to pass coherence - which is desirable - but will be incredibly hard to revert because of this. I would like to make this change separately once we've already changed solvers

[orphan check]: https://github.com/rust-lang/rust/blob/fd80c02c168c2dfbb82c29d2617f524d2723205b/compiler/rustc_trait_selection/src/traits/coherence.rs#L566-L579
[overlap check]: https://github.com/rust-lang/rust/blob/fd80c02c168c2dfbb82c29d2617f524d2723205b/compiler/rustc_trait_selection/src/traits/coherence.rs#L92-L98
[implicit negative]: https://github.com/rust-lang/rust/blob/fd80c02c168c2dfbb82c29d2617f524d2723205b/compiler/rustc_trait_selection/src/traits/coherence.rs#L223-L281

## Questions of particular interest

### Distinct impls based on associated type

NM: Sometimes it would be useful to have distinct impls based on the associated type. Have we thought about this?

all: Yes.

NM: I'd like it supported, but let's not talk about it now.

### What exactly is breaking?

Jack: What exactly is breaking?

...

### Fatal overflow examples

TODO(@lcnr): Where does fatal overflow result in undesirable errors.

### RFC for overflow stability guarantees?

- do we want a global flag to increase the recursion depth

### Crater runs?

NM: This suggests we did crater runs. What was the outcome?

https://github.com/rust-lang/rust/pull/116357

## Notes, minutes from the meeting itself

What is blocking us from stabilizing next-coherence?

* nikomatsakis: Overflow, alias-relate
* errs: we should do our due diligence, but I don't want to block forever on this
* tracking issue [#114862](https://github.com/rust-lang/rust/issues/114862):

lcnr:

https://github.com/rust-lang/rust/issues/105787

https://github.com/rust-lang/trait-system-refactor-initiative/issues/8

https://github.com/rust-lang/trait-system-refactor-initiative/issues/1

## orphan check and projections

https://github.com/rust-lang/rust/issues/99554

We did the naive fix for this which treated associated types by searching their inputs `<T as Foo>::Item`...but it broke a TON of code that follows this pattern...

#[derive(Deserialize, Archive)]
struct Foo<T>(T);
// desugars
impl<T, D> Deserialize<Foo<T>, D> for <Foo<T> as Archive>::Archived {
    // ...
}

impl<T> Archive for Foo<T> {
   type Assoc = LocalType;
}

...but we could fix this if we can normalize successfully. [This appears to be what we concluded last year](https://github.com/rust-lang/rust/issues/99554#issuecomment-1332630114). lcnr did some exploration and concluded that it is sound and wanted to have a [deep dive reviewing their hackmd][deepdive]. Key point is that when we normalize in coherence mode, we have to check *is knowable*.

[deepdive]: https://hackmd.io/SxCN_4Y9S0-s0maV4JIEBw

NM: One thing I'm interested in looking at together is how and whether we could extend a-mir-formality to model these things.