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
-  are never overlapping impls, where two impls could be used with
-  equal precedence.
+- **Evaluation**: Checks whether obligations holds without constraining
+  any inference variables. Used by selection.
 
 ## 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,68 +122,23 @@ 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
-the `Self` types, but in the future we may also recursively consider some of the
-nested obligations, in the case of an impl.
-
-**TODO**: what does "unifying the `Self` types" mean? The `Self` of the
-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.
+_matching_. For `impl` candidates <!-- date-check: Oct 2022 -->,
+this amounts to unifying the impl header (the `Self` type and the trait arguments)
+while ignoring  nested obligations. If matching succeeds then we add it
+to a set of candidates. There are other rules when assembling candidates for
+built-in traits such as `Copy`, `Sized`, and `CoerceUnsized`.
 
 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
-of candidates by using where clauses and other conditions. 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;
-}
-```
+scope that could possibly apply. Otherwise, we can **winnow** down the set
+of candidates by using where clauses and other conditions. Winnowing uses
+`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. 
 
-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?
+If this reduced set yields a single, unambiguous entry, we're good to go,
+otherwise the result is considered ambiguous.
 
 #### Winnowing: Resolving ambiguities
 
@@ -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
-impl for each method call. In this second selection, we do not consider any
-where-clauses to be in scope 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,
-we only need to do a "shallow" selection for an obligation. That is, we wish to
-identify which impl applies, but we do not (yet) need to decide how to select
-any nested obligations. Nonetheless, we *do* currently do a complete resolution,
-and that is because it can sometimes inform the results of type inference.
+selection. At codegen time, we repeat the trait selection to choose a particular
+impl for each method call. This is done using `fn codegen_select_candidate`. 
+In this second selection, we do not consider any where-clauses to be in scope 
+because we know that each resolution will resolve to a particular impl.
+
+One interesting twist has to do with nested obligations. In general, in codegen,
+we only to figure out which candidate applies, we do not care about nested obligations,
+as these are already assumed to be true. Nonetheless, we *do* currently do fulfill all of them.
+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.