relating projection substs is unsound during coherence #102048

lcnr · 2022-09-20T11:50:52Z

// This must fail coherence.
//
// Getting this to pass was fairly difficult, so here's an explanation
// of what's happening:
//
// Normalizing projections currently tries to replace them with inference variables
// while emitting a nested `Projection` obligation. This cannot be done if the projection
// has bound variables which is the case here.
//
// So the projections stay until after normalization. When unifying two projections we
// currently treat them as if they are injective, so we **incorrectly** unify their
// substs. This means that coherence for the two impls ends up unifying `?T` and `?U`
// as it tries to unify `<?T as WithAssoc1<'a>>::Assoc` with `<?U as WithAssoc1<'a>>::Assoc`.
//
// `impl1` therefore has the projection `<?T as WithAssoc2<'a>>::Assoc` and we have the
// assumption `?T: for<'a> WithAssoc2<'a, Assoc = i32>` in the `param_env`, so we normalize
// that to `i32`. We then try to unify `i32` from `impl1` with `u32` from `impl2` which fails,
// causing coherence to consider these two impls distinct.
pub trait Trait<T> {}

pub trait WithAssoc1<'a> {
    type Assoc;
}
pub trait WithAssoc2<'a> {
    type Assoc;
}

// impl 1
impl<T, U> Trait<for<'a> fn(<T as WithAssoc1<'a>>::Assoc, <U as WithAssoc2<'a>>::Assoc)> for (T, U)
where
    T: for<'a> WithAssoc1<'a> + for<'a> WithAssoc2<'a, Assoc = i32>,
    U: for<'a> WithAssoc2<'a>,
{
}

// impl 2
impl<T, U> Trait<for<'a> fn(<U as WithAssoc1<'a>>::Assoc, u32)> for (T, U) where
    U: for<'a> WithAssoc1<'a>
{
}

this currently compiles even though the following crate would mean that both impls overlap:

extern crate test1;
use test1::*;

struct Ty1;
struct Ty2;

impl WithAssoc1<'_> for Ty1 {
    type Assoc = ();
}
impl WithAssoc2<'_> for Ty1 {
    type Assoc = i32;
}
impl WithAssoc1<'_> for Ty2 {
    type Assoc = ();
}
impl WithAssoc2<'_> for Ty2 {
    type Assoc = u32;
}

fn foo<T, U>()
where
    (T, U): Trait<for<'a> fn((), u32)>,
{
}

fn main() {
    foo::<Ty1, Ty2>();
}

however, it seems like rustc generally has issues with both of these impls, so it actually believes that none of these impls apply 😁 see also #102047 where the first impl results in an ICE.

lcnr · 2022-09-20T11:53:35Z

cc @rust-lang/types

BoxyUwU · 2022-09-20T11:59:00Z

#96912 fixes this but it'll be a while before it can be merged

apiraino · 2022-09-20T14:07:09Z

WG-prioritization assigning priority (Zulip discussion).

@rustbot label -I-prioritize +P-medium

lcnr · 2023-11-06T09:59:18Z

This is also wrong if only region arguments differ:

trait Trait<T> {}

trait WithAssoc<'a> {
    type Assoc;
}

impl<T: for<'a> WithAssoc<'a>> Trait<T> for for<'a> fn(<T as WithAssoc<'a>>::Assoc) {}

