We sometimes make decisions during type inference which are not strictly necessary, i.e. we constrain inference variables to some specific type even though another type may be equally as valid. For example:

fn impl_trait() -> impl Into<u32> {
    0u16
}

fn main() {
    // There are two possible types for `x`:
    // - `u32` by using the "alias bound" of `impl Into<u32>`
    // - `impl Into<u32>`, i.e. `u16`, by using `impl<T> From<T> for T`
    //
    // We infer the type of `x` to be `u32` here as it is highly likely
    // that this is expected by the user.
    let x = impl_trait().into();
    println!("{}", std::mem::size_of_val(&x));
}

This behavior can result in unexpected errors in case we incorrectly guide inference. It also causes trait solving to be order dependent. It mostly happens in places where we have multiple valid ways - candidates - to prove a given goal and choose a single one of them. The exact way we prefer candidates is deeply intertwined with the inner workings on the trait solver and cannot trivially be emulated in the new solver.

## there must not be incompleteness in coherence

Coherence must not have any incompleteness as incompleteness can result in incorrect errors which can be used to allow overlapping impls.

Outside of coherence we rely on incompleteness for things to work™, to match the behavior expected by users, and for backwards compatible reasons.

## `select` in the new solver

Unlike the current trait solver, candidate selection is not a fundamental part of the new trait solver. The new trait solver instead tries to merge its different candidates: https://github.com/rust-lang/rust/blob/1a449dcfd25143f7e1f6b6f5ddf1c12af361e2ff/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L760-L797.

We do however also need something closer to the current selection behavior:
- get a single candidate (incompletely prefering some over others)
- return the nested obligations of that candidate

The most notable place where this behavior is needed is `coerce_unsized`: https://github.com/rust-lang/rust/blob/1a449dcfd25143f7e1f6b6f5ddf1c12af361e2ff/compiler/rustc_hir_typeck/src/coercion.rs#L602-L706. This implements its own, completely separate fulfillment loop with special behavior to decide whether or not an unsize coercion should take place. Rewriting this fulfillment loop to not rely on the existing behavior of`select` while mostly being backwards compatible is a difficult issue and I expect it to require a significant time investment.

Because of the above, with the new solver we implemented a `select` which lives *outside* of the trait solver and has the same behavior as the old select: https://github.com/rust-lang/rust/blob/1a449dcfd25143f7e1f6b6f5ddf1c12af361e2ff/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L760-L797

This means that the way incompleteness is handled inside of the solver, e.g. by trait goals, is separate from how it is handled by `select` (which is used by method probing and coercions).

## Incompleteness inside of the trait solver

