diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index de094592a6f..7e76f6cb452 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -21,7 +21,7 @@ - [Opaque types (impl Trait)](./clauses/opaque_types.md) - [Well known traits](./clauses/well_known_traits.md) - [Well-formedness checking](./clauses/wf.md) - - [Coherence](./coherence.md) + - [Coherence](./clauses/coherence.md) - [Canonical queries](./canonical_queries.md) - [Canonicalization](./canonical_queries/canonicalization.md) - [Chalk engine](./engine.md) diff --git a/book/src/clauses/coherence.md b/book/src/clauses/coherence.md index b92e06ec0cf..81a5678bb2d 100644 --- a/book/src/clauses/coherence.md +++ b/book/src/clauses/coherence.md @@ -61,7 +61,7 @@ Thus, it is probably best to look at the only *truly authoritative* source on th ## The Orphan Check in rustc -The orphan check as implemented today in the Rust compiler takes place in the `[orphan_check](https://github.com/rust-lang/rust/blob/b7c6e8f1805cd8a4b0a1c1f22f17a89e9e2cea23/src/librustc/traits/coherence.rs#L236)` function which is called [for every declared impl](https://github.com/rust-lang/rust/blob/b7c6e8f1805cd8a4b0a1c1f22f17a89e9e2cea23/src/librustc_typeck/coherence/orphan.rs#L45). Since implementations for locally defined traits are always defined, that function returns OK if the trait being implemented is local. Otherwise, it dispatches to the `[orphan_check_trait_ref](https://github.com/rust-lang/rust/blob/b7c6e8f1805cd8a4b0a1c1f22f17a89e9e2cea23/src/librustc/traits/coherence.rs#L343)` function which does the major orphan rules checking. +The orphan check as implemented today in the Rust compiler takes place in the [`orphan_check`](https://github.com/rust-lang/rust/blob/b7c6e8f1805cd8a4b0a1c1f22f17a89e9e2cea23/src/librustc/traits/coherence.rs#L236) function which is called [for every declared impl](https://github.com/rust-lang/rust/blob/b7c6e8f1805cd8a4b0a1c1f22f17a89e9e2cea23/src/librustc_typeck/coherence/orphan.rs#L45). Since implementations for locally defined traits are always defined, that function returns OK if the trait being implemented is local. Otherwise, it dispatches to the [`orphan_check_trait_ref`](https://github.com/rust-lang/rust/blob/b7c6e8f1805cd8a4b0a1c1f22f17a89e9e2cea23/src/librustc/traits/coherence.rs#L343) function which does the major orphan rules checking. Recall that the impls we are dealing with are in the form `impl Trait for P0`. @@ -90,37 +90,39 @@ Here’s how the lowering rules would look: For each trait `Trait`, - If `Trait` is local to the current crate, we generate: - forall { LocalImplAllowed(Self: Trait) } + `forall { LocalImplAllowed(Self: Trait) }` This models that any impls are allowed if the trait is local to the current crate. - If `Trait` is upstream to the current crate, we need a rule which models the additional conditions on which impls are allowed: - forall { LocalImplAllowed(Self: Trait) :- IsLocal(Self) } - forall { - LocalImplAllowed(Self: Trait) :- IsFullyVisible(Self), IsLocal(P1) - } - forall { - LocalImplAllowed(Self: Trait) :- - IsFullyVisible(Self), - IsFullyVisible(P1), - IsLocal(P2) - } - forall { - LocalImplAllowed(Self: Trait) :- - IsFullyVisible(Self), - IsFullyVisible(P1), - IsFullyVisible(P2), - IsLocal(P3) - } +```ignore +forall { LocalImplAllowed(Self: Trait) :- IsLocal(Self) } +forall { + LocalImplAllowed(Self: Trait) :- IsFullyVisible(Self), IsLocal(P1) +} +forall { + LocalImplAllowed(Self: Trait) :- + IsFullyVisible(Self), + IsFullyVisible(P1), + IsLocal(P2) +} +forall { + LocalImplAllowed(Self: Trait) :- + IsFullyVisible(Self), + IsFullyVisible(P1), + IsFullyVisible(P2), + IsLocal(P3) +} +... +forall { + LocalImplAllowed(Self: Trait) :- + IsFullyVisible(Self), + IsFullyVisible(P1), + IsFullyVisible(P2), ... - forall { - LocalImplAllowed(Self: Trait) :- - IsFullyVisible(Self), - IsFullyVisible(P1), - IsFullyVisible(P2), - ... - IsFullyVisible(Pn-1), - IsLocal(Pn) - } - Here, we have modelled every possible case of `P1` to `Pn` being local and then checked if all prior type parameters are fully visible. This truly is a direct translation of the rules listed above! + IsFullyVisible(Pn-1), + IsLocal(Pn) +} +``` +Here, we have modelled every possible case of `P1` to `Pn` being local and then checked if all prior type parameters are fully visible. This truly is a direct translation of the rules listed above! Now, to complete the orphan check, we can iterate over each impl of the same form as before and check if `LocalImplAllowed(P0: Trait)` is provable. @@ -131,16 +133,20 @@ The purpose of the overlap check is to ensure that there is only up to one impl This is a simple application of the mathematical law: -> If two sets $$A$$ and $$B$$ are disjoint, then $$A\cap B = \emptyset$$ +> If two sets *A* and *B* are disjoint, then *A* ∩ *B* = ∅ More concretely, let’s say you have the following two impls: ([example from RFC 1023](https://rust-lang.github.io/rfcs/1023-rebalancing-coherence.html#type-locality-and-negative-reasoning)) - impl Clone for T {..} - impl Clone for MyType {..} +```rust,ignore +impl Clone for T { /* ... */ } +impl Clone for MyType { /* ... */ } +``` Then we’ll try to solve the following: - not { exists { T = MyType, T: Copy } } +```ignore +not { exists { T = MyType, T: Copy } } +``` One way to read this is to say “try to prove that there is no `MyType` for any `U` that implements the `Copy` trait”. The reason we’re trying to prove this is because if there is such an implementation, then the second impl would overlap with the first one. The first impl applies to any type that implements `Copy`. @@ -181,47 +187,51 @@ This significantly narrows down our set of potential impls that we need to accou For downstream crates, we need to add rules for all possible impls that they could potentially add using any upstream traits or traits in the current crate. We can do this by enumerating the possibilities generated from the orphan rules specified above: - - // Given a trait MyTrait where WCs - - forall { - Implemented(Self: MyTrait) :- - WCs, // where clauses - Compatible, - DownstreamType(Self), // local to a downstream crate - CannotProve, - } - forall { - Implemented(Self: MyTrait) :- - WCs, - Compatible, - IsFullyVisible(Self), - DownstreamType(P1), - CannotProve, - } - ... - forall { - Implemented(Self: MyTrait) :- - WCs, - Compatible, - IsFullyVisible(Self), - IsFullyVisible(P1), - ..., - IsFullyVisible(Pn-1), - DownstreamType(Pn), - CannotProve, - } +```ignore +// Given a trait MyTrait where WCs + +forall { + Implemented(Self: MyTrait) :- + WCs, // where clauses + Compatible, + DownstreamType(Self), // local to a downstream crate + CannotProve, +} +forall { + Implemented(Self: MyTrait) :- + WCs, + Compatible, + IsFullyVisible(Self), + DownstreamType(P1), + CannotProve, +} +... +forall { + Implemented(Self: MyTrait) :- + WCs, + Compatible, + IsFullyVisible(Self), + IsFullyVisible(P1), + ..., + IsFullyVisible(Pn-1), + DownstreamType(Pn), + CannotProve, +} +``` Perhaps somewhat surprisingly, `IsFullyVisible` works here too. This is because our previous definition of the lowering for `IsFullyVisible` was quite broad. By lowering *all* types in the current crate and in upstream crates with `IsFullyVisible`, that predicate covers the correct set of types here too. The orphan rules only require that there are no types parameters prior to the first local type. Types that are not type parameters and also by definition not downstream types are all of the types in the current crate and in upstream crates. This is exactly what `IsFullyVisible` covers. Fundamental types in both the current crate and in upstream crates can be considered local in a downstream crate if they are provided with a downstream type. To model this, we can add an additional rule for fundamental types: - - forall { DownstreamType(MyFundamentalType) :- DownstreamType(T) } +```ignore +forall { DownstreamType(MyFundamentalType) :- DownstreamType(T) } +``` **Where clauses:** Traits can have where clauses. - #[upstream] trait Foo where Self: Eq { ... } +```rust,ignore +#[upstream] trait Foo where Self: Eq { /* ... */ } +``` **The question is**: do we need to bring these where clauses down into the rule that we generate for the overlap check? **Answer:** Yes. Since the trait can only be implemented for types that satisfy its where clauses, it makes sense to also limit our assumption of compatible impls to impls that can exist. @@ -234,60 +244,79 @@ Thus, based on the discussion above, the overlap check with coherence in mind ca - All disjoint queries take place inside of `compatible` + - `compatible { G }` desugars into `forall { (Compatible, DownstreamType(T)) => G }`, thus introducing a `Compatible` predicate using implication + - For each upstream trait `MyTrait`, we lower it into the following rule: - forall { - Implemented(Self: MyTrait) :- - Compatible, - IsUpstream(Self), - IsUpstream(P1), - ..., - IsUpstream(Pn), - CannotProve - } - This will accomplish our goal of returning an ambiguous answer whenever the overlap check query asks about any impls that an upstream crate may add in a compatible way. We determined in the discussion above that these are the only impls in any crate that can be added compatibly. - **Note:** Trait where clauses are lowered into the rule’s conditions as well as a prerequisite to everything else. + + ```ignore + forall { + Implemented(Self: MyTrait) :- + Compatible, + IsUpstream(Self), + IsUpstream(P1), + ..., + IsUpstream(Pn), + CannotProve + } + ``` + + This will accomplish our goal of returning an ambiguous answer whenever the +overlap check query asks about any impls that an upstream crate may add in a +compatible way. We determined in the discussion above that these are the only +impls in any crate that can be added compatibly. + + **Note:** Trait `where` clauses are lowered into the rule’s conditions as well as a prerequisite to everything else. + - For all traits `MyTrait where WCs` in the current crate and in upstream traits, - forall { - Implemented(Self: MyTrait) :- - WCs, // where clauses - Compatible, - DownstreamType(Self), // local to a downstream crate - CannotProve, - } - forall { - Implemented(Self: MyTrait) :- - WCs, - Compatible, - IsFullyVisible(Self), - DownstreamType(P1), - CannotProve, - } - ... - forall { - Implemented(Self: MyTrait) :- - WCs, - Compatible, - IsFullyVisible(Self), - IsFullyVisible(P1), - ..., - IsFullyVisible(Pn-1), - DownstreamType(Pn), - CannotProve, - } + ```ignore + forall { + Implemented(Self: MyTrait) :- + WCs, // where clauses + Compatible, + DownstreamType(Self), // local to a downstream crate + CannotProve, + } + forall { + Implemented(Self: MyTrait) :- + WCs, + Compatible, + IsFullyVisible(Self), + DownstreamType(P1), + CannotProve, + } + ... + forall { + Implemented(Self: MyTrait) :- + WCs, + Compatible, + IsFullyVisible(Self), + IsFullyVisible(P1), + ..., + IsFullyVisible(Pn-1), + DownstreamType(Pn), + CannotProve, + } + ``` + - For fundamental types in both the current crate and in upstream crates, - forall { DownstreamType(MyFundamentalType) :- DownstreamType(T) } + ```ignore + forall { DownstreamType(MyFundamentalType) :- DownstreamType(T) } + ``` + ## Alternative Designs Initially, when Niko and I started working on this, Niko suggested the following implementation: -- For each upstream trait, `MyTrait`, we lower it into the following rule: - forall { - Implemented(Self: MyTrait) :- - Compatible, - not { LocalImplAllowed(Self: MyTrait) }, - CannotProve - } +> For each upstream trait, `MyTrait`, we lower it into the following rule: +> ```ignore +> forall { +> Implemented(Self: MyTrait) :- +> Compatible, +> not { LocalImplAllowed(Self: MyTrait) }, +> CannotProve +> } +> ``` This appears to make sense because we need to assume that any impls that the current crate cannot add itself may exist somewhere else. By using `not { LocalImplAllowed(…) }`, we modelled exactly that. The problem is, that this assumption is actually too strong. What we actually need to model is that any **compatible** impls that the current crate cannot add itself may exist somewhere else. This is a **subset** of the impls covered by `not { LocalImplAllowed(…) }`. diff --git a/book/src/glossary.md b/book/src/glossary.md index b6667e731a7..270b643b250 100644 --- a/book/src/glossary.md +++ b/book/src/glossary.md @@ -2,6 +2,34 @@ This is a glossary of terminology (possibly) used in the chalk crate. +## Notation + +### Basic notation + +| Notation | Meaning | +|--------------|-----------------------------------------| +| `?0` | [Type inference variable] | +| `^0`, `^1.0` | [Bound variable]; bound in a [`forall`] | +| `!0`, `!1.0` | [Placeholder] | +| `A :- B` | [Clause]; A is true if B is true | + +### Rules + +- `forall { (Vec: Clone) :- (T: Clone)`: for every `T`, `Vec` + implements `Clone` if `T` implements `Clone` + +### Queries + +- `Vec: Clone`: does `Vec` implement `Clone`? +- `exists { Vec: Clone }`: does there exist a `T` such that `Vec` + implements `Clone`? + +[Type inference variable]: ../types/rust_types.md#inference-variables +[Bound variable]: ../types/rust_types.md#bound-variables +[`forall`]: #debruijn-index +[Placeholder]: ../types/rust_types.md#placeholders +[Clause]: ../clauses/goals_and_clauses.md + ## Binary connective There are sixteen logical connectives on two boolean variables. The most interesting in this context are listed below. There is also a truth table given @@ -50,7 +78,7 @@ the optional positive literal. Due to the equivalence `(P => Q) <=> (!P || Q)` the clause can be expressed as `B && C && ... => A` which means that A is true if `B`, `C`, etc. are all true. All rules in chalk are in this form. For example -```notrust +```rust,ignore struct A {} impl B for A where T: C + D {} ``` @@ -58,7 +86,7 @@ impl B for A where T: C + D {} is expressed as the *Horn clause* `(T: C) && (T: D) => (A: B)`. This formula has to hold for all values of `T`. The second example -```notrust +```rust,ignore struct A {} impl B for A {} impl C for A {} @@ -76,6 +104,11 @@ Given the example `forall { exists { T: Foo } }` the literal names `U` and `T` are replaced with `0` and `1` respectively and the names are erased from the binders: `forall<_> { exists<_> { 1: Foo } }`. +As another example, in `forall { forall { X } }`, `X` is represented +as `^1.0`. The `1` represents the de Bruijn index of the variable and the `0` +represents the index in that scope: `X` is bound in the second scope counting +from where it is referenced, and it is the first variable bound in that scope. + ## Formula A formula is a logical expression consisting of literals and constants connected by logical operators. @@ -149,7 +182,7 @@ syntactic rules. In the context of the Rust type system this means that basic rules for type construction have to be met. Two examples: 1) Given a struct definition -```notrust +```rust,ignore struct HashSet ``` then a type `HashSet` is well-formed since `i32` implements `Hash`. A type