impl<'a, T: WithAssoc<'a>> Trait<T> for fn(<T as WithAssoc<'a>>::Assoc) {}

stabilize `-Znext-solver=coherence` TODO: - [ ] go through all issues in https://github.com/rust-lang/trait-system-refactor-initiative/issues again to check whether anything was missed - [ ] crater run + perf - [ ] finish the FCP proposal, fill in acknowledgements (want to avoid pinging people before this is ready r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable, to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that it's current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars fixes rust-lang#102048 In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals - rust-lang#114061 TODO: may get fixed by rust-lang#117164 before then ### Applying inference constraints during the implicit-negative check In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820. (TODO: move to dev-guide). In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore does not currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is a potential future compatability issue. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} fn main() {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This is necessary as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. However, normalization does not eagerly evaluate the nested bounds of impls in the old solver. The constraints from normalizing a type can result in an error without ever having to evaluate the nested bounds. Always discarding constraints on overflow is a breaking change. To avoid this while still avoiding many hangs we apply constraints only inside of `NormalizesTo` goals, unless they are from a where-bound: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs#L381-L417). This is necessary for the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Change the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to be close to being as strong enough to avoid accidental hangs in nearly all cases. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. TODO: how close can we get to a perf run using the new solver? We are still unable to compile the full benchmark suite when fully enabling the new trait solver. Even without any micro optimizations, the performance of the new solver seems to already match the old one. TODO: link There are very rare cases where non-fatal overflow and the removal of the `fn match_fresh_trait_refs` approximation result in significantly worse performance. Most notably, we believe that [`typenum`](https://crates.io/crates/typenum) should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Its performance is currently TODO cmp coherence, cmp full. Due to an improved structure and far better caching, we believe that there is still a significant room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. TODO - [ ] crater - [ ] look through https://github.com/rust-lang/trait-system-refactor-initiative/issues again - [ ] finish perf section of the FCP - [ ] more deep dives for the solver r? `@compiler-errors` ---- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable, to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that it's current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars fixes rust-lang#102048 In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals - rust-lang#114061 TODO: may get fixed by rust-lang#117164 before then ### Applying inference constraints during the implicit-negative check In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820. (TODO: move to dev-guide). In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore does not currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is a potential future compatability issue. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} fn main() {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This is necessary as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. However, normalization does not eagerly evaluate the nested bounds of impls in the old solver. The constraints from normalizing a type can result in an error without ever having to evaluate the nested bounds. Always discarding constraints on overflow is a breaking change. To avoid this while still avoiding many hangs we apply constraints only inside of `NormalizesTo` goals, unless they are from a where-bound: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs#L381-L417). This is necessary for the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Change the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to be close to being as strong enough to avoid accidental hangs in nearly all cases. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. TODO: how close can we get to a perf run using the new solver? We are still unable to compile the full benchmark suite when fully enabling the new trait solver. Even without any micro optimizations, the performance of the new solver seems to already match the old one. TODO: link There are very rare cases where non-fatal overflow and the removal of the `fn match_fresh_trait_refs` approximation result in significantly worse performance. Most notably, we believe that [`typenum`](https://crates.io/crates/typenum) should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Its performance is currently TODO cmp coherence, cmp full. Due to an improved structure and far better caching, we believe that there is still a significant room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements TODO

stabilize `-Znext-solver=coherence` TODO: - [ ] go through all issues in https://github.com/rust-lang/trait-system-refactor-initiative/issues again to check whether anything was missed - [ ] crater run + perf - [ ] finish the FCP proposal, fill in acknowledgements (want to avoid pinging people before this is ready) - [ ] some additional t-types sync deep-dives for the solver r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable, to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that it's current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars fixes rust-lang#102048 In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals - rust-lang#114061 TODO: may get fixed by rust-lang#117164 before then ### Applying inference constraints during the implicit-negative check In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820. (TODO: move to dev-guide). In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore does not currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} ``` ```rust // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is a potential future compatability issue. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} fn main() {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This is necessary as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. However, normalization does not eagerly evaluate the nested bounds of impls in the old solver. The constraints from normalizing a type can result in an error without ever having to evaluate the nested bounds. Always discarding constraints on overflow is a breaking change. To avoid this while still avoiding many hangs we apply constraints only inside of `NormalizesTo` goals, unless they are from a where-bound: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs#L381-L417). This is necessary for the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Change the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to be close to being as strong enough to avoid accidental hangs in nearly all cases. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. TODO: how close can we get to a perf run using the new solver? We are still unable to compile the full benchmark suite when fully enabling the new trait solver. Even without any micro optimizations, the performance of the new solver seems to already match the old one. TODO: link There are very rare cases where non-fatal overflow and the removal of the `fn match_fresh_trait_refs` approximation result in significantly worse performance. Most notably, we believe that [`typenum`](https://crates.io/crates/typenum) should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Its performance is currently TODO cmp coherence, cmp full. Due to an improved structure and far better caching, we believe that there is still a significant room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements TODO

stabilize `-Znext-solver=coherence` TODO: - [ ] finish the FCP proposal, fill in acknowledgements (want to avoid pinging people before this is ready) - [ ] some additional t-types sync deep-dives for the solver r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable, to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that it's current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars fixes rust-lang#102048 In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals - rust-lang#114061 TODO: may get fixed by rust-lang#117164 before then ### Applying inference constraints during the implicit-negative check In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` ### Breakage due to removal of incomplete candidate preference In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { type Assoc = usize; } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820. (TODO: move to dev-guide). In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore does not currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} ``` ```rust // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is a potential future compatability issue. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} fn main() {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This is necessary as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. However, normalization does not eagerly evaluate the nested bounds of impls in the old solver. The constraints from normalizing a type can result in an error without ever having to evaluate the nested bounds. Always discarding constraints on overflow is a breaking change. To avoid this while still avoiding many hangs we apply constraints only inside of `NormalizesTo` goals, unless they are from a where-bound: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs#L381-L417). This is necessary for the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Change the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to be close to being as strong enough to avoid accidental hangs in nearly all cases. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. TODO: how close can we get to a perf run using the new solver? We are still unable to compile the full benchmark suite when fully enabling the new trait solver. Even without any micro optimizations, the performance of the new solver seems to already match the old one. TODO: link There are very rare cases where non-fatal overflow and the removal of the `fn match_fresh_trait_refs` approximation result in significantly worse performance. Most notably, we believe that [`typenum`](https://crates.io/crates/typenum) should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Its performance is currently TODO cmp coherence, cmp full. Due to an improved structure and far better caching, we believe that there is still a significant room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements TODO

stabilize `-Znext-solver=coherence` r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable, to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that it's current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars fixes rust-lang#102048 In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals - rust-lang#114061 TODO: may get fixed by rust-lang#117164 before then ### Applying inference constraints during the implicit-negative check In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` ### Breakage due to removal of incomplete candidate preference In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { type Assoc = usize; } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820. (TODO: move to dev-guide). In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore does not currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} ``` ```rust // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is a potential future compatability issue. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} fn main() {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This is necessary as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. However, normalization does not eagerly evaluate the nested bounds of impls in the old solver. The constraints from normalizing a type can result in an error without ever having to evaluate the nested bounds. Always discarding constraints on overflow is a breaking change. To avoid this while still avoiding many hangs we apply constraints only inside of `NormalizesTo` goals, unless they are from a where-bound: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs#L381-L417). This is necessary for the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Change the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to be close to being as strong enough to avoid accidental hangs in nearly all cases. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. TODO: how close can we get to a perf run using the new solver? We are still unable to compile the full benchmark suite when fully enabling the new trait solver. Even without any micro optimizations, the performance of the new solver seems to already match the old one. TODO: link There are very rare cases where non-fatal overflow and the removal of the `fn match_fresh_trait_refs` approximation result in significantly worse performance. Most notably, we believe that [`typenum`](https://crates.io/crates/typenum) should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Its performance is currently TODO cmp coherence, cmp full. Due to an improved structure and far better caching, we believe that there is still a significant room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements TODO

stabilize `-Znext-solver=coherence` r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`: rust-lang#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang#117164. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes rust-lang#107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide once that PR lands :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. TODO: get some rough results here and put them in a table ### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

stabilize `-Znext-solver=coherence` r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`: rust-lang#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang#117164. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes rust-lang#107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide once that PR lands :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. TODO: get some rough results here and put them in a table ### Unstable features #### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. #### fixes to `#![feature(specialization)]` - fixes rust-lang#105782 - fixes rust-lang#118987 #### fixes to `#![feature(type_alias_impl_trait)]` - fixes rust-lang#119272 - rust-lang#105787 (comment) ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

…er-errors stabilize `-Znext-solver=coherence` r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`, fixing rust-lang#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang#117164. This change breaks the [`derive-visitor`](https://crates.io/crates/derive-visitor) crate. I have opened an issue in that repo: nikis05/derive-visitor#16. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes rust-lang#107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide once that PR lands :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. TODO: get some rough results here and put them in a table ### Unstable features #### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. #### fixes to `#![feature(specialization)]` - fixes rust-lang#105782 - fixes rust-lang#118987 #### fixes to `#![feature(type_alias_impl_trait)]` - fixes rust-lang#119272 - rust-lang#105787 (comment) - fixes rust-lang#124207 ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

stabilize `-Znext-solver=coherence` try-job: x86_64-fuchsia r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`, fixing rust-lang#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang#117164. This change breaks the [`derive-visitor`](https://crates.io/crates/derive-visitor) crate. I have opened an issue in that repo: nikis05/derive-visitor#16. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes rust-lang#107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide once that PR lands :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. TODO: get some rough results here and put them in a table ### Unstable features #### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. #### fixes to `#![feature(specialization)]` - fixes rust-lang#105782 - fixes rust-lang#118987 #### fixes to `#![feature(type_alias_impl_trait)]` - fixes rust-lang#119272 - rust-lang#105787 (comment) - fixes rust-lang#124207 ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

stabilize `-Znext-solver=coherence` r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`, fixing rust-lang#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang#117164. This change breaks the [`derive-visitor`](https://crates.io/crates/derive-visitor) crate. I have opened an issue in that repo: nikis05/derive-visitor#16. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes rust-lang#107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal in rust-lang#119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide once that PR lands :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. TODO: get some rough results here and put them in a table ### Unstable features #### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. #### fixes to `#![feature(specialization)]` - fixes rust-lang#105782 - fixes rust-lang#118987 #### fixes to `#![feature(type_alias_impl_trait)]` - fixes rust-lang#119272 - rust-lang#105787 (comment) - fixes rust-lang#124207 ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

stabilize `-Znext-solver=coherence` again r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. Closes rust-lang#114862. This is a direct copy of rust-lang#121848 which has been reverted due to a hang in `nalgebra`: rust-lang#130056. This hang should have been fixed by rust-lang#130617. See the added section in the stabilization report containing user facing changes merged since the original FCP. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`, fixing rust-lang#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang#117164. This change breaks the [`derive-visitor`](https://crates.io/crates/derive-visitor) crate. I have opened an issue in that repo: nikis05/derive-visitor#16. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes rust-lang#107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal rust-lang#119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. TODO: get some rough results here and put them in a table ### Unstable features #### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. #### fixes to `#![feature(specialization)]` - fixes rust-lang#105782 - fixes rust-lang#118987 #### fixes to `#![feature(type_alias_impl_trait)]` - fixes rust-lang#119272 - rust-lang#105787 (comment) - fixes rust-lang#124207 ### Important changes since the original FCP rust-lang#127574 changes the coherence unknowable candidate to only apply if all the super trait bounds may hold. This allows more code to compile and fixes a regression in `pyella` rust-lang#130617 bails with ambiguity if the query response would contain too many non-region inference variables. This should only be triggered in case the result contains a lot of ambiguous aliases in which case further constraining the goal should resolve this. This PR prevents the hang in `nalgebra`. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

lcnr · 2024-09-25T07:00:02Z

what happened here? cc @rust-lang/infra @lnicola it looks like this got closed by a repeated auto merge or sth? The PR closing this issue has been reverted 🤔

kennytm · 2024-09-25T07:18:38Z

@lcnr 3 weeks ago this issue was closed by commit 17b322f of #121848. The commit message contains the magic phrase "fixes #xxxx":

...

#### Structurally relating aliases containing bound vars

Fixes #102048. In the existing solver relating ambiguous projections containing bound variables is structural. ...

So after the PR is merged this issue is closed.

Then, 30 minutes ago, the rust-analyzer repo synchronized commits from the rust repo in rust-lang/rust-analyzer#18183, and the above #121848 PR got included as rust-lang/rust-analyzer@0fba741.

Since @bors has privilege on both repositories, GitHub somehow considers merging rust-lang/rust-analyzer@0fba741 means this issue is fixed and thus closing the issue.

lnicola · 2024-09-25T07:47:25Z

Yeah, sorry, I don't know if we can avoid those, josh-project/josh#1328.

CC @RalfJung are you doing anything special to prevent bors from closing issues left and right?

RalfJung · 2024-09-25T07:57:04Z

We didn't have trouble with bors closing issues yet. But that may be because Miri's issue numbers are still in the 4 digit range.

lnicola · 2024-09-25T08:00:03Z

This wasn't a conflict with the r-a issue numbers, it was a rust-lang/rust issue that was closed, reopened, then closed by bors because of a merge commit into r-a.

RalfJung · 2024-09-25T08:02:25Z

Ah, yeah that happens every now and then also when people with "close" permissions push these kinds of PRs to their forks, or things like that. It's quite annoying but not unique to josh.

IMO ideally github would entirely ignore commit messages and only look at PR descriptions, since we anyway have a PR-only workflow.

stabilize `-Znext-solver=coherence` again r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang#114862. Closes rust-lang#114862. This is a direct copy of rust-lang#121848 which has been reverted due to a hang in `nalgebra`: rust-lang#130056. This hang should have been fixed by rust-lang#130617 and rust-lang#130821. See the added section in the stabilization report containing user facing changes merged since the original FCP. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`, fixing rust-lang#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang#117164. This change breaks the [`derive-visitor`](https://crates.io/crates/derive-visitor) crate. I have opened an issue in that repo: nikis05/derive-visitor#16. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes rust-lang#107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal rust-lang#119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. ### Unstable features #### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. #### fixes to `#![feature(specialization)]` - fixes rust-lang#105782 - fixes rust-lang#118987 #### fixes to `#![feature(type_alias_impl_trait)]` - fixes rust-lang#119272 - rust-lang#105787 (comment) - fixes rust-lang#124207 ### Important changes since the original FCP rust-lang#127574 changes the coherence unknowable candidate to only apply if all the super trait bounds may hold. This allows more code to compile and fixes a regression in `pyella` rust-lang#130617 bails with ambiguity if the query response would contain too many non-region inference variables. This should only be triggered in case the result contains a lot of ambiguous aliases in which case further constraining the goal should resolve this. rust-lang#130821 adds caching to a lot of type folders, which is necessary to handle exponentially large types and handles the hang in `nalgebra` together with rust-lang#130617. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

saethlin · 2024-10-09T23:07:27Z

Ugh, this again. Maybe I should just change my workflow so this stops happening. Sorry for the noise.

…rors stabilize `-Znext-solver=coherence` again r? `@compiler-errors` --- This PR stabilizes the use of the next generation trait solver in coherence checking by enabling `-Znext-solver=coherence` by default. More specifically its use in the *implicit negative overlap check*. The tracking issue for this is rust-lang/rust#114862. Closes #114862. This is a direct copy of #121848 which has been reverted due to a hang in `nalgebra`: #130056. This hang should have been fixed by #130617 and #130821. See the added section in the stabilization report containing user facing changes merged since the original FCP. ## Background ### The next generation trait 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 is intended to replace the existing *evaluate*, *fulfill*, and *project* implementation. It also has a wider impact on the rest of the type system, for example by changing our approach to handling associated types. For a more detailed explanation of the new trait solver, see the [rustc-dev-guide](https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html). This does not stabilize the current behavior of the new trait solver, only the behavior impacting the implicit negative overlap check. There are many areas in the new solver which are not yet finalized. We are confident that their final design will not conflict with the user-facing behavior observable via coherence. More on that further down. Please check out [the chapter](https://rustc-dev-guide.rust-lang.org/solve/significant-changes.html) summarizing the most significant changes between the existing and new implementations. ### Coherence and the implicit negative overlap check Coherence checking detects any overlapping impls. Overlapping trait impls always error while overlapping inherent impls result in an error if they have methods with the same name. Coherence also results in an error if any other impls could exist, even if they are currently unknown. This affects impls which may get added to upstream crates in a backwards compatible way and impls from downstream crates. Coherence failing to detect overlap is generally considered to be unsound, even if it is difficult to actually get runtime UB this way. It is quite easy to get ICEs due to bugs in coherence. 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. The overlap check has to *prove that unifying the impls does not succeed*. This means that **incorrectly getting a type error during coherence is unsound** as it would allow impls to overlap: coherence has to be *complete*. Completeness means that we never incorrectly error. This means that during coherence we must only add inference constraints if they are definitely necessary. During ordinary type checking [this does not hold](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=01d93b592bd9036ac96071cbf1d624a9), so the trait solver has to behave differently, depending on whether we're in coherence or not. 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" as it may get added in another crate, we add an ambiguous candidate: [source](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L858-L883). [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 ## Motivation Replacing the existing solver in coherence fixes soundness bugs by removing sources of incompleteness in the type system. The new solver separately strengthens coherence, resulting in more impls being disjoint and passing the coherence check. The concrete changes will be elaborated further down. We believe the stabilization to reduce the likelihood of future bugs in coherence as the new implementation is easier to understand and reason about. It allows us to remove the support for coherence and implicit-negative reasoning in the old solver, allowing us to remove some code and simplifying the old trait solver. We will only remove the old solver support once this stabilization has reached stable to make sure we're able to quickly revert in case any unexpected issues are detected before then. Stabilizing the use of the next-generation trait solver expresses our confidence that its current behavior is intended and our work towards enabling its use everywhere will not require any breaking changes to the areas used by coherence checking. We are also confident that we will be able to replace the existing solver everywhere, as maintaining two separate systems adds a significant maintainance burden. ## User-facing impact and reasoning ### Breakage due to improved handling of associated types The new solver fixes multiple issues related to associated types. As these issues caused coherence to consider more types distinct, fixing them results in more overlap errors. This is therefore a breaking change. #### Structurally relating aliases containing bound vars Fixes rust-lang/rust#102048. In the existing solver relating ambiguous projections containing bound variables is structural. This is *incomplete* and allows overlapping impls. These was mostly not exploitable as the same issue also caused impls to not apply when trying to use them. The new solver defers alias-relating to a nested goal, fixing this issue: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Trait {} trait Project { type Assoc<'a>; } impl Project for u32 { type Assoc<'a> = &'a u32; } // Eagerly normalizing `<?infer as Project>::Assoc<'a>` is ambiguous, // so the old solver ended up structurally relating // // (?infer, for<'a> fn(<?infer as Project>::Assoc<'a>)) // // with // // ((u32, fn(&'a u32))) // // Equating `&'a u32` with `<u32 as Project>::Assoc<'a>` failed, even // though these types are equal modulo normalization. impl<T: Project> Trait for (T, for<'a> fn(<T as Project>::Assoc<'a>)) {} impl<'a> Trait for (u32, fn(&'a u32)) {} //[next]~^ ERROR conflicting implementations of trait `Trait` for type `(u32, for<'a> fn(&'a u32))` ``` A crater run did not discover any breakage due to this change. #### Unknowable candidates for higher ranked trait goals This avoids an unsoundness by attempting to normalize in `trait_ref_is_knowable`, fixing rust-lang/rust#114061. This is a side-effect of supporting lazy normalization, as that forces us to attempt to normalize when checking whether a `TraitRef` is knowable: [source](https://github.com/rust-lang/rust/blob/47dd709bedda8127e8daec33327e0a9d0cdae845/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L754-L764). ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait IsUnit {} impl IsUnit for () {} pub trait WithAssoc<'a> { type Assoc; } // We considered `for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit` // to be knowable, even though the projection is ambiguous. pub trait Trait {} impl<T> Trait for T where T: 'static, for<'a> T: WithAssoc<'a>, for<'a> <T as WithAssoc<'a>>::Assoc: IsUnit, { } impl<T> Trait for Box<T> {} //[next]~^ ERROR conflicting implementations of trait `Trait` ``` The two impls of `Trait` overlap given the following downstream crate: ```rust use dep::*; struct Local; impl WithAssoc<'_> for Box<Local> { type Assoc = (); } ``` There a similar coherence unsoundness caused by our handling of aliases which is fixed separately in rust-lang/rust#117164. This change breaks the [`derive-visitor`](https://crates.io/crates/derive-visitor) crate. I have opened an issue in that repo: nikis05/derive-visitor#16. ### Evaluating goals to a fixpoint and applying inference constraints In the old implementation of the implicit-negative check, each obligation is [checked separately without applying its inference constraints](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L323-L338). The new solver instead [uses a `FulfillmentCtxt`](https://github.com/rust-lang/rust/blob/bea5bebf3defc56e5e3446b4a95c685dbb885fd3/compiler/rustc_trait_selection/src/traits/coherence.rs#L315-L321) for this, which evaluates all obligations in a loop until there's no further inference progress. This is necessary for backwards compatibility as we do not eagerly normalize with the new solver, resulting in constraints from normalization to only get applied by evaluating a separate obligation. This also allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Mirror { type Assoc; } impl<T> Mirror for T { type Assoc = T; } trait Foo {} trait Bar {} // The self type starts out as `?0` but is constrained to `()` // due to the where-clause below. Because `(): Bar` is known to // not hold, we can prove the impls disjoint. impl<T> Foo for T where (): Mirror<Assoc = T> {} //[current]~^ ERROR conflicting implementations of trait `Foo` for type `()` impl<T> Foo for T where T: Bar {} fn main() {} ``` The old solver does not run nested goals to a fixpoint in evaluation. The new solver does do so, strengthening inference and improving the overlap check: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait Foo {} impl<T> Foo for (u8, T, T) {} trait NotU8 {} trait Bar {} impl<T, U: NotU8> Bar for (T, T, U) {} trait NeedsFixpoint {} impl<T: Foo + Bar> NeedsFixpoint for T {} impl NeedsFixpoint for (u8, u8, u8) {} trait Overlap {} impl<T: NeedsFixpoint> Overlap for T {} impl<T, U: NotU8, V> Overlap for (T, U, V) {} //[current]~^ ERROR conflicting implementations of trait `Foo` ``` ### Breakage due to removal of incomplete candidate preference Fixes #107887. In the old solver we incompletely prefer the builtin trait object impl over user defined impls. This can break inference guidance, inferring `?x` in `dyn Trait<u32>: Trait<?x>` to `u32`, even if an explicit impl of `Trait<u64>` also exists. This caused coherence to incorrectly allow overlapping impls, resulting in ICEs and a theoretical unsoundness. See rust-lang/rust#107887 (comment). This compiles on stable but results in an overlap error with `-Znext-solver=coherence`: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence struct W<T: ?Sized>(*const T); trait Trait<T: ?Sized> { type Assoc; } // This would trigger the check for overlap between automatic and custom impl. // They actually don't overlap so an impl like this should remain possible // forever. // // impl Trait<u64> for dyn Trait<u32> {} trait Indirect {} impl Indirect for dyn Trait<u32, Assoc = ()> {} impl<T: Indirect + ?Sized> Trait<u64> for T { type Assoc = (); } // Incomplete impl where `dyn Trait<u32>: Trait<_>` does not hold, but // `dyn Trait<u32>: Trait<u64>` does. trait EvaluateHack<U: ?Sized> {} impl<T: ?Sized, U: ?Sized> EvaluateHack<W> for T where T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` U: IsU64, T: Trait<U, Assoc = ()>, // incompletely constrains `_` to `u32` { } trait IsU64 {} impl IsU64 for u64 {} trait Overlap<U: ?Sized> { type Assoc: Default; } impl<T: ?Sized + EvaluateHack<W>, U: ?Sized> Overlap for T { type Assoc = Box<u32>; } impl<U: ?Sized> Overlap for dyn Trait<u32, Assoc = ()> { //[next]~^ ERROR conflicting implementations of trait `Overlap<_>` type Assoc = usize; } ``` ### Considering region outlives bounds in the `leak_check` For details on the `leak_check`, see the FCP proposal #119820.[^leak_check] [^leak_check]: which should get moved to the dev-guide :3 In both coherence and during candidate selection, the `leak_check` relies on the region constraints added in `evaluate`. It therefore currently does not register outlives obligations: [source](https://github.com/rust-lang/rust/blob/ccb1415eac3289b5ebf64691c0190dc52e0e3d0e/compiler/rustc_trait_selection/src/traits/select/mod.rs#L792-L810). This was likely done as a performance optimization without considering its impact on the `leak_check`. This is the case as in the old solver, *evaluatation* and *fulfillment* are split, with evaluation being responsible for candidate selection and fulfillment actually registering all the constraints. This split does not exist with the new solver. The `leak_check` can therefore eagerly detect errors caused by region outlives obligations. This improves both coherence itself and candidate selection: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence trait LeakErr<'a, 'b> {} // Using this impl adds an `'b: 'a` bound which results // in a higher-ranked region error. This bound has been // previously ignored but is now considered. impl<'a, 'b: 'a> LeakErr<'a, 'b> for () {} trait NoOverlapDir<'a> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> NoOverlapDir<'a> for T {} impl<'a> NoOverlapDir<'a> for () {} //[current]~^ ERROR conflicting implementations of trait `NoOverlapDir<'_>` // -------------------------------------- // necessary to avoid coherence unknowable candidates struct W<T>(T); trait GuidesSelection<'a, U> {} impl<'a, T: for<'b> LeakErr<'a, 'b>> GuidesSelection<'a, W<u32>> for T {} impl<'a, T> GuidesSelection<'a, W<u8>> for T {} trait NotImplementedByU8 {} trait NoOverlapInd<'a, U> {} impl<'a, T: GuidesSelection<'a, W>, U> NoOverlapInd<'a, U> for T {} impl<'a, U: NotImplementedByU8> NoOverlapInd<'a, U> for () {} //[current]~^ conflicting implementations of trait `NoOverlapInd<'_, _>` ``` ### Removal of `fn match_fresh_trait_refs` The old solver tries to [eagerly detect unbounded recursion](https://github.com/rust-lang/rust/blob/b14fd2359f47fb9a14bbfe55359db4bb3af11861/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1196-L1211), forcing the affected goals to be ambiguous. This check is only an approximation and has not been added to the new solver. The check is not necessary in the new solver and it would be problematic for caching. As it depends on all goals currently on the stack, using a global cache entry would have to always make sure that doing so does not circumvent this check. This changes some goals to error - or succeed - instead of failing with ambiguity. This allows more code to compile: ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence // Need to use this local wrapper for the impls to be fully // knowable as unknowable candidate result in ambiguity. struct Local<T>(T); trait Trait {} // This impl does not hold, but is ambiguous in the old // solver due to its overflow approximation. impl Trait for Local<u32> where Local<u16>: Trait {} // This impl holds. impl Trait<Local<()>> for Local<u8> {} // In the old solver, `Local<?t>: Trait<Local<?u>>` is ambiguous, // resulting in `Local<?u>: NoImpl`, also being ambiguous. // // In the new solver the first impl does not apply, constraining // `?u` to `Local<()>`, causing `Local<()>: NoImpl` to error. trait Indirect<T> {} impl<T, U> Indirect for T where T: Trait, U: NoImpl {} // Not implemented for `Local<()>` trait NoImpl {} impl NoImpl for Local<u8> {} impl NoImpl for Local<u16> {} // `Local<?t>: Indirect<Local<?u>>` cannot hold, so // these impls do not overlap. trait NoOverlap {} impl<T: Indirect, U> NoOverlap for T {} impl<T, U> NoOverlap<Local> for Local<T> {} //~^ ERROR conflicting implementations of trait `NoOverlap<Local<_>>` ``` ### Non-fatal overflow The old solver immediately emits a fatal error when hitting the recursion limit. The new solver instead returns overflow. This both allows more code to compile and is results in performance and potential future compatability issues. Non-fatal overflow is generally desirable. With fatal overflow, changing the order in which we evaluate nested goals easily causes breakage if we have goal which errors and one which overflows. It is also required to prevent breakage due to the removal of `fn match_fresh_trait_refs`, e.g. [in `typenum`](rust-lang/trait-system-refactor-initiative#73). #### Enabling more code to compile In the below example, the old solver first tried to prove an overflowing goal, resulting in a fatal error. The new solver instead returns ambiguity due to overflow for that goal, causing the implicit negative overlap check to succeed as `Box<u32>: NotImplemented` does not hold. ```rust // revisions: current next //[next] compile-flags: -Znext-solver=coherence //[current] ERROR overflow evaluating the requirement trait Indirect<T> {} impl<T: Overflow<()>> Indirect<T> for () {} trait Overflow {} impl<T, U> Overflow for Box<T> where U: Indirect<Box<Box<T>>>, {} trait NotImplemented {} trait Trait {} impl<T, U> Trait for T where // T: NotImplemented, // causes old solver to succeed U: Indirect<T>, T: NotImplemented, {} impl Trait<()> for Box<u32> {} ``` #### Avoiding hangs with non-fatal overflow Simply returning ambiguity when reaching the recursion limit can very easily result in hangs, e.g. ```rust trait Recur {} impl<T, U> Recur for ((T, U), (U, T)) where (T, U): Recur, (U, T): Recur, {} trait NotImplemented {} impl<T: NotImplemented> Recur for T {} ``` This can happen quite frequently as it's easy to have exponential blowup due to multiple nested goals at each step. As the trait solver is depth-first, this immediately caused a fatal overflow error in the old solver. In the new solver we have to handle the whole proof tree instead, which can very easily hang. To avoid this we restrict the recursion depth after hitting the recursion limit for the first time. We also **ignore all inference constraints from goals resulting in overflow**. This is mostly backwards compatible as any overflow in the old solver resulted in a fatal error. ### sidenote about normalization We return ambiguous nested goals of `NormalizesTo` goals to the caller and ignore their impact when computing the `Certainty` of the current goal. See the [normalization chapter](https://rustc-dev-guide.rust-lang.org/solve/normalization.html) for more details.This means we apply constraints resulting from other nested goals and from equating the impl header when normalizing, even if a nested goal results in overflow. This is necessary to avoid breaking the following example: ```rust trait Trait { type Assoc; } struct W<T: ?Sized>(*mut T); impl<T: ?Sized> Trait for W<W<T>> where W<T>: Trait, { type Assoc = (); } // `W<?t>: Trait<Assoc = u32>` does not hold as // `Assoc` gets normalized to `()`. However, proving // the where-bounds of the impl results in overflow. // // For this to continue to compile we must not discard // constraints from normalizing associated types. trait NoOverlap {} impl<T: Trait<Assoc = u32>> NoOverlap for T {} impl<T: ?Sized> NoOverlap for W<T> {} ``` #### Future compatability concerns Non-fatal overflow results in some unfortunate future compatability concerns. Changing the approach to avoid more hangs by more strongly penalizing overflow can cause breakage as we either drop constraints or ignore candidates necessary to successfully compile. Weakening the overflow penalities instead allows more code to compile and strengthens inference while potentially causing more code to hang. While the current approach is not perfect, we believe it to be good enough. We believe it to apply the necessary inference constraints to avoid breakage and expect there to not be any desirable patterns broken by our current penalities. Similarly we believe the current constraints to avoid most accidental hangs. Ignoring constraints of overflowing goals is especially useful, as it may allow major future optimizations to our overflow handling. See [this summary](https://hackmd.io/ATf4hN0NRY-w2LIVgeFsVg) and the linked documents in case you want to know more. ### changes to performance In general, trait solving during coherence checking is not significant for performance. Enabling the next-generation trait solver in coherence does not impact our compile time benchmarks. We are still unable to compile the benchmark suite when fully enabling the new trait solver. There are rare cases where the new solver has significantly worse performance due to non-fatal overflow, its reliance on fixpoint algorithms and the removal of the `fn match_fresh_trait_refs` approximation. We encountered such issues in [`typenum`](https://crates.io/crates/typenum) and believe it should be [pretty much as bad as it can get](rust-lang/trait-system-refactor-initiative#73). Due to an improved structure and far better caching, we believe that there is a lot of room for improvement and that the new solver will outperform the existing implementation in nearly all cases, sometimes significantly. We have not yet spent any time micro-optimizing the implementation and have many unimplemented major improvements, such as fast-paths for trivial goals. ### Unstable features #### Unsupported unstable features The new solver currently does not support all unstable features, most notably `#![feature(generic_const_exprs)]`, `#![feature(associated_const_equality)]` and `#![feature(adt_const_params)]` are not yet fully supported in the new solver. We are confident that supporting them is possible, but did not consider this to be a priority. This stabilization introduces new ICE when using these features in impl headers. #### fixes to `#![feature(specialization)]` - fixes #105782 - fixes #118987 #### fixes to `#![feature(type_alias_impl_trait)]` - fixes #119272 - rust-lang/rust#105787 (comment) - fixes #124207 ### Important changes since the original FCP rust-lang/rust#127574 changes the coherence unknowable candidate to only apply if all the super trait bounds may hold. This allows more code to compile and fixes a regression in `pyella` rust-lang/rust#130617 bails with ambiguity if the query response would contain too many non-region inference variables. This should only be triggered in case the result contains a lot of ambiguous aliases in which case further constraining the goal should resolve this. rust-lang/rust#130821 adds caching to a lot of type folders, which is necessary to handle exponentially large types and handles the hang in `nalgebra` together with #130617. ## This does not stabilize the whole solver While this stabilizes the use of the new solver in coherence checking, there are many parts of the solver which will remain fully unstable. We may still adapt these areas while working towards stabilizing the new solver everywhere. We are confident that we are able to do so without negatively impacting coherence. ### goals with a non-empty `ParamEnv` Coherence always uses an empty environment. We therefore do not depend on the behavior of `AliasBound` and `ParamEnv` candidates. We only stabilizes the behavior of user-defined and builtin implementations of traits. There are still many open questions there. ### opaque types in the defining scope The handling of opaque types - `impl Trait` - in both the new and old solver is still not fully figured out. Luckily this can be ignored for now. While opaque types are reachable during coherence checking by using `impl_trait_in_associated_types`, the behavior during coherence is separate and self-contained. The old and new solver fully agree here. ### normalization is hard This stabilizes that we equate associated types involving bound variables using deferred-alias-equality. We also stop eagerly normalizing in coherence, which should not have any user-facing impact. We do not stabilize the normalization behavior outside of coherence, e.g. we currently deeply normalize all types during writeback with the new solver. This may change going forward ### how to replace `select` from the old solver We sometimes depend on getting a single `impl` for a given trait bound, e.g. when resolving a concrete method for codegen/CTFE. We do not depend on this during coherence, so the exact approach here can still be freely changed going forward. ## Acknowledgements This work would not have been possible without `@compiler-errors.` He implemented large chunks of the solver himself but also and did a lot of testing and experimentation, eagerly discovering multiple issues which had a significant impact on our approach. `@BoxyUwU` has also done some amazing work on the solver. Thank you for the endless hours of discussion resulting in the current approach. Especially the way aliases are handled has gone through multiple revisions to get to its current state. There were also many contributions from - and discussions with - other members of the community and the rest of `@rust-lang/types.` This solver builds upon previous improvements to the compiler, as well as lessons learned from `chalk` and `a-mir-formality`. Getting to this point would not have been possible without that and I am incredibly thankful to everyone involved. See the [list of relevant PRs](https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-03-22+).

rustbot added the I-prioritize Issue: Indicates that prioritization has been requested for this issue. label Sep 20, 2022

rustbot added P-medium Medium priority and removed I-prioritize Issue: Indicates that prioritization has been requested for this issue. labels Sep 20, 2022

lcnr mentioned this issue Sep 20, 2022

trait selection fails for projections under binders #102052

Open

gburgessiv mentioned this issue Feb 25, 2023

Add known-bug tests for all(?) I-unsound issues #105107

Closed

lcnr added the fixed-by-next-solver Fixed by the next-generation trait solver, `-Znext-solver`. label Mar 21, 2023

lcnr mentioned this issue Nov 9, 2023

equality of aliases with ambiguous normalization rust-lang/trait-system-refactor-initiative#75

Open

lcnr added this to T-types unsound issues Nov 15, 2023

lcnr moved this to new solver in coherence in T-types unsound issues Nov 15, 2023

lcnr mentioned this issue Jan 11, 2024

more eagerly instantiate binders #119849

Merged

lcnr mentioned this issue Mar 1, 2024

stabilize -Znext-solver=coherence #121848

Merged

bors closed this as completed in 17b322f Sep 6, 2024

github-project-automation bot moved this from new solver in coherence to new solver everywhere in T-types unsound issues Sep 6, 2024

lcnr removed this from T-types unsound issues Sep 11, 2024

lcnr reopened this Sep 13, 2024

lcnr mentioned this issue Sep 21, 2024

stabilize -Znext-solver=coherence again #130654

Merged

bors closed this as completed in rust-lang/rust-analyzer@0fba741 Sep 25, 2024

lcnr reopened this Sep 25, 2024

RalfJung mentioned this issue Sep 25, 2024

Github sometimes closes issues that have been re-opened #130817

Open

saethlin closed this as completed in saethlin/miri@c62efd4 Oct 9, 2024

lqd reopened this Oct 9, 2024

bors closed this as completed in #130654 Oct 15, 2024

bors closed this as completed in a0c2aba Oct 15, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

relating projection substs is unsound during coherence #102048

relating projection substs is unsound during coherence #102048

lcnr commented Sep 20, 2022 •

edited

Loading

lcnr commented Sep 20, 2022

BoxyUwU commented Sep 20, 2022

apiraino commented Sep 20, 2022

lcnr commented Nov 6, 2023

lcnr commented Sep 25, 2024

kennytm commented Sep 25, 2024

lnicola commented Sep 25, 2024

RalfJung commented Sep 25, 2024 via email

lnicola commented Sep 25, 2024

RalfJung commented Sep 25, 2024

saethlin commented Oct 9, 2024 •

edited

Loading

relating projection substs is unsound during coherence #102048

relating projection substs is unsound during coherence #102048

Comments

lcnr commented Sep 20, 2022 • edited Loading

lcnr commented Sep 20, 2022

BoxyUwU commented Sep 20, 2022

apiraino commented Sep 20, 2022

lcnr commented Nov 6, 2023

lcnr commented Sep 25, 2024

kennytm commented Sep 25, 2024

lnicola commented Sep 25, 2024

RalfJung commented Sep 25, 2024 via email

lnicola commented Sep 25, 2024

RalfJung commented Sep 25, 2024

saethlin commented Oct 9, 2024 • edited Loading

lcnr commented Sep 20, 2022 •

edited

Loading

saethlin commented Oct 9, 2024 •

edited

Loading