Outside of select which currently matches the behavior of the old solver, the trait solver itself is currently incomplete in 3 different places. We always first try to merge all options via [`fn try_merge_responses`](https://github.com/rust-lang/rust/blob/a482149598f5aacf3837eee87026dd634f08641c/compiler/rustc_trait_selection/src/solve/mod.rs#L238-L260) and only rely on incompleteness if that fails.

### merging trait and project candidates

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

We prefer candidates from the environment, the exact rules for this are still undecided, see https://github.com/rust-lang/rust/pull/113445 which has the minimal amount of incompleteness here.

#### Case Study: [the order of where clauses](https://github.com/rust-lang/rust/issues/41756)

trait Left<T> {}
impl<T, U> Left<U> for T {}

trait Right<T> {}
impl<T, U> Right<U> for T {}

trait Join<U> {
    fn test();
}

// With the reordering,
//   impl<T, U> Join<U> for T where T: Right<U>, T: Left<U> {
// you'll get a different output
impl<T, U> Join<U> for T where T: Left<U>, T: Right<U> {
    fn test() {
        println!("{}", std::any::type_name::<U>());
    }
}

fn impls_join<T: Join<U>, U>() {
    println!("{}", std::any::type_name::<U>());
}

fn try_it<T>() where T: Left<bool>, T: Right<()> {
    // Both entering the trait solver via select and
    // ordinary trait solving have the same result, as
    // a nested goal is resposible for the incompleteness.
    <T as Join<_>>::test();
    impls_join::<T, _>();
}

fn main() {
    try_it::<u8>() // the type here is irrelevant
}

https://rust.godbolt.org/z/rajs4seb5

We have the following proof tree for this example:
- goal: `T: Join<?U> where T: Left<bool>, T: Right<()>`
- impl: `impl<T, U> Join<U>`
- nested goal: `T: Left<?U>`
- proven via impl: AMBIG, no constraints (`?U: Sized` bound)
- proven via param env: OK, `?U == bool`
- a complete solver would return AMBIG
- prefering param env candidates and constrains `?U` to `bool`
- nested goal: `T: Right<bool>` (after incomplete previous goal)
- proven via impl: OK
- param env candidate `T: Right<()>` does not apply

If we instead first check `T: Right<?U>` we would incompletely constrain `?U` to `()`.

### alias-relate bidrectional normalization

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

If we have an `AliasRelate` goal with normalizeable aliases on both sides it's often possible to prove it by both first normalize the lhs and then the rhs or the other way around. These two candidates end up having subtly different responses, e.g. they can differ in whether a type is normalized in the inference constraints.

trait Trait {
    type Assoc;
    fn assoc(&self) -> &Self::Assoc;
}

struct Foo<'a>(&'a str);
impl<'a> Trait for Foo<'a> {
    type Assoc = Foo<'a>;
    fn assoc(&self) -> &Self::Assoc {
        self
    }
}

fn main() {
    let origin = Foo("hi");
    let target = if false {
        origin.assoc()
    } else {
        origin.assoc()
    };
}

would result in

error[E0284]: type annotations needed: cannot satisfy `<Foo<'_> as Trait>::Assoc <: <Foo<'_> as Trait>::Assoc`
  --> src/main.rs:16:18
   |
16 |       let target = if false {
   |  __________________^
17 | |         origin.assoc()
18 | |     } else {
19 | |         origin.assoc()
20 | |     };
   | |_____^ cannot satisfy `<Foo<'_> as Trait>::Assoc <: <Foo<'_> as Trait>::Assoc`

It might be possible to avoid this issue (at least in some cases), by converting the returned region constraints into some "normal form" wrt to the query input which should allow us to merge these responses. I am not sure whether this is possible in the general case.

This is also frequently an issue with opaque types. Given an alias relate goal `AliasRelate(impl Trait, <iter::Empty<i32> as Iterator>::Item)`, should the hidden type of `impl Trait` be `<iter::Empty<i32> as Iterator>::Item` or `i32`? To handle this we add a fourth option to prove `alias-relate` goals: `bidirectional-normalizes-to` https://github.com/rust-lang/rust/blob/55e8df2b0e3c4494b77f2431b912c51e6fe733ba/compiler/rustc_trait_selection/src/solve/alias_relate.rs#L170-L194

This goal is `lhs normalizes-to rhs AND rhs normalizes-to lhs`. If we add keep the requirement of the type system that normalization does not add additional bounds apart from the WF-conditions of the alias, then this shouldn't even be incomplete.

We currently also prefer the `substs-relate` candidate in alias-relate over any `normalizes-to`, but afaict this one is unnecessary if we have `bidirectional-normalizes-to`.

## a stack of questions

### how do I ask a question while reading?

more context for question

lcnr: like this :3

### when do we WANT this behavior?

nikomatsakis: the doc didn't go into cases where env preference is required.

lcnr: doc https://github.com/rust-lang/trait-system-refactor-initiative/issues/45

### what is behavior of solver for the case study?

> Case Study: the order of where clauses

nikomatsakis: It's not spelled out very clearly, or at least I was unsure. I believe the new trait solver *does* exhibit order dependency here, right?

