diff --git a/src/trait-resolution.md b/src/trait-resolution.md index 5bf8f8716..b9fa81bd6 100644 --- a/src/trait-resolution.md +++ b/src/trait-resolution.md @@ -202,8 +202,8 @@ impl Get for Box { What happens when we invoke `get_it(&Box::new(1_u16))`, for example? In this case, the `Self` type is `Box` – that unifies with both impls, -because the first applies to all types, and the second to all -boxes. In order for this to be unambiguous, the compiler does a *winnowing* +because the first applies to all types `T`, and the second to all +`Box`. In order for this to be unambiguous, the compiler does a *winnowing* pass that considers `where` clauses and attempts to remove candidates. In this case, the first impl only applies if `Box : Copy`, which doesn't hold. After winnowing, @@ -242,7 +242,7 @@ fn foo(x: X) { In the body of `foo`, clearly we can use methods of `A1`, `A2`, or `B` on variable `x`. The line marked `(*)` will incur an obligation `X: A1`, -which the line marked `(#)` will incur an obligation `X: B`. Meanwhile, +while the line marked `(#)` will incur an obligation `X: B`. Meanwhile, the parameter environment will contain two where-clauses: `X : A2` and `X : B`. For each obligation, then, we search this list of where-clauses. The obligation `X: B` trivially matches against the where-clause `X: B`. diff --git a/src/traits-goals-and-clauses.md b/src/traits-goals-and-clauses.md index 0cbdb7077..882f86b8e 100644 --- a/src/traits-goals-and-clauses.md +++ b/src/traits-goals-and-clauses.md @@ -67,7 +67,7 @@ its inputs P0..Pm: Projection = >::AssocItem ``` -Given that, we can define a `DomainGoal` as follows: +Given these, we can define a `DomainGoal` as follows: ```text DomainGoal = Implemented(TraitRef) @@ -78,33 +78,82 @@ DomainGoal = Implemented(TraitRef) | WellFormed(Type) | WellFormed(TraitRef) | WellFormed(Projection = Type) - | Outlives(Type, Region) - | Outlives(Region, Region) + | Outlives(Type: Region) + | Outlives(Region: Region) ``` -- `Implemented(TraitRef)` -- true if the given trait is - implemented for the given input types and lifetimes -- `FromEnv(TraitEnv)` -- true if the given trait is *assumed* to be implemented; - that is, if it can be derived from the in-scope where clauses - - as we'll see in the section on lowering, `FromEnv(X)` implies - `Implemented(X)` but not vice versa. This distinction is crucial - to [implied bounds]. -- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` - is equal to `Type`; see [the section on associated - types](./traits-associated-types.html) - - in general, proving `ProjectionEq(TraitRef::Item = Type)` also - requires proving `Implemented(TraitRef)` -- `Normalize(Projection -> Type)` -- the given associated type `Projection` can - be [normalized][n] to `Type` - - as discussed in [the section on associated - types](./traits-associated-types.html), - `Normalize` implies `ProjectionEq` but not vice versa -- `WellFormed(..)` -- these goals imply that the given item is - *well-formed* - - well-formedness is important to [implied bounds]. +Let's break down each one of these, one-by-one. + +#### Implemented(TraitRef) +e.g. `Implemented(i32: Copy)` + +True if the given trait is implemented for the given input types and lifetimes. + +#### ProjectionEq(Projection = Type) +e.g. `ProjectionEq::Item = u8` + +The given associated type `Projection` is equal to `Type`; this can be proved +with either normalization or using skolemized types. See [the section +on associated types](./traits-associated-types.html). + +#### Normalize(Projection -> Type) +e.g. `ProjectionEq::Item -> u8` + +The given associated type `Projection` can be [normalized][n] to `Type`. + +As discussed in [the section on associated +types](./traits-associated-types.html), `Normalize` implies `ProjectionEq`, +but not vice versa. In general, proving `Normalize(::Item -> U)` +also requires proving `Implemented(T: Trait)`. [n]: ./traits-associated-types.html#normalize +#### FromEnv(TraitRef), FromEnv(Projection = Type) +e.g. `FromEnv(Self: Add)` + +e.g. `FromEnv(::Item<'a> = &'a [u8])` + +True if the inner `TraitRef` or projection equality is *assumed* to be true; +that is, if it can be derived from the in-scope where clauses. + +For example, given the following function: + +```rust +fn loud_clone(stuff: &T) -> T { + println!("cloning!"); + stuff.clone() +} +``` + +Inside the body of our function, we would have `FromEnv(T: Clone)`. In-scope +where clauses nest, so a function body inside an impl body inherits the +impl body's where clauses, too. + +This and the next rule are used to implement [implied bounds]. As we'll see +in the section on lowering, `FromEnv(X)` implies `Implemented(X)`, but not +vice versa. This distinction is crucial to implied bounds. + +#### WellFormed(Item) +These goals imply that the given item is *well-formed*. + +We can talk about different types of items being well-formed: + +**Types**, like `WellFormed(Vec)`, which is true in Rust, or + `WellFormed(Vec)`, which is not (because `str` is not `Sized`.) + +**TraitRefs**, like `WellFormed(Vec: Clone)`. + +**Projections**, like `WellFormed(T: Iterator)`. + +Well-formedness is important to [implied bounds]. In particular, the reason +it is okay to assume `FromEnv(T: Clone)` in the example above is that we +_also_ verify `WellFormed(T: Clone)` for each call site of `loud_clone`. + +#### Outlives(Type: Region), Outlives(Region: Region) +e.g. `Outlives(&'a str: 'b)`, `Outlives('a: 'static)` + +True if the given type or region on the left outlives the right-hand region. + ## Coinductive goals diff --git a/src/traits-lowering-rules.md b/src/traits-lowering-rules.md index 73660c42c..80884cbdd 100644 --- a/src/traits-lowering-rules.md +++ b/src/traits-lowering-rules.md @@ -113,7 +113,7 @@ forall { ``` This clause says that if we are assuming that the trait holds, then we can also -assume that it's where-clauses hold. It's perhaps useful to see an example: +assume that its where-clauses hold. It's perhaps useful to see an example: ```rust,ignore trait Eq: PartialEq { ... }