From 479d914ff009a0372427b42f3796f5937297644f Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 27 Feb 2018 05:50:43 -0500 Subject: [PATCH 01/13] work on traits chapters --- src/SUMMARY.md | 13 +- src/trait-resolution.md | 7 +- src/traits-associated-types.md | 143 +++++++++++++++++ src/traits-bibliography.md | 28 ++++ src/traits-canonicalization.md | 93 +++++++++++ src/traits-goals-and-clauses.md | 148 ++++++++++++++++++ src/traits-lowering-rules.md | 267 ++++++++++++++++++++++++++++++++ src/traits-lowering-to-logic.md | 182 ++++++++++++++++++++++ src/traits-regions.md | 3 + src/traits-wf.md | 11 ++ src/traits.md | 18 +++ src/type-inference.md | 2 + 12 files changed, 912 insertions(+), 3 deletions(-) create mode 100644 src/traits-associated-types.md create mode 100644 src/traits-bibliography.md create mode 100644 src/traits-canonicalization.md create mode 100644 src/traits-goals-and-clauses.md create mode 100644 src/traits-lowering-rules.md create mode 100644 src/traits-lowering-to-logic.md create mode 100644 src/traits-regions.md create mode 100644 src/traits-wf.md create mode 100644 src/traits.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index ab9da7295..1c5bc284d 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -17,10 +17,19 @@ - [The HIR (High-level IR)](./hir.md) - [The `ty` module: representing types](./ty.md) - [Type inference](./type-inference.md) -- [Trait resolution](./trait-resolution.md) +- [Trait solving (old-style)](./trait-resolution.md) - [Higher-ranked trait bounds](./trait-hrtb.md) - [Caching subtleties](./trait-caching.md) - - [Speciailization](./trait-specialization.md) + - [Specialization](./trait-specialization.md) +- [Trait solving (new-style)](./traits.md) + - [Canonicalization](./traits-canonicalization.md) + - [Lowering to logic](./traits-lowering-to-logic.md) + - [Goals and clauses](./traits-goals-and-clauses.md) + - [Lowering rules](./traits-lowering-rules.md) + - [Equality and associated types](./traits-associated-types.md) + - [Region constraints](./traits-regions.md) + - [Well-formedness checking](./traits-wf.md) + - [Bibliography](./traits-bibliography.md) - [Type checking](./type-checking.md) - [The MIR (Mid-level IR)](./mir.md) - [MIR construction](./mir-construction.md) diff --git a/src/trait-resolution.md b/src/trait-resolution.md index 28176d740..cccfcd54b 100644 --- a/src/trait-resolution.md +++ b/src/trait-resolution.md @@ -1,8 +1,13 @@ -# Trait resolution +# Trait resolution (old-style) This chapter describes the general process of _trait resolution_ and points out some non-obvious things. +**Note:** This chapter (and its subchapters) describe how the trait +solver **currently** works. However, we are in the process of +designing a new trait solver. If you'd prefer to read about *that*, +see [the traits chapter](./traits.html). + ## Major concepts Trait resolution is the process of pairing up an impl with each diff --git a/src/traits-associated-types.md b/src/traits-associated-types.md new file mode 100644 index 000000000..a640bf032 --- /dev/null +++ b/src/traits-associated-types.md @@ -0,0 +1,143 @@ +# Equality and associated types + +This section covers how the trait system handles equality between +associated types. The full system consists of several moving parts, +which we will introduce one by one: + +- Projection and the `Normalize` predicate +- Skolemization +- The `ProjectionEq` predicate +- Integration with unification + +## Associated type projection and normalization + +When a trait defines an associated type (e.g., +[the `Item` type in the `IntoIterator` trait][intoiter-item]), that +type can be referenced by the user using an **associated type +projection** like ` as IntoIterator>::Item`. (Often, +though, people will use the shorthand syntax `T::Item` -- presently, +that syntax is expanded during +["type collection"](./type-checking.html) into the explicit form, +though that is something we may want to change in the future.) + +In some cases, associated type projections can be **normalized** -- +that is, simplified -- based on the types given in an impl. So, to +continue with our example, the impl of `IntoIterator` for `Option` +declares (among other things) that `Item = T`: + +```rust +impl IntoIterator for Option { + type Item = T; + .. +} +``` + +This means we can normalize the projection ` as +IntoIterator>::Item` to just `u32`. + +In this case, the projection was a "monomorphic" one -- that is, it +did not have any type parameters. Monomorphic projections are special +because they can **always** be fully normalized -- but often we can +normalize other associated type projections as well. For example, +` as IntoIterator>::Item` (where `?T` is an inference +variable) can be normalized to just `?T`. + +In our logic, normalization is defined by a predicate +`Normalize`. The `Normalize` clauses arise only from +impls. For example, the `impl` of `IntoIterator` for `Option` that +we saw above would be lowered to a program clause like so: + + forall { + Normalize( as IntoIterator>::Item -> T) + } + +(An aside: since we do not permit quantification over traits, this is +really more like a family of predicates, one for each associated +type.) + +We could apply that rule to normalize either of the examples that +we've seen so far. + +## Skolemized associated types + +Sometimes however we want to work with associated types that cannot be +normalized. For example, consider this function: + +```rust +fn foo(...) { ... } +``` + +In this context, how would we normalize the type `T::Item`? Without +knowing what `T` is, we can't really do so. To represent this case, we +introduce a type called a **skolemized associated type +projection**. This is written like so `(IntoIterator::Item)`. You +may note that it looks a lot like a regular type (e.g., `Option`), +except that the "name" of the type is `(IntoIterator::Item)`. This is +not an accident: skolemized associated type projections work just like +ordinary types like `Vec` when it comes to unification. That is, +they are only considered equal if (a) they are both references to the +same associated type, like `IntoIterator::Item` and (b) their type +arguments are equal. + +Skolemized associated types are never written directly by the user. +They are used internally by the trait system only, as we will see +shortly. + +## Projection equality + +So far we have seen two ways to answer the question of "When can we +consider an associated type projection equal to another type?": + +- the `Normalize` predicate could be used to transform associated type + projections when we knew which impl was applicable; +- **skolemized** associated types can be used when we don't. + +We now introduce the `ProjectionEq` predicate to bring those two cases +together. The `ProjectionEq` predicate looks like so: + + ProjectionEq(::Item = U) + +and we will see that it can be proven *either* via normalization or +skolemization. As part of lowering an associated type declaration from +some trait, we create two program clauses for `ProjectionEq`: + + forall { + ProjectionEq(::Item = U) :- + Normalize(::Item -> U) + } + + forall { + ProjectionEq(::Item = (IntoIterator::Item)) + } + +These are the only two `ProjectionEq` program clauses we ever make for +any given associated item. + +## Integration with unification + +Now we are ready to discuss how associated type equality integrates +with unification. As described in the +[type inference](./type-inference.html) section, unification is +basically a procedure with a signature like this: + + Unify(A, B) = Result<(Subgoals, RegionConstraints), NoSolution> + +In other words, we try to unify two things A and B. That procedure +might just fail, in which case we get back `Err(NoSolution)`. This +would happen, for example, if we tried to unify `u32` and `i32`. + +The key point is that, on success, unification can also give back to +us a set of subgoals that still remain to be proven (it can also give +back region constraints, but those are not relevant here). + +Whenever unification encounters an (unskolemized!) associated type +projection P being equated with some other type T, it always succeeds, +but it produces a subgoal `ProjectionEq(P = T)` that is propagated +back up. Thus it falls to the ordinary workings of the trait system +to process that constraint. + +(If we unify two projections P1 and P2, then unification produces a +variable X and asks us to prove that `ProjectionEq(P1 = X)` and +`ProjectionEq(P2 = X)`. That used to be needed in an older system to +prevent cycles; I rather doubt it still is. -nmatsakis) + diff --git a/src/traits-bibliography.md b/src/traits-bibliography.md new file mode 100644 index 000000000..d9ff912c7 --- /dev/null +++ b/src/traits-bibliography.md @@ -0,0 +1,28 @@ +# Bibliography + +If you'd like to read more background material, here are some +recommended texts and papers: + +[Programming with Higher-order Logic][phl], by Dale Miller and Gopalan +Nadathur, covers the key concepts of Lambda prolog. Although it's a +slim little volume, it's the kind of book where you learn something +new every time you open it. + +[phl]: https://www.amazon.com/Programming-Higher-Order-Logic-Dale-Miller/dp/052187940X + + + +["A proof procedure for the logic of Hereditary Harrop formulas"][pphhf], +by Gopalan Nadathur. This paper covers the basics of universes, +environments, and Lambda Prolog-style proof search. Quite readable. + +[pphhf]: https://dl.acm.org/citation.cfm?id=868380 + + + +["A new formulation of tabled resolution with delay"][nftrd], by +[Theresa Swift]. This paper gives a kind of abstract treatment of the +SLG formulation that is the basis for our on-demand solver. + +[nftrd]: https://dl.acm.org/citation.cfm?id=651202 +[ts]: http://www3.cs.stonybrook.edu/~tswift/ diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md new file mode 100644 index 000000000..35352d605 --- /dev/null +++ b/src/traits-canonicalization.md @@ -0,0 +1,93 @@ +# Canonicalization + +Canonicalization is the process of **isolating** an inference value +from its context. It is really based on a very simple concept: every +[inference variable](./type-inference.html#vars) is always in one of two +states: either it is **unbound**, in which case we don't know yet what +type it is, or it is **bound**, in which case we do. So to isolate +some thing T from its environment, we just walk down and find the +unbound variables that appear in T; those variables get renumbered in +a canonical order (left to right, for the most part, but really it +doesn't matter as long as it is consistent). + +So, for example, if we have the type `X = (?T, ?U)`, where `?T` and +`?U` are distinct, unbound inference variables, then the canonical +form of `X` would be `(?0, ?1)`, where `?0` and `?1` represent these +**canonical placeholders**. Note that the type `Y = (?U, ?T)` also +canonicalizes to `(?0, ?1)`. But the type `Z = (?T, ?T)` would +canonicalize to `(?0, ?0)` (as would `(?U, ?U)`). In other words, the +exact identity of the inference variables is not important -- unless +they are repeated. + +We use this to improve caching as well as to detect cycles and other +things during trait resolution. Roughly speaking, the idea is that if +two trait queries have the same canonicalize form, then they will get +the same answer -- modulo the precise identities of the variables +involved. + +To see how it works, imagine that we are asking to solve the following +trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound. +This query contains two unbound variables, but it also contains the +lifetime `'static`. The trait system generally ignores all lifetimes +and treats them equally, so when canonicalizing, we will *also* +replace any [free lifetime](./background.html#free-vs-bound) with a +canonical variable. Therefore, we get the following result: + + ?0: Foo<'?1, ?2> + +Sometimes we write this differently, like so: + + for { ?0: Foo<'?1, ?2> } + +This `for<>` gives some information about each of the canonical +variables within. In this case, I am saying that `?0` is a type +(`T`), `?1` is a lifetime (`L`), and `?2` is also a type (`T`). The +`canonicalize` method *also* gives back a `CanonicalVarValues` array +with the "original values" for each canonicalized variable: + + [?A, 'static, ?B] + +Now we do the query and get back some result R. As part of that +result, we'll have an array of values for the canonical inputs. For +example, the canonical result might be: + +``` +for<2> { + values = [ Vec, '1, ?0 ] + ^^ ^^ ^^ these are variables in the result! + ... +} +``` + +Note that this result is itself canonical and may include some +variables (in this case, `?0`). + +What we want to do conceptually is to (a) instantiate each of the +canonical variables in the result with a fresh inference variable +and then (b) unify the values in the result with the original values. +Doing step (a) would yield a result of + +``` +{ + values = [ Vec, '?X, ?C ] + ^^ ^^^ fresh inference variables in `self` + .. +} +``` + +Step (b) would then unify: + +``` +?A with Vec +'static with '?X +?B with ?C +``` + +(What we actually do is a mildly optimized variant of that: Rather +than eagerly instantiating all of the canonical values in the result +with variables, we instead walk the vector of values, looking for +cases where the value is just a canonical variable. In our example, +`values[2]` is `?C`, so that we means we can deduce that `?C := ?B and +`'?X := 'static`. This gives us a partial set of values. Anything for +which we do not find a value, we create an inference variable.) + diff --git a/src/traits-goals-and-clauses.md b/src/traits-goals-and-clauses.md new file mode 100644 index 000000000..ad1655726 --- /dev/null +++ b/src/traits-goals-and-clauses.md @@ -0,0 +1,148 @@ +# Goals and clauses + +In logic programming terms, a **goal** is something that you must +prove and a **clause** is something that you know is true. As +described in the [lowering to logic](./traits-lowering-to-logic.html) +chapter, Rust's trait solver is based on an extension of hereditary +harrop (HH) clauses, which extend traditional Prolog Horn clauses with +a few new superpowers. + +## Goals and clauses meta structure + +In Rust's solver, **goals** and **clauses** have the following forms +(note that the two definitions reference one another): + + Goal = DomainGoal + | Goal && Goal + | Goal || Goal + | exists { Goal } // existential quantification + | forall { Goal } // universal quantification + | if (Clause) { Goal } // implication + + Clause = DomainGoal + | Clause :- Goal // if can prove Goal, then Clause is true + | Clause && Clause + | forall { Clause } + + K = // a "kind" + | + +The proof procedure for these sorts of goals is actually quite +straightforward. Essentially, it's a form of depth-first search. The +paper +["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf] +gives the details. + +[pphhf]: ./traits-bibliography.html#pphhf + + + +## Domain goals + +To define the set of *domain goals* in our system, we need to first +introduce a few simple formulations. A **trait reference** consists of +the name of a trait allow with a suitable set of inputs P0..Pn: + + TraitRef = P0: TraitName + +So, for example, `u32: Display` is a trait reference, as is `Vec: +IntoIterator`. Note that Rust surface syntax also permits some extra +things, like associated type bindings (`Vec: IntoIterator`), that are not part of a trait reference. + +A **projection** consists of a an associated item reference along with +its inputs P0..Pm: + + Projection = >::AssocItem + +Given that, we can define a `DomainGoal` as follows: + + DomainGoal = Implemented(TraitRef) + | ProjectionEq(Projection = Type) + | Normalize(Projection -> Type) + | FromEnv(TraitRef) + | FromEnv(Projection = Type) + | WellFormed(Type) + | WellFormed(TraitRef) + | WellFormed(Projection = Type) + | 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) +- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be normalized + 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]. + + + +## Coinductive goals + +Most goals in our system are "inductive". In an inductive goal, +circular reasoning is disallowed. Consider this example clause: + + Implemented(Foo: Bar) :- + Implemented(Foo: Bar). + +Considered inductively, this clause is useless: if we are trying to +prove `Implemented(Foo: Bar)`, we would then recursively have to prove +`Implemented(Foo: Bar)`, and that cycle would continue ad infinitum +(the trait solver will terminate here, it would just consider that +`Implemented(Foo: Bar)` is not known to be true). + +However, some goals are *co-inductive*. Simply put, this means that +cycles are OK. So, if `Bar` were a co-inductive trait, then the rule +above would be perfectly valid, and it would indicate that +`Implemented(Foo: Bar)` is true. + +*Auto traits* are one example in Rust where co-inductive goals are used. +Consider the `Send` trait, and imagine that we have this struct: + +```rust +struct Foo { + next: Option> +} +``` + +The default rules for auto traits say that `Foo` is `Send` if the +types of its fields are `Send`. Therefore, we would have a rule like + + Implemented(Foo: Send) :- + Implemented(Option>: Send). + +As you can probably imagine, proving that `Option>: Send` is +going to wind up circularly requiring us to prove that `Foo: Send` +again. So this would be an example where we wind up in a cycle -- but +that's ok, we *do* consider `Foo: Send` to hold, even though it +references itself. + +In general, co-inductive traits are used in Rust trait solving when we +want to enumerate a fixed set of possibilities. In the case of auto +traits, we are enumerating the set of reachable types from a given +starting point (i.e., `Foo` can reach values of type +`Option>`, which implies it can reach values of type +`Box`, and then of type `Foo`, and then the cycle is complete). + +In addition to auto traits, `WellFormed` predicates are co-inductive. +These are used to achieve a similar "enumerate all the cases" pattern, +as described in the section on [implied bounds]. + +[implied bounds]: ./traits-lowering-rules.html#implied-bounds + +## Incomplete chapter + +Some topics yet to be written: + +- Elaborate on the proof procedure +- SLG solving -- introduce negative reasoning diff --git a/src/traits-lowering-rules.md b/src/traits-lowering-rules.md new file mode 100644 index 000000000..d096b4364 --- /dev/null +++ b/src/traits-lowering-rules.md @@ -0,0 +1,267 @@ +# Lowering rules + +This section gives the complete lowering rules for Rust traits into +[program clauses][pc]. These rules reference the [domain goals][dg] defined in +an earlier section. + +[pc]: ./traits-goals-and-clauses.html +[dg]: ./traits-goals-and-clauses.html#domain-goals + +## Notation + +The nonterminal `Pi` is used to mean some generic *parameter*, either a +named lifetime like `'a` or a type paramter like `A`. + +The nonterminal `Ai` is used to mean some generic *argument*, which +might be a lifetime like `'a` or a type like `Vec`. + +When defining the lowering rules, we will give goals and clauses in +the [notation given in this section](./traits-goals-and-clauses.html). +We sometimes insert "macros" like `LowerWhereClause!` into these +definitions; these macros reference other sections within this chapter. + +## Lowering where clauses + +When used in a goal position, where clauses can be mapped directly +[domain goals][dg], as follows: + +- `A0: Foo` maps to `Implemented(A0: Foo)`. +- `A0: Foo` maps to `ProjectionEq(>::Item = T)` +- `T: 'r` maps to `Outlives(T, 'r)` +- `'a: 'b` maps to `Outlives('a, 'b)` + +In the rules below, we will use `WC` to indicate where clauses that +appear in Rust syntax; we will then use the same `WC` to indicate +where those where clauses appear as goals in the program clauses that +we are producing. In that case, the mapping above is used to convert +from the Rust syntax into goals. + +### Transforming the lowered where clauses + +In addition, in the rules below, we sometimes do some transformations +on the lowered where clauses, as defined here: + +- `FromEnv(WC)` -- this indicates that: + - `Implemented(TraitRef)` becomes `FromEnv(TraitRef)` + - `ProjectionEq(Projection = Ty)` becomes `FromEnv(Projection = Ty)` + - other where-clauses are left intact +- `WellFormed(WC)` -- this indicates that: + - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)` + - `ProjectionEq(Projection = Ty)` becomes `WellFormed(Projection = Ty)` + +*TODO*: I suspect that we want to alter the outlives relations too, +but Chalk isn't modeling those right now. + +## Lowering traits + +Given a trait definition + +```rust +trait Trait // P0 == Self +where WC +{ + // trait items +} +``` + +we will produce a number of declarations. This section is focused on +the program clauses for the trait header (i.e., the stuff outside the +`{}`); the [section on trait items](#trait-items) covers the stuff +inside the `{}`. + +### Trait header + +From the trait itself we mostly make "meta" rules that setup the +relationships between different kinds of domain goals. The first dush +rule from the trait header creates the mapping between the `FromEnv` +and `Implemented` predicates: + + forall { + Implemented(Self: Trait) :- FromEnv(Self: Trait + +#### Implied bounds + +The next few clauses have to do with implied bounds (see also +[RFC 2089]). For each trait, we produce two clauses: + +[RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html + + // For each where clause WC: + forall { + FromEnv(WC) :- FromEnv(Self: Trait { + WellFormed(Self: Trait) :- Implemented(Self: Trait), WellFormed(WC) + } + +This `WellFormed` rule states that `T: Trait` is well-formed if (a) +`T: Trait` is implemented and (b) all the where-clauses declared on +`Trait` are well-formed (and hence they are implemented). Remember +that the `WellFormed` predicate is +[coinductive](./traits-goals-and-clauses.html#coinductive); in this +case, it is serving as a kind of "carrier" that allows us to enumerate +all the where clauses that are transitively implied by `T: Trait`. + +An example: + +```rust +trait Foo: A + Bar { } +trait Bar: B + Foo { } +trait A { } +trait B { } +``` + +Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and `T: B`. +And indeed if we were to try to prove `WellFormed(T: Foo)`, we would have to prove each +one of those: + +- `WellFormed(T: Foo)` + - `Implemented(T: Foo)` + - `WellFormed(T: A)` + - `Implemented(T: A)` + - `WellFormed(T: Bar)` + - `Implemented(T: Bar)` + - `WellFormed(T: B)` + - `Implemented(T: Bar)` + - `WellFormed(T: Foo)` -- cycle, true coinductively + +This `WellFormed` predicate is only used when proving that impls are +well-formed -- basically, for each impl of some trait ref `TraitRef`, +we must that `WellFormed(TraitRef)`. This in turn justifies the +implied bounds rules that allow us to extend the set of `FromEnv` +items. + + + +## Lowering trait items + +### Associated type declarations + +Given a trait that declares a (possibly generic) associated type: + +```rust +trait Trait // P0 == Self +where WC +{ + type AssocType: Bounds where WC1; +} +``` + +We will produce a number of program clases. The first two define +the rules by which `ProjectionEq` can succeed; these two clauses are discussed +in detail in the [section on associated types](./traits-associated-types.html). + + // ProjectionEq can succeed by normalizing: + forall { + ProjectionEq(>::AssocType = U) :- + Normalize(>::AssocType -> U) + } + + // ProjectionEq can succeed by skolemizing: + forall { + ProjectionEq( + >::AssocType = + (Trait::AssocType) + ) :- + // But only if the trait is implemented, and the conditions from + // the associated type are met as well: + Implemented(Self: Trait), + WC1 + } + +The next rule covers implied bounds for the projection. In particular, +the `Bounds` declared on the associated type must be proven to hold to +show that the impl is well-formed, and hence we can rely on them from +elsewhere. + + // XXX how exactly should we set this up? Have to be careful; + // presumably this has to be a kind of `FromEnv` setup. + +### Lowering function and constant declarations + +Chalk didn't model functions and constants, but I would eventually +like to treat them exactly like normalization. See [the section on function/constant +values below](#constant-vals) for more details. + +## Lowering impls + +Given an impl of a trait: + +```rust +impl Trait for A0 +where WC +{ + // zero or more impl items +} +``` + +Let `TraitRef` be the trait reference `A0: Trait`. Then we +will create the following rules: + + forall { + Implemented(TraitRef) :- WC + } + +In addition, we will lower all of the *impl items*. + +## Lowering impl items + +### Associated type values + +Given an impl that contains: + +```rust +impl Trait for A0 +where WC +{ + type AssocType: Bounds where WC1 = T; +} +``` + +We produce the following rule: + + forall { + forall { + Normalize(>::AssocType -> T) :- + WC, WC1 + } + } + +Note that `WC` and `WC1` both encode where-clauses that the impl can +rely on, whereas the bounds `Bounds` on the associated type are things +that the impl must prove (see the well-formedness checking). + + + +### Function and constant values + +Chalk didn't model functions and constants, but I would eventually +like to treat them exactly like normalization. This presumably +involves adding a new kind of parameter (constant), and then having a +`NormalizeValue` domain goal. This is *to be written* because the +details are a bit up in the air. + + diff --git a/src/traits-lowering-to-logic.md b/src/traits-lowering-to-logic.md new file mode 100644 index 000000000..7b1c2ed6b --- /dev/null +++ b/src/traits-lowering-to-logic.md @@ -0,0 +1,182 @@ +# Lowering to logic + +The key observation here is that the Rust trait system is basically a +kind of logic, and it can be mapped onto standard logical inference +rules. We can then look for solutions to those inference rules in a +very similar fashion to how e.g. a [Prolog] solver works. It turns out +that we can't *quite* use Prolog rules (also called Horn clauses) but +rather need a somewhat more expressive variant. + +[Prolog]: https://en.wikipedia.org/wiki/Prolog + +## Rust traits and logic + +One of the first observations is that the Rust trait system is +basically a kind of logic. As such, we can map our struct, trait, and +impl declarations into logical inference rules. For the most part, +these are basically Horn clauses, though we'll see that to capture the +full richness of Rust -- and in particular to support generic +programming -- we have to go a bit further than standard Horn clauses. + +To see how this mapping works, let's start with an example. Imagine +we declare a trait and a few impls, like so: + +```rust +trait Clone { } +impl Clone for usize { } +impl Clone for Vec where T: Clone { } +``` + +We could map these declarations to some Horn clauses, written in a +Prolog-like notation, as follows: + +``` +Clone(usize). +Clone(Vec) :- Clone(?T). +``` + +In Prolog terms, we might say that `Clone(Foo)` -- where `Foo` is some +Rust type -- is a *predicate* that represents the idea that the type +`Foo` implements `Clone`. These rules are **program clauses**; they +state the conditions under which that predicate can be proven (i.e., +considered true). So the first rule just says "Clone is implemented +for `usize`". The next rule says "for any type `?T`, Clone is +implemented for `Vec` if clone is implemented for `?T`". So +e.g. if we wanted to prove that `Clone(Vec>)`, we would do +so by applying the rules recursively: + +- `Clone(Vec>)` is provable if: + - `Clone(Vec)` is provable if: + - `Clone(usize)` is provable. (Which is is, so we're all good.) + +But now suppose we tried to prove that `Clone(Vec)`. This would +fail (after all, I didn't give an impl of `Clone` for `Bar`): + +- `Clone(Vec)` is provable if: + - `Clone(Bar)` is provable. (But it is not, as there are no applicable rules.) + +We can easily extend the example above to cover generic traits with +more than one input type. So imagine the `Eq` trait, which declares +that `Self` is equatable with a value of type `T`: + +```rust +trait Eq { ... } +impl Eq for usize { } +impl> Eq> for Vec { } +``` + +That could be mapped as follows: + +``` +Eq(usize, usize). +Eq(Vec, Vec) :- Eq(?T, ?U). +``` + +So far so good. + +## Type-checking normal functions + +OK, now that we have defined some logical rules that are able to +express when traits are implemented and to handle associated types, +let's turn our focus a bit towards **type-checking**. Type-checking is +interesting because it is what gives us the goals that we need to +prove. That is, everything we've seen so far has been about how we +derive the rules by which we can prove goals from the traits and impls +in the program; but we are also interesting in how derive the goals +that we need to prove, and those come from type-checking. + +Consider type-checking the function `foo()` here: + +```rust +fn foo() { bar::() } +fn bar() { } +``` + +This function is very simple, of course: all it does is to call +`bar::()`. Now, looking at the definition of `bar()`, we can see +that it has one where-clause `U: Eq`. So, that means that `foo()` will +have to prove that `usize: Eq` in order to show that it can call `bar()` +with `usize` as the type argument. + +If we wanted, we could write a Prolog predicate that defines the +conditions under which `bar()` can be called. We'll say that those +conditions are called being "well-formed": + +``` +barWellFormed(?U) :- Eq(?U). +``` + +Then we can say that `foo()` type-checks if the reference to +`bar::` (that is, `bar()` applied to the type `usize`) is +well-formed: + +``` +fooTypeChecks :- barWellFormed(usize). +``` + +If we try to prove the goal `fooTypeChecks`, it will succeed: + +- `fooTypeChecks` is provable if: + - `barWellFormed(usize)`, which is provable if: + - `Eq(usize)`, which is provable because of an impl. + +Ok, so far so good. Let's move on to type-checking a more complex function. + +## Type-checking generic functions: beyond Horn clauses + +In the last section, we used standard Prolog horn-clauses (augmented with Rust's +notion of type equality) to type-check some simple Rust functions. But that only +works when we are type-checking non-generic functions. If we want to type-check +a generic function, it turns out we need a stronger notion of goal than Prolog +can be provide. To see what I'm talking about, let's revamp our previous +example to make `foo` generic: + +```rust +fn foo() { bar::() } +fn bar() { } +``` + +To type-check the body of `foo`, we need to be able to hold the type +`T` "abstract". That is, we need to check that the body of `foo` is +type-safe *for all types `T`*, not just for some specific type. We might express +this like so: + +``` +fooTypeChecks :- + // for all types T... + forall { + // ...if we assume that Eq(T) is provable... + if (Eq(T)) { + // ...then we can prove that `barWellFormed(T)` holds. + barWellFormed(T) + } + }. +``` + +This notation I'm using here is the notation I've been using in my +prototype implementation; it's similar to standard mathematical +notation but a bit Rustified. Anyway, the problem is that standard +Horn clauses don't allow universal quantification (`forall`) or +implication (`if`) in goals (though many Prolog engines do support +them, as an extension). For this reason, we need to accept something +called "first-order hereditary harrop" (FOHH) clauses -- this long +name basically means "standard Horn clauses with `forall` and `if` in +the body". But it's nice to know the proper name, because there is a +lot of work describing how to efficiently handle FOHH clauses; see for +example Gopalan Nadathur's excellent +["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf] +in [the bibliography]. + +[the bibliography]: ./traits-bibliography.html +[pphhf]: ./traits-bibliography.html#pphhf + +It turns out that supporting FOHH is not really all that hard. And +once we are able to do that, we can easily describe the type-checking +rule for generic functions like `foo` in our logic. + +## Source + +This page is a lightly adapted version of a +[blog post by Nicholas Matsakis][lrtl]. + +[lrtl]: http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/ diff --git a/src/traits-regions.md b/src/traits-regions.md new file mode 100644 index 000000000..baa3582b6 --- /dev/null +++ b/src/traits-regions.md @@ -0,0 +1,3 @@ +# Region constraints + +*to be written* diff --git a/src/traits-wf.md b/src/traits-wf.md new file mode 100644 index 000000000..c002b8cc1 --- /dev/null +++ b/src/traits-wf.md @@ -0,0 +1,11 @@ +# Well-formedness checking + +This chapter is mostly *to be written*. WF checking, in short, has the +job of checking that the various declarations in a Rust program are +well-formed. This is the basis for implied bounds, and partly for that +reason, this checking can be surprisingly subtle! (For example, we +have to be sure that each impl proves the WF conditions declared on +the trait.) + + + diff --git a/src/traits.md b/src/traits.md new file mode 100644 index 000000000..28e27e82e --- /dev/null +++ b/src/traits.md @@ -0,0 +1,18 @@ +# Trait solving (new-style) + +🚧 This chapter describes "new-style" trait solving. This is still in +the process of being implemented; this chapter serves as a kind of +in-progress design document. If you would prefer to read about how the +current trait solver works, check out +[this chapter](./trait-resolution.html).🚧 + +Trait solving is based around a few key ideas: + +- [Canonicalization](./traits-canonicalization.html), which allows us to + extract types that contain inference variables in them from their + inference context, work with them, and then bring the results back + into the original context. +- [Lowering to logic](./traits-lowering-to-logic.html), which expresses + Rust traits in terms of standard logical terms. + +*more to come* diff --git a/src/type-inference.md b/src/type-inference.md index 8812d34d7..3795ea70e 100644 --- a/src/type-inference.md +++ b/src/type-inference.md @@ -43,6 +43,8 @@ The `tcx.infer_ctxt` method actually returns a builder, which means there are some kinds of configuration you can do before the `infcx` is created. See `InferCtxtBuilder` for more information. + + ## Inference variables The main purpose of the inference context is to house a bunch of From e4aaa9c7f9e23d24e8f5d566143c232631970014 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 9 Mar 2018 04:14:18 -0500 Subject: [PATCH 02/13] clarify how there are two traits chapters --- src/trait-resolution.md | 2 +- src/traits.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/trait-resolution.md b/src/trait-resolution.md index cccfcd54b..d6edcf68a 100644 --- a/src/trait-resolution.md +++ b/src/trait-resolution.md @@ -6,7 +6,7 @@ some non-obvious things. **Note:** This chapter (and its subchapters) describe how the trait solver **currently** works. However, we are in the process of designing a new trait solver. If you'd prefer to read about *that*, -see [the traits chapter](./traits.html). +see [*this* traits chapter](./traits.html). ## Major concepts diff --git a/src/traits.md b/src/traits.md index 28e27e82e..0098704d8 100644 --- a/src/traits.md +++ b/src/traits.md @@ -4,7 +4,7 @@ the process of being implemented; this chapter serves as a kind of in-progress design document. If you would prefer to read about how the current trait solver works, check out -[this chapter](./trait-resolution.html).🚧 +[this other chapter](./trait-resolution.html).🚧 Trait solving is based around a few key ideas: From 6f99f12c2acbceae307c43e53a05071aa434380b Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 9 Mar 2018 04:16:34 -0500 Subject: [PATCH 03/13] link to traits working group tracking issue --- src/traits.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/traits.md b/src/traits.md index 0098704d8..f0e67ffd4 100644 --- a/src/traits.md +++ b/src/traits.md @@ -1,10 +1,15 @@ # Trait solving (new-style) -🚧 This chapter describes "new-style" trait solving. This is still in -the process of being implemented; this chapter serves as a kind of +🚧 This chapter describes "new-style" trait solving. This is still in the +[process of being implemented][wg]; this chapter serves as a kind of in-progress design document. If you would prefer to read about how the current trait solver works, check out -[this other chapter](./trait-resolution.html).🚧 +[this other chapter](./trait-resolution.html). (By the way, if you +would like to help in hacking on the new solver, you will find +instructions for getting involved in the +[Traits Working Group tracking issue][wg].) 🚧 + +[wg]: https://github.com/rust-lang/rust/issues/48416 Trait solving is based around a few key ideas: From fd92491375f30b89050ebe51130112d1cee8896e Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 9 Mar 2018 04:19:36 -0500 Subject: [PATCH 04/13] don't say 'thing' --- src/traits-canonicalization.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md index 35352d605..8ab73a7ff 100644 --- a/src/traits-canonicalization.md +++ b/src/traits-canonicalization.md @@ -2,13 +2,15 @@ Canonicalization is the process of **isolating** an inference value from its context. It is really based on a very simple concept: every -[inference variable](./type-inference.html#vars) is always in one of two -states: either it is **unbound**, in which case we don't know yet what -type it is, or it is **bound**, in which case we do. So to isolate -some thing T from its environment, we just walk down and find the -unbound variables that appear in T; those variables get renumbered in -a canonical order (left to right, for the most part, but really it -doesn't matter as long as it is consistent). +[inference variable](./type-inference.html#vars) is always in one of +two states: either it is **unbound**, in which case we don't know yet +what type it is, or it is **bound**, in which case we do. So to +isolate some data-structure T that contains types/regions from its +environment, we just walk down and find the unbound variables that +appear in T; those variables get replaced with "canonical variables", +starting from zero and numbered in a fixed order (left to right, for +the most part, but really it doesn't matter as long as it is +consistent). So, for example, if we have the type `X = (?T, ?U)`, where `?T` and `?U` are distinct, unbound inference variables, then the canonical From 3c8a827a37a5c48661fdaf4e5b34806f528bffd9 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 9 Mar 2018 04:30:48 -0500 Subject: [PATCH 05/13] expand reorder topic list slightly --- src/SUMMARY.md | 2 +- src/traits-canonicalization.md | 5 +++-- src/traits.md | 22 ++++++++++++++++------ 3 files changed, 20 insertions(+), 9 deletions(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 1c5bc284d..9c1920d32 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -22,8 +22,8 @@ - [Caching subtleties](./trait-caching.md) - [Specialization](./trait-specialization.md) - [Trait solving (new-style)](./traits.md) - - [Canonicalization](./traits-canonicalization.md) - [Lowering to logic](./traits-lowering-to-logic.md) + - [Canonical queries](./traits-canonicalization.md) - [Goals and clauses](./traits-goals-and-clauses.md) - [Lowering rules](./traits-lowering-rules.md) - [Equality and associated types](./traits-associated-types.md) diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md index 8ab73a7ff..9b71c8470 100644 --- a/src/traits-canonicalization.md +++ b/src/traits-canonicalization.md @@ -24,8 +24,9 @@ they are repeated. We use this to improve caching as well as to detect cycles and other things during trait resolution. Roughly speaking, the idea is that if two trait queries have the same canonicalize form, then they will get -the same answer -- modulo the precise identities of the variables -involved. +the same answer. That answer will be expressed in terms of the +canonical variables (`?0`, `?1`), which we can then map back to the +original variables (`?T`, `?U`). To see how it works, imagine that we are asking to solve the following trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound. diff --git a/src/traits.md b/src/traits.md index f0e67ffd4..18cb0c649 100644 --- a/src/traits.md +++ b/src/traits.md @@ -13,11 +13,21 @@ instructions for getting involved in the Trait solving is based around a few key ideas: -- [Canonicalization](./traits-canonicalization.html), which allows us to - extract types that contain inference variables in them from their - inference context, work with them, and then bring the results back - into the original context. - [Lowering to logic](./traits-lowering-to-logic.html), which expresses Rust traits in terms of standard logical terms. - -*more to come* + - The [goals and clauses](./traits-goals-and-clauses.html) chapter + describes the precise lowering rules we use. +- [Canonical queries](./traits-canonicalization.html), which allow us + to solve trait problems (like "is `Foo` implemented for the type + `Bar`?") once, and then apply that same result independently in many + different inference contexts. +- [Lazy normalization](./traits-associated-types.html), which is the + technique we use to accommodate associated types when figuring out + whether types are equal. +- [Region constraints](./traits-regions.md), which are accumulated + during trait solving but mostly ignored. This means that trait + solving effectively ignores the precise regions involved, always -- + but we still remember the constraints on them so that those + constraints can be checked by thet type checker. + +Note: this is not a complete list of topics. See the sidebar for more. From c3a35021d6e607ecc7b05573875b49d476ded8f6 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 05:32:47 -0500 Subject: [PATCH 06/13] add background material on trait queries --- src/SUMMARY.md | 8 +- src/traits-canonical-queries.md | 228 ++++++++++++++++++++++++++++++++ src/traits-canonicalization.md | 7 +- src/traits-slg.md | 1 + src/traits.md | 2 +- 5 files changed, 241 insertions(+), 5 deletions(-) create mode 100644 src/traits-canonical-queries.md create mode 100644 src/traits-slg.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 9c1920d32..95a5ee577 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -23,12 +23,14 @@ - [Specialization](./trait-specialization.md) - [Trait solving (new-style)](./traits.md) - [Lowering to logic](./traits-lowering-to-logic.md) - - [Canonical queries](./traits-canonicalization.md) - - [Goals and clauses](./traits-goals-and-clauses.md) - - [Lowering rules](./traits-lowering-rules.md) + - [Goals and clauses](./traits-goals-and-clauses.md) + - [Lowering rules](./traits-lowering-rules.md) + - [Canonical queries](./traits-canonical-queries.md) + - [Canonicalization](./traits-canonicalization.md) - [Equality and associated types](./traits-associated-types.md) - [Region constraints](./traits-regions.md) - [Well-formedness checking](./traits-wf.md) + - [The SLG solver](./traits-slg.md) - [Bibliography](./traits-bibliography.md) - [Type checking](./type-checking.md) - [The MIR (Mid-level IR)](./mir.md) diff --git a/src/traits-canonical-queries.md b/src/traits-canonical-queries.md new file mode 100644 index 000000000..ec861eb47 --- /dev/null +++ b/src/traits-canonical-queries.md @@ -0,0 +1,228 @@ +# Canonical queries + +The "start" of the trait system is the **canonical query** (these are +both queries in the more general sense of the word -- something you +would like to know the answer to -- and in the +[rustc-specific sense](./query.html)). The idea is that the type +checker or other parts of the system, may in the course of doing their +thing want to know whether some trait is implemented for some type +(e.g., is `u32: Debug` true?). Or they may want to +[normalize some associated type](./traits-associated-types.html). + +This section covers queries at a fairly high level of abstraction. The +subsections look a bit more closely at how these ideas are implemented +in rustc. + +## The traditional, interactive Prolog query + +In a traditional Prolog system, when you start a query, the solver +will run off and start supplying you with every possible answer it can +find. So given something like this: + + ?- Vec: AsRef + +The solver might answer: + + Vec: AsRef<[i32]> + continue? (y/n) + +This `continue` bit is interesting. The idea in Prolog is that the +solver is finding **all possible** instantiations of your query that +are true. In this case, if we instantiate `?U = [i32]`, then the query +is true (note that a traditional Prolog interface does not, directly, +tell us a value for `?U`, but we can infer one by unifying the +response with our original query -- Rust's solver gives back a +substitution instead). If we were to hit `y`, the solver might then +give us another possible answer: + + Vec: AsRef> + continue? (y/n) + +This answer derives from the fact that there is a reflexive impl +(`impl AsRef for T`) for `AsRef`. If were to hit `y` again, +then we might get back a negative response: + + no + +Naturally, in some cases, there may be no possible answers, and hence +the solver will just give me back `no` right away: + + ?- Box: Copy + no + +In some cases, there might be an infinite number of responses. So for +example if I gave this query, and I kept hitting `y`, then the solver +would never stop giving me back answers: + + ?- Vec: Clone + Vec: Clone + continue? (y/n) + Vec>: Clone + continue? (y/n) + Vec>>: Clone + continue? (y/n) + Vec>>>: Clone + continue? (y/n) + +As you can imagine, the solver will gleefully keep adding another +layer of `Box` until we ask it to stop, or it runs out of memory. + +Another interesting thing is that queries might still have variables +in them. For example: + + ?- Rc: Clone + +might produce the answer: + + Rc: Clone + continue? (y/n) + +After all, `Rc` is true **no matter what type `?T` is**. + +## A trait query in rustc + +The trait queries in rustc work somewhat differently. Instead of +trying to enumerate **all possible** answers for you, they are looking +for an **unambiguous** answer. In particular, when they tells you the +value for a type variable, that means that this is the **only possible +instantiation** that you could use, given the current set of impls and +where-clauses, that would be provable. (Internally within the solver, +though, they can potentially enumerate all possible answers. See +[the description of the SLG solver](./traits-slg.html) for details.) + +The response to a trait query in rustc is typically a +`Result, NoSolution>` (where the `T` will vary a bit +depending on the query itself). The `Err(NoSolution)` case indicates +that the query was false and had no answers (e.g., `Box: Copy`). +Otherwise, the `QueryResult` gives back information about the possible answer(s) +we did find. It consists of four parts: + +- **Certainty:** tells you how sure we are of this answer. It can have two values: + - `Proven` means that the result is known to be true. + - This might be the result for trying to prove `Vec: Clone`, + say, or `Rc: Clone`. + - `Ambiguous` means that there were things we could not yet prove to + be either true *or* false, typically because more type information + was needed. (We'll see an example shortly.) + - This might be the result for trying to prove `Vec: Clone`. +- **Var values:** Values for each of the unbound inference variables + (like `?T`) that appeared in your original query. (Remember that in Prolog, + we had to infer these.) + - As we'll see in the example below, we can get back var values even + for `Ambiguous` cases. +- **Region constraints:** these are relations that must hold between + the lifetimes that you supplied as inputs. We'll ignore these here, + but see the + [section on handling regions in traits](./traits-regions.html) for + more details. +- **Value:** The query result also comes with a value of type `T`. For + some specialized queries -- like normalizing associated types -- + this is used to carry back an extra result, but it's often just + `()`. + +### Examples + +Let's work through an example query to see what all the parts mean. +Consider [the `Borrow` trait][borrow]. This trait has a number of +impls; among them, there are these two (for clarify, I've written the +`Sized` bounds explicitly): + +[borrow]: https://doc.rust-lang.org/std/borrow/trait.Borrow.html + +```rust +impl Borrow for T where T: ?Sized +impl Borrow<[T]> for Vec where T: Sized +``` + +**Example 1.** Imagine we are type-checking this (rather artificial) +bit of code: + +```rust +fn foo(a: A, vec_b: Option) where A: Borrow { } + +fn main() { + let mut t: Vec<_> = vec![]; // Type: Vec + let mut u: Option<_> = None; // Type: Option + foo(t, u); // Example 1: requires `Vec: Borrow` + ... +} +``` + +As the comments indicate, we first create two variables `t` and `u`; +`t` is an empty vector and `u` is a `None` option. Both of these +variables have unbound inference variables in their type: `?T` +represents the elements in the vector `t` and `?U` represents the +value stored in the option `u`. Next, we invoke `foo`; comparing the +signature of `foo` to its arguments, we wind up with `A = Vec` and +`B = ?U`.Therefore, the where clause on `foo` requires that `Vec: +Borrow`. This is thus our first example trait query. + +There are many possible solutions to the query `Vec: Borrow`; +for example: + +- `?U = Vec`, +- `?U = [?T]`, +- `?T = u32, ?U = [u32]` +- and so forth. + +Therefore, the result we get back would be as follows (I'm going to +ignore region constraints and the "value"): + +- Certainty: `Ambiguous` -- we're not sure yet if this holds +- Var values: `[?T = ?T, ?U = ?U]` -- we learned nothing about the values of the variables + +In short, the query result says that it is too soon to say much about +whether this trait is proven. During type-checking, this is not an +immediate error: instead, the type checker would hold on to this +requirement (`Vec: Borrow`) and wait. As we'll see in the next +example, it may happen that `?T` and `?U` wind up constrained from +other sources, in which case we can try the trait query again. + +**Example 2.** We can now extend our previous example a bit, +and assign a value to `u`: + +```rust +fn foo(a: A, vec_b: Option) where A: Borrow { } + +fn main() { + // What we saw before: + let mut t: Vec<_> = vec![]; // Type: Vec + let mut u: Option<_> = None; // Type: Option + foo(t, u); // `Vec: Borrow` => ambiguous + + // New stuff: + u = Some(vec![]); // ?U = Vec +} +``` + +As a result of this assignment, the type of `u` is forced to be +`Option>`, where `?V` represents the element type of the +vector. This in turn implies that `?U` is [unified] to `Vec`. + +[unified]: ./type-checking.html + +Let's suppose that the type checker decides to revisit the +"as-yet-unproven" trait obligation we saw before, `Vec: +Borrow`. `?U` is no longer an unbound inference variable; it now +has a value, &. So, if we "refresh" the query with that value, we get: + + Vec: Borrow> + +This time, there is only one impl that applies, the reflexive impl: + + impl Borrow for T where T: ?Sized + +Therefore, the trait checker will answer: + +- Certainty: `Proven` +- Var values: `[?T = ?T, ?V = ?T]` + +Here, it is saying that we have indeed proven that the obligation +holds, and we also know that `?T` and `?V` are the same type (but we +don't know what that type is yet!). + +(In fact, as the function ends here, the type checker would give an +error at this point, since the element types of `t` and `u` are still +not yet known, even though they are known to be the same.) + + diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md index 9b71c8470..94b1d6b85 100644 --- a/src/traits-canonicalization.md +++ b/src/traits-canonicalization.md @@ -1,7 +1,10 @@ # Canonicalization Canonicalization is the process of **isolating** an inference value -from its context. It is really based on a very simple concept: every +from its context. It is a key part of implementing +[canonical queries][cq]. + +Canonicalization is really based on a very simple concept: every [inference variable](./type-inference.html#vars) is always in one of two states: either it is **unbound**, in which case we don't know yet what type it is, or it is **bound**, in which case we do. So to @@ -12,6 +15,8 @@ starting from zero and numbered in a fixed order (left to right, for the most part, but really it doesn't matter as long as it is consistent). +[cq]: ./traits-canonical-queries.html + So, for example, if we have the type `X = (?T, ?U)`, where `?T` and `?U` are distinct, unbound inference variables, then the canonical form of `X` would be `(?0, ?1)`, where `?0` and `?1` represent these diff --git a/src/traits-slg.md b/src/traits-slg.md new file mode 100644 index 000000000..cdd52ece9 --- /dev/null +++ b/src/traits-slg.md @@ -0,0 +1 @@ +# The SLG solver diff --git a/src/traits.md b/src/traits.md index 18cb0c649..6994f33d2 100644 --- a/src/traits.md +++ b/src/traits.md @@ -24,7 +24,7 @@ Trait solving is based around a few key ideas: - [Lazy normalization](./traits-associated-types.html), which is the technique we use to accommodate associated types when figuring out whether types are equal. -- [Region constraints](./traits-regions.md), which are accumulated +- [Region constraints](./traits-regions.html), which are accumulated during trait solving but mostly ignored. This means that trait solving effectively ignores the precise regions involved, always -- but we still remember the constraints on them so that those From 22b5ec479684ad8349b2173d784b9588f4512b84 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 05:45:36 -0500 Subject: [PATCH 07/13] update for notation --- src/traits-canonicalization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md index 94b1d6b85..db2f939f6 100644 --- a/src/traits-canonicalization.md +++ b/src/traits-canonicalization.md @@ -60,7 +60,7 @@ result, we'll have an array of values for the canonical inputs. For example, the canonical result might be: ``` -for<2> { +for { values = [ Vec, '1, ?0 ] ^^ ^^ ^^ these are variables in the result! ... From 53115310f72cf5fdf46a607e79aa9819957fcf34 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 06:44:29 -0500 Subject: [PATCH 08/13] rework canon section substantially to spell out steps more clearly --- src/traits-canonical-queries.md | 2 + src/traits-canonicalization.md | 175 +++++++++++++++++++++++++++----- 2 files changed, 151 insertions(+), 26 deletions(-) diff --git a/src/traits-canonical-queries.md b/src/traits-canonical-queries.md index ec861eb47..ee66a73db 100644 --- a/src/traits-canonical-queries.md +++ b/src/traits-canonical-queries.md @@ -90,6 +90,8 @@ where-clauses, that would be provable. (Internally within the solver, though, they can potentially enumerate all possible answers. See [the description of the SLG solver](./traits-slg.html) for details.) + + The response to a trait query in rustc is typically a `Result, NoSolution>` (where the `T` will vary a bit depending on the query itself). The `Err(NoSolution)` case indicates diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md index db2f939f6..fc55fac0d 100644 --- a/src/traits-canonicalization.md +++ b/src/traits-canonicalization.md @@ -2,7 +2,8 @@ Canonicalization is the process of **isolating** an inference value from its context. It is a key part of implementing -[canonical queries][cq]. +[canonical queries][cq], and you may wish to read the parent chapter +to get more context. Canonicalization is really based on a very simple concept: every [inference variable](./type-inference.html#vars) is always in one of @@ -33,6 +34,8 @@ the same answer. That answer will be expressed in terms of the canonical variables (`?0`, `?1`), which we can then map back to the original variables (`?T`, `?U`). +## Canonicalizing the query + To see how it works, imagine that we are asking to solve the following trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound. This query contains two unbound variables, but it also contains the @@ -48,54 +51,174 @@ Sometimes we write this differently, like so: for { ?0: Foo<'?1, ?2> } This `for<>` gives some information about each of the canonical -variables within. In this case, I am saying that `?0` is a type -(`T`), `?1` is a lifetime (`L`), and `?2` is also a type (`T`). The -`canonicalize` method *also* gives back a `CanonicalVarValues` array -with the "original values" for each canonicalized variable: +variables within. In this case, each `T` indicates a type variable, +so `?0` and `?2` are types; the `L` indicates a lifetime varibale, so +`?1` is a lifetime. The `canonicalize` method *also* gives back a +`CanonicalVarValues` array OV with the "original values" for each +canonicalized variable: [?A, 'static, ?B] + +We'll need this vector OV later, when we process the query response. + +## Executing the query + +Once we've constructed the canonical query, we can try to solve it. +To do so, we will wind up creating a fresh inference context and +**instantiating** the canonical query in that context. The idea is that +we create a substitution S from the canonical form containing a fresh +inference variable (of suitable kind) for each canonical variable. +So, for our example query: -Now we do the query and get back some result R. As part of that -result, we'll have an array of values for the canonical inputs. For -example, the canonical result might be: + for { ?0: Foo<'?1, ?2> } + +the substitution S might be: + + S = [?A, '?B, ?C] + +We can then replace the bound canonical variables (`?0`, etc) with +these inference variables, yielding the following fully instantiated +query: + + ?A: Foo<'?B, ?C> + +Remember that substitution S though! We're going to need it later. + +OK, now that we have a fresh inference context and an instantiated +query, we can go ahead and try to solve it. The trait solver itself is +explained in more detail in [another section](./traits-slg.html), but +suffice to say that it will compute a [certainty value][cqqr] (`Proven` or +`Ambiguous`) and have side-effects on the inference variables we've +created. For example, if there were only one impl of `Foo`, like so: + +[cqqr]: ./traits-canonical-queries.html#query-response ``` -for { - values = [ Vec, '1, ?0 ] - ^^ ^^ ^^ these are variables in the result! - ... -} +impl<'a, X> Foo<'a, X> for Vec +where X: 'a +{ ... } ``` -Note that this result is itself canonical and may include some -variables (in this case, `?0`). +then we might wind up with a certainty value of `Proven`, as well as +creating fresh inference variables `'?D` and `?E` (to represent the +parameters on the impl) and unifying as follows: + +- `'?B = '?D` +- `?A = Vec` +- `?C = ?E` + +We would also accumulate the region constraint `?E: '?D`, due to the +where clause. + +In order to create our final query result, we have to "lift" these +values out of the query's inference context and into something that +can be reapplied in our original inference context. We do that by +**re-applying canonicalization**, but to the **query result**. -What we want to do conceptually is to (a) instantiate each of the -canonical variables in the result with a fresh inference variable -and then (b) unify the values in the result with the original values. -Doing step (a) would yield a result of +## Canonicalizing the query result + +As discussed in [the parent section][cqqr], most trait queries wind up +with a result that brings together a "certainty value" `certainty`, a +result substitution `var_values`, and some region constraints. To +create this, we wind up re-using the substitution S that we created +when first instantiating our query. To refresh your memory, we had a query + + for { ?0: Foo<'?1, ?2> } + +for which we made a substutition S: + + S = [?A, '?B, ?C] + +We then did some work which unified some of those variables with other things. If we +"refresh" S with the latest results, we get: + + S = [Vec, '?D, ?E] + +These are precisely the new values for the three input variables from +our original query. Note though that they include some new variables +(like `?E`). We can make those go away by canonicalizing again! We don't +just canonicalize S, though, we canonicalize the whole query response QR: + + QR = { + certainty: Proven, // or whatever + var_values: [Vec, '?D, ?E] // this is S + region_constraints: [?E: '?D], // from the impl + value: (), // for our purposes, just (), but + // in some cases this might have + // a type or other info + } + +The result would be as follows: + + Canonical(QR) = for { + certainty: Proven, + var_values: [Vec, '?1, ?2] + region_constraints: [?2: '?1], + value: (), + } + +(One subtle point: when we canonicalize the query **result**, we do not +use any special treatment for free lifetimes. Note that both +references to `'?D`, for example, were converted into the same +canonical variable (`?1`). This is in contrast to the original query, +where we canonicalized every free lifetime into a fresh canonical +variable.) + +Now, this result must be reapplied in each context where needed. + +## Processing the canonicalized query result + +In the previous section we produced a canonical query result. We now have +to apply that result in our original context. If you recall, way back in the +beginning, we were trying to prove this query: + + ?A: Foo<'static, ?B> + +We canonicalized that into this: + + for { ?0: Foo<'?1, ?2> } + +and now we got back a canonical response: + + for { + certainty: Proven, + var_values: [Vec, '?1, ?2] + region_constraints: [?2: '?1], + value: (), + } + +We now want to apply that response to our context. Conceptually, how +we do that is to (a) instantiate each of the canonical variables in +the result with a fresh inference variable, (b) unify the values in +the result with the original values, and then (c) record the region +constraints for later. Doing step (a) would yield a result of ``` { - values = [ Vec, '?X, ?C ] - ^^ ^^^ fresh inference variables in `self` - .. -} + certainty: Proven, + var_values: [Vec, '?D, ?C] + ^^ ^^^ fresh inference variables + region_constraints: [?C: '?D], + value: (), +} ``` Step (b) would then unify: ``` ?A with Vec -'static with '?X +'static with '?D ?B with ?C ``` -(What we actually do is a mildly optimized variant of that: Rather +And finally the region constraint of `?C: 'static` would be recorded +for later verification. + +(What we *actually* do is a mildly optimized variant of that: Rather than eagerly instantiating all of the canonical values in the result with variables, we instead walk the vector of values, looking for cases where the value is just a canonical variable. In our example, `values[2]` is `?C`, so that we means we can deduce that `?C := ?B and -`'?X := 'static`. This gives us a partial set of values. Anything for +`'?D := 'static`. This gives us a partial set of values. Anything for which we do not find a value, we create an inference variable.) From 95f99572771272df3a196662211a8d95b6ca21ef Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 07:04:16 -0500 Subject: [PATCH 09/13] numerous edits --- src/SUMMARY.md | 6 +++--- src/glossary.md | 3 +++ src/traits-associated-types.md | 2 ++ src/traits-goals-and-clauses.md | 18 +++++++++++++---- src/traits-lowering-rules.md | 35 +++++++++++++++++---------------- src/traits-lowering-to-logic.md | 23 ++++++++++++---------- 6 files changed, 53 insertions(+), 34 deletions(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 95a5ee577..6612372be 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -24,11 +24,11 @@ - [Trait solving (new-style)](./traits.md) - [Lowering to logic](./traits-lowering-to-logic.md) - [Goals and clauses](./traits-goals-and-clauses.md) - - [Lowering rules](./traits-lowering-rules.md) + - [Equality and associated types](./traits-associated-types.md) + - [Region constraints](./traits-regions.md) - [Canonical queries](./traits-canonical-queries.md) - [Canonicalization](./traits-canonicalization.md) - - [Equality and associated types](./traits-associated-types.md) - - [Region constraints](./traits-regions.md) + - [Lowering rules](./traits-lowering-rules.md) - [Well-formedness checking](./traits-wf.md) - [The SLG solver](./traits-slg.md) - [Bibliography](./traits-bibliography.md) diff --git a/src/glossary.md b/src/glossary.md index 7152cba36..e542d4e35 100644 --- a/src/glossary.md +++ b/src/glossary.md @@ -31,10 +31,12 @@ LTO | Link-Time Optimizations. A set of optimizations offer [LLVM] | (actually not an acronym :P) an open-source compiler backend. It accepts LLVM IR and outputs native binaries. Various languages (e.g. Rust) can then implement a compiler front-end that output LLVM IR and use LLVM to compile to all the platforms LLVM supports. MIR | the Mid-level IR that is created after type-checking for use by borrowck and trans ([see more](./mir.html)) miri | an interpreter for MIR used for constant evaluation ([see more](./miri.html)) +normalize | a general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](./traits-associated-types.html#normalize) newtype | a "newtype" is a wrapper around some other type (e.g., `struct Foo(T)` is a "newtype" for `T`). This is commonly used in Rust to give a stronger type for indices. NLL | [non-lexical lifetimes](./mir-regionck.html), an extension to Rust's borrowing system to make it be based on the control-flow graph. node-id or NodeId | an index identifying a particular node in the AST or HIR; gradually being phased out and replaced with `HirId`. obligation | something that must be proven by the trait system ([see more](trait-resolution.html)) +projection | a general term for a "relative path", e.g. `x.f` is a "field projection", and `T::Item` is an ["associated type projection"](./traits-goals-and-clauses.html#trait-ref) promoted constants | constants extracted from a function and lifted to static scope; see [this section](./mir.html#promoted) for more details. provider | the function that executes a query ([see more](query.html)) quantified | in math or logic, existential and universal quantification are used to ask questions like "is there any type T for which is true?" or "is this true for all types T?"; see [the background chapter for more](./background.html#quantified) @@ -49,6 +51,7 @@ span | a location in the user's source code, used for error substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap`) tcx | the "typing context", main data structure of the compiler ([see more](ty.html)) 'tcx | the lifetime of the currently active inference context ([see more](ty.html)) +trait reference | the name of a trait along with a suitable set of input type/lifetimes ([see more](./traits-goals-and-clauses.html#trait-ref)) token | the smallest unit of parsing. Tokens are produced after lexing ([see more](the-parser.html)). [TLS] | Thread-Local Storage. Variables may be defined so that each thread has its own copy (rather than all threads sharing the variable). This has some interactions with LLVM. Not all platforms support TLS. trans | the code to translate MIR into LLVM IR. diff --git a/src/traits-associated-types.md b/src/traits-associated-types.md index a640bf032..6ac3fc512 100644 --- a/src/traits-associated-types.md +++ b/src/traits-associated-types.md @@ -20,6 +20,8 @@ that syntax is expanded during ["type collection"](./type-checking.html) into the explicit form, though that is something we may want to change in the future.) + + In some cases, associated type projections can be **normalized** -- that is, simplified -- based on the types given in an impl. So, to continue with our example, the impl of `IntoIterator` for `Option` diff --git a/src/traits-goals-and-clauses.md b/src/traits-goals-and-clauses.md index ad1655726..92e1b67d9 100644 --- a/src/traits-goals-and-clauses.md +++ b/src/traits-goals-and-clauses.md @@ -12,12 +12,14 @@ a few new superpowers. In Rust's solver, **goals** and **clauses** have the following forms (note that the two definitions reference one another): - Goal = DomainGoal + Goal = DomainGoal // defined in the section below | Goal && Goal | Goal || Goal | exists { Goal } // existential quantification | forall { Goal } // universal quantification | if (Clause) { Goal } // implication + | true // something that's trivially true + | ambiguous // something that's never provable Clause = DomainGoal | Clause :- Goal // if can prove Goal, then Clause is true @@ -39,9 +41,11 @@ gives the details. ## Domain goals + + To define the set of *domain goals* in our system, we need to first introduce a few simple formulations. A **trait reference** consists of -the name of a trait allow with a suitable set of inputs P0..Pn: +the name of a trait along with a suitable set of inputs P0..Pn: TraitRef = P0: TraitName @@ -50,7 +54,9 @@ IntoIterator`. Note that Rust surface syntax also permits some extra things, like associated type bindings (`Vec: IntoIterator`), that are not part of a trait reference. -A **projection** consists of a an associated item reference along with + + +A **projection** consists of an associated item reference along with its inputs P0..Pm: Projection = >::AssocItem @@ -77,7 +83,9 @@ Given that, we can define a `DomainGoal` as follows: 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) -- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be normalized + - 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 @@ -85,6 +93,8 @@ Given that, we can define a `DomainGoal` as follows: *well-formed* - well-formedness is important to [implied bounds]. +[n]: ./traits-associated-types.html#normalize + ## Coinductive goals diff --git a/src/traits-lowering-rules.md b/src/traits-lowering-rules.md index d096b4364..46827dce5 100644 --- a/src/traits-lowering-rules.md +++ b/src/traits-lowering-rules.md @@ -1,8 +1,8 @@ # Lowering rules This section gives the complete lowering rules for Rust traits into -[program clauses][pc]. These rules reference the [domain goals][dg] defined in -an earlier section. +[program clauses][pc]. It is a kind of reference. These rules +reference the [domain goals][dg] defined in an earlier section. [pc]: ./traits-goals-and-clauses.html [dg]: ./traits-goals-and-clauses.html#domain-goals @@ -22,7 +22,7 @@ definitions; these macros reference other sections within this chapter. ## Lowering where clauses -When used in a goal position, where clauses can be mapped directly +When used in a goal position, where clauses can be mapped directly to [domain goals][dg], as follows: - `A0: Foo` maps to `Implemented(A0: Foo)`. @@ -72,12 +72,12 @@ inside the `{}`. ### Trait header From the trait itself we mostly make "meta" rules that setup the -relationships between different kinds of domain goals. The first dush +relationships between different kinds of domain goals. The first such rule from the trait header creates the mapping between the `FromEnv` and `Implemented` predicates: forall { - Implemented(Self: Trait) :- FromEnv(Self: Trait) :- FromEnv(Self: Trait) } @@ -114,7 +114,7 @@ to be **well-formed**: // For each where clause WC: forall { - WellFormed(Self: Trait) :- Implemented(Self: Trait), WellFormed(WC) + WellFormed(Self: Trait) :- Implemented(Self: Trait) && WellFormed(WC) } This `WellFormed` rule states that `T: Trait` is well-formed if (a) @@ -150,7 +150,7 @@ one of those: This `WellFormed` predicate is only used when proving that impls are well-formed -- basically, for each impl of some trait ref `TraitRef`, -we must that `WellFormed(TraitRef)`. This in turn justifies the +we must show that `WellFormed(TraitRef)`. This in turn justifies the implied bounds rules that allow us to extend the set of `FromEnv` items. @@ -170,9 +170,10 @@ where WC } ``` -We will produce a number of program clases. The first two define +We will produce a number of program clauses. The first two define the rules by which `ProjectionEq` can succeed; these two clauses are discussed -in detail in the [section on associated types](./traits-associated-types.html). +in detail in the [section on associated types](./traits-associated-types.html),, +but reproduced here for reference: // ProjectionEq can succeed by normalizing: forall { @@ -180,7 +181,8 @@ in detail in the [section on associated types](./traits-associated-types.html). Normalize(>::AssocType -> U) } - // ProjectionEq can succeed by skolemizing: + // ProjectionEq can succeed by skolemizing, see "associated type" + // chapter for more: forall { ProjectionEq( >::AssocType = @@ -188,13 +190,13 @@ in detail in the [section on associated types](./traits-associated-types.html). ) :- // But only if the trait is implemented, and the conditions from // the associated type are met as well: - Implemented(Self: Trait), - WC1 + Implemented(Self: Trait) + && WC1 } The next rule covers implied bounds for the projection. In particular, the `Bounds` declared on the associated type must be proven to hold to -show that the impl is well-formed, and hence we can rely on them from +show that the impl is well-formed, and hence we can rely on them elsewhere. // XXX how exactly should we set this up? Have to be careful; @@ -237,7 +239,7 @@ Given an impl that contains: impl Trait for A0 where WC { - type AssocType: Bounds where WC1 = T; + type AssocType where WC1 = T; } ``` @@ -246,13 +248,12 @@ We produce the following rule: forall { forall { Normalize(>::AssocType -> T) :- - WC, WC1 + WC && WC1 } } Note that `WC` and `WC1` both encode where-clauses that the impl can -rely on, whereas the bounds `Bounds` on the associated type are things -that the impl must prove (see the well-formedness checking). +rely on. diff --git a/src/traits-lowering-to-logic.md b/src/traits-lowering-to-logic.md index 7b1c2ed6b..4e4e7cae9 100644 --- a/src/traits-lowering-to-logic.md +++ b/src/traits-lowering-to-logic.md @@ -33,6 +33,9 @@ Prolog-like notation, as follows: ``` Clone(usize). Clone(Vec) :- Clone(?T). + +// The notation `A :- B` means "A is true if B is true". +// Or, put another way, B implies A. ``` In Prolog terms, we might say that `Clone(Foo)` -- where `Foo` is some @@ -82,20 +85,20 @@ let's turn our focus a bit towards **type-checking**. Type-checking is interesting because it is what gives us the goals that we need to prove. That is, everything we've seen so far has been about how we derive the rules by which we can prove goals from the traits and impls -in the program; but we are also interesting in how derive the goals +in the program; but we are also interested in how to derive the goals that we need to prove, and those come from type-checking. Consider type-checking the function `foo()` here: ```rust fn foo() { bar::() } -fn bar() { } +fn bar>() { } ``` This function is very simple, of course: all it does is to call `bar::()`. Now, looking at the definition of `bar()`, we can see -that it has one where-clause `U: Eq`. So, that means that `foo()` will -have to prove that `usize: Eq` in order to show that it can call `bar()` +that it has one where-clause `U: Eq`. So, that means that `foo()` will +have to prove that `usize: Eq` in order to show that it can call `bar()` with `usize` as the type argument. If we wanted, we could write a Prolog predicate that defines the @@ -103,7 +106,7 @@ conditions under which `bar()` can be called. We'll say that those conditions are called being "well-formed": ``` -barWellFormed(?U) :- Eq(?U). +barWellFormed(?U) :- Eq(?U, ?U). ``` Then we can say that `foo()` type-checks if the reference to @@ -118,7 +121,7 @@ If we try to prove the goal `fooTypeChecks`, it will succeed: - `fooTypeChecks` is provable if: - `barWellFormed(usize)`, which is provable if: - - `Eq(usize)`, which is provable because of an impl. + - `Eq(usize, usize)`, which is provable because of an impl. Ok, so far so good. Let's move on to type-checking a more complex function. @@ -132,8 +135,8 @@ can be provide. To see what I'm talking about, let's revamp our previous example to make `foo` generic: ```rust -fn foo() { bar::() } -fn bar() { } +fn foo>() { bar::() } +fn bar>() { } ``` To type-check the body of `foo`, we need to be able to hold the type @@ -145,8 +148,8 @@ this like so: fooTypeChecks :- // for all types T... forall { - // ...if we assume that Eq(T) is provable... - if (Eq(T)) { + // ...if we assume that Eq(T, T) is provable... + if (Eq(T, T)) { // ...then we can prove that `barWellFormed(T)` holds. barWellFormed(T) } From 7a78a998cea262950d04f291618ba7ea7540d517 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 07:06:36 -0500 Subject: [PATCH 10/13] add implied bounds placeholder --- src/SUMMARY.md | 1 + src/traits-implied-bounds.md | 9 +++++++++ 2 files changed, 10 insertions(+) create mode 100644 src/traits-implied-bounds.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 6612372be..8aa450b7b 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -25,6 +25,7 @@ - [Lowering to logic](./traits-lowering-to-logic.md) - [Goals and clauses](./traits-goals-and-clauses.md) - [Equality and associated types](./traits-associated-types.md) + - [Implied bounds](./traits-implied-bounds.md) - [Region constraints](./traits-regions.md) - [Canonical queries](./traits-canonical-queries.md) - [Canonicalization](./traits-canonicalization.md) diff --git a/src/traits-implied-bounds.md b/src/traits-implied-bounds.md new file mode 100644 index 000000000..26a63bf32 --- /dev/null +++ b/src/traits-implied-bounds.md @@ -0,0 +1,9 @@ +# Implied Bounds + +*to be written* + +Cover: + +- Why the `FromEnv` setup etc is the way it is +- Perhaps move some of the material from 'lowering rules' in to here +- Show various examples where you could go wrong From 994a38b19802a8982f413ba6c769c4ccecb80888 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 07:09:25 -0500 Subject: [PATCH 11/13] update the summary landing page --- src/traits.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/traits.md b/src/traits.md index 6994f33d2..b75e7fec6 100644 --- a/src/traits.md +++ b/src/traits.md @@ -16,8 +16,10 @@ Trait solving is based around a few key ideas: - [Lowering to logic](./traits-lowering-to-logic.html), which expresses Rust traits in terms of standard logical terms. - The [goals and clauses](./traits-goals-and-clauses.html) chapter - describes the precise lowering rules we use. -- [Canonical queries](./traits-canonicalization.html), which allow us + describes the precise form of rules we use, and + [lowering rules](./lowering-rules.html) gives the complete set of + lowering rules in a more reference-like form. +- [Canonical queries](./traits-canonical-queries.html), which allow us to solve trait problems (like "is `Foo` implemented for the type `Bar`?") once, and then apply that same result independently in many different inference contexts. From d9f0a45a045c7901cf2c36b4134f5f96db5e959c Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 07:10:44 -0500 Subject: [PATCH 12/13] fix link --- src/traits.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/traits.md b/src/traits.md index b75e7fec6..175e6418b 100644 --- a/src/traits.md +++ b/src/traits.md @@ -17,7 +17,7 @@ Trait solving is based around a few key ideas: Rust traits in terms of standard logical terms. - The [goals and clauses](./traits-goals-and-clauses.html) chapter describes the precise form of rules we use, and - [lowering rules](./lowering-rules.html) gives the complete set of + [lowering rules](./traits-lowering-rules.html) gives the complete set of lowering rules in a more reference-like form. - [Canonical queries](./traits-canonical-queries.html), which allow us to solve trait problems (like "is `Foo` implemented for the type From 49e8e092c12a6bf97ec240eb65f8d6713e4088a4 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 10 Mar 2018 07:11:11 -0500 Subject: [PATCH 13/13] trailing whitespace --- src/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 8aa450b7b..d4ee59abf 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -21,7 +21,7 @@ - [Higher-ranked trait bounds](./trait-hrtb.md) - [Caching subtleties](./trait-caching.md) - [Specialization](./trait-specialization.md) -- [Trait solving (new-style)](./traits.md) +- [Trait solving (new-style)](./traits.md) - [Lowering to logic](./traits-lowering-to-logic.md) - [Goals and clauses](./traits-goals-and-clauses.md) - [Equality and associated types](./traits-associated-types.md)