lcnr: yes, but it is not strictly necessary and I have an open PR which changes this and afaict doesn't break anything "important" that I know of https://github.com/rust-lang/rust/pull/113445

use std::fmt::Display;
fn test<T: Display + Into<String>>(t: T) -> String {
    let x = t.into();
    format!("{x}")
}

fn main() {
    test(22)
}

use std::fmt::Display;
fn test<T: Display + Into<String>>(t: T) {
    let x = t.into();
    println!("{x}");
}

fn main() {
    test("test")
}

[another version](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=36e56365ba55c5fe60a759f658ec0ff8)

use std::fmt::Debug;

fn test<T: Debug + Into<String>>(t: T) -> String {
    let x = t.into();
    format!("{x}")
}

#[derive(Debug)]
struct Foo;

impl From<Foo> for String { 
    fn from(x: Foo) -> String { format!("{x:?}") }
}

fn main() {
    test(Foo);
}

what about moving the "arbitrary choice" into type check? This is what chalk was trying to do.

Example: blanket

preference only at the "top level" feels bad, e.g. moving stuff into extension traits can break type inference:

trait Nested<T> {}
impl<T, U> Nested<U> for T {}

trait Root<U> {
    fn test();
}

impl<T, U> Root<U> for T where T: Nested<U> {
    fn test() {
        println!("{}", std::any::type_name::<U>());
    }
}

fn impls_root<T: Root<U>, U>() {
    println!("{}", std::any::type_name::<U>());
}

fn try_it<T>() where T: Nested<bool> {
    // Both entering the trait solver via select and
    // ordinary trait solving have the same result, as
    // a nested goal is resposible for the incompleteness.
    <T as Root<_>>::test();
    impls_root::<T, _>();
}

fn main() {
    try_it::<u8>() // the type here is irrelevant
}

trait Left<T> {}
impl<T, U> Left<U> for T {}

trait Right<T> {}
impl<T, U> Right<U> for T {}

trait Join<U> {
    fn test();
}

// With the reordering,
//   impl<T, U> Join<U> for T where T: Right<U>, T: Left<U> {
// you'll get a different output
impl<T, U> Join<U> for T where T: Left<U>, T: Right<U> {
    fn test() {
        println!("{}", std::any::type_name::<U>());
    }
}

fn impls_join<T: Left<U> + Right<U>, U>() {
    println!("{}", std::any::type_name::<U>());
}

fn try_it<T>() where T: Left<bool>, T: Right<()> {
    impls_join::<T, _>();
}

fn main() {
    try_it::<u8>() // the type here is irrelevant

### normalization behavior

nikomatsakis: In the section ...

> alias-relate bidrectional normalization

it states that normalization can result in subtle errors and gives an example, but I don't understand what is causing this error to arise. When we invoke `origin.assoc()` we get back a return type of `&'x <Foo<'y> as Trait>::Assoc`, and we invoke it twice, once for each branch of the `if`, so they are getting equated... this presumably attempts to normalize... which I would *assume* succeeds...?

lcnr: for `<Foo<'0> as Trait>::Assoc <: <Foo<'1> as Trait>::Assoc`

normalizing `Foo<'a> as Trait>::Assoc` results in some region constraint on `'a` which gets put into an ordered list. So by normalizing with different orders the lists have the same content, but different orders

Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [(OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation)], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }] })
Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [(OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation)], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }] })
Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [(OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation)], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }] })

### "add-keep"

nikomatsakis: from the text:

> If we add keep the requirement of the type system that normalization does not add additional bounds apart from the WF-conditions of the alias, then this shouldn’t even be incomplete.

We don't have this requrement today, right? So presumably it is *add*, and I don't think it's possible to add, because it would narrow down the set of impls we can accept rather dramatically?

lcnr: projections are wf if they implement their trait and the gat where bounds hold. this is exactly what we use to normalize. This stops being the case with https://github.com/rust-lang/trait-system-refactor-initiative/issues/12