Update `traits/resolution.md` (#1494)

* Update `traits/resolution.md`

Co-authored by: @lcnr and @spastorino

* Update src/traits/resolution.md

* Wrapping

* Update src/traits/resolution.md

Co-authored-by: Santiago Pastorino <spastorino@gmail.com>

Co-authored-by: Santiago Pastorino <spastorino@gmail.com>

src/traits/resolution.md

@@ -72,10 +72,10 @@ Trait resolution consists of three major parts:
   are completely fulfilled. Basically it is a worklist of obligations
   to be selected: once selection is successful, the obligation is
   removed from the worklist and any nested obligations are enqueued.
+  Fulfillment constrains inference variables.
 
-- **Coherence**: The coherence checks are intended to ensure that there
+- **Evaluation**: Checks whether obligations holds without constraining
-  are never overlapping impls, where two impls could be used with
+  any inference variables. Used by selection.
-  equal precedence.
 
 ## Selection
 
@@ -111,6 +111,8 @@ may lead to other errors downstream).
 
 ### Candidate assembly
 
+**TODO**: Talk about _why_ we have different candidates, and why it needs to happen in a probe.
+
 Searches for impls/where-clauses/etc that might
 possibly be used to satisfy the obligation. Each of those is called
 a candidate. To avoid ambiguity, we want to find exactly one
@@ -120,69 +122,24 @@ the obligation contains unbound inference variables.
 
 The subroutines that decide whether a particular impl/where-clause/etc applies
 to a particular obligation are collectively referred to as the process of
-_matching_. As of <!-- date-check --> May 2022, this amounts to unifying
+_matching_. For `impl` candidates <!-- date-check: Oct 2022 -->,
-the `Self` types, but in the future we may also recursively consider some of the
+this amounts to unifying the impl header (the `Self` type and the trait arguments)
-nested obligations, in the case of an impl.
+while ignoring  nested obligations. If matching succeeds then we add it
-
+to a set of candidates. There are other rules when assembling candidates for
-**TODO**: what does "unifying the `Self` types" mean? The `Self` of the
+built-in traits such as `Copy`, `Sized`, and `CoerceUnsized`.
-obligation with that of an impl?
-
-The basic idea for candidate assembly is to do a first pass in which
-we identify all possible candidates. During this pass, all that we do
-is try and unify the type parameters. (In particular, we ignore any
-nested where clauses.) Presuming that this unification succeeds, the
-impl is added as a candidate.
 
 Once this first pass is done, we can examine the set of candidates. If
 it is a singleton set, then we are done: this is the only impl in
-scope that could possibly apply. Otherwise, we can winnow down the set
+scope that could possibly apply. Otherwise, we can **winnow** down the set
-of candidates by using where clauses and other conditions. If this
+of candidates by using where clauses and other conditions. Winnowing uses
-reduced set yields a single, unambiguous entry, we're good to go,
+`evaluate_candidate` to check whether the nested obligations may apply. 
+If this still leaves more than 1 candidate, we use ` fn candidate_should_be_dropped_in_favor_of` 
+to prefer some candidates over others. 
+
+
+If this reduced set yields a single, unambiguous entry, we're good to go,
 otherwise the result is considered ambiguous.
 
-#### The basic process: Inferring based on the impls we see
-
-This process is easier if we work through some examples. Consider
-the following trait:
-
-```rust,ignore
-trait Convert<Target> {
-    fn convert(&self) -> Target;
-}
-```
-
-This trait just has one method. It's about as simple as it gets. It
-converts from the (implicit) `Self` type to the `Target` type. If we
-wanted to permit conversion between `isize` and `usize`, we might
-implement `Convert` like so:
-
-```rust,ignore
-impl Convert<usize> for isize { ... } // isize -> usize
-impl Convert<isize> for usize { ... } // usize -> isize
-```
-
-Now imagine there is some code like the following:
-
-```rust,ignore
-let x: isize = ...;
-let y = x.convert();
-```
-
-The call to convert will generate a trait reference `Convert<$Y> for
-isize`, where `$Y` is the type variable representing the type of
-`y`. Of the two impls we can see, the only one that matches is
-`Convert<usize> for isize`. Therefore, we can
-select this impl, which will cause the type of `$Y` to be unified to
-`usize`. (Note that while assembling candidates, we do the initial
-unifications in a transaction, so that they don't affect one another.)
-
-**TODO**: The example says we can "select" the impl, but this section is
-talking specifically about candidate assembly. Does this mean we can sometimes
-skip confirmation? Or is this poor wording?
-**TODO**: Is the unification of `$Y` part of trait resolution or type
-inference? Or is this not the same type of "inference variable" as in type
-inference?
-
 #### Winnowing: Resolving ambiguities
 
 But what happens if there are multiple impls where all the types
@@ -281,38 +238,18 @@ result of selection would be an error.
 Note that the candidate impl is chosen based on the `Self` type, but
 confirmation is done based on (in this case) the `Target` type parameter.
 
-### Selection during translation
+### Selection during codegen
 
 As mentioned above, during type checking, we do not store the results of trait
-selection. At trans time, we repeat the trait selection to choose a particular
+selection. At codegen time, we repeat the trait selection to choose a particular
-impl for each method call. In this second selection, we do not consider any
+impl for each method call. This is done using `fn codegen_select_candidate`. 
-where-clauses to be in scope because we know that each resolution will resolve
+In this second selection, we do not consider any where-clauses to be in scope 
-to a particular impl.
+because we know that each resolution will resolve to a particular impl.
 
-One interesting twist has to do with nested obligations. In general, in trans,
+One interesting twist has to do with nested obligations. In general, in codegen,
-we only need to do a "shallow" selection for an obligation. That is, we wish to
+we only to figure out which candidate applies, we do not care about nested obligations,
-identify which impl applies, but we do not (yet) need to decide how to select
+as these are already assumed to be true. Nonetheless, we *do* currently do fulfill all of them.
-any nested obligations. Nonetheless, we *do* currently do a complete resolution,
+That is because it can sometimes inform the results of type inference.
-and that is because it can sometimes inform the results of type inference.
 That is, we do not have the full substitutions in terms of the type variables
 of the impl available to us, so we must run trait selection to figure
 everything out.
-
-**TODO**: is this still talking about trans?
-
-Here is an example:
-
-```rust,ignore
-trait Foo { ... }
-impl<U, T:Bar<U>> Foo for Vec<T> { ... }
-
-impl Bar<usize> for isize { ... }
-```
-
-After one shallow round of selection for an obligation like `Vec<isize>
-: Foo`, we would know which impl we want, and we would know that
-`T=isize`, but we do not know the type of `U`.  We must select the
-nested obligation `isize : Bar<U>` to find out that `U=usize`.
-
-It would be good to only do *just as much* nested resolution as
-necessary. Currently, though, we just do a full resolution.