From 467c6eefd0cff3d4919b236eec8e0cdc6baa9fbf Mon Sep 17 00:00:00 2001 From: scalexm Date: Fri, 25 Jun 2021 00:39:16 +0200 Subject: [PATCH] Update "implied bounds" rules for types to match #206 --- book/src/clauses/implied_bounds.md | 39 ++++++++++++++---------------- book/src/clauses/lowering_rules.md | 6 ++--- 2 files changed, 21 insertions(+), 24 deletions(-) diff --git a/book/src/clauses/implied_bounds.md b/book/src/clauses/implied_bounds.md index 2b9e1efd6ed..26055e6da74 100644 --- a/book/src/clauses/implied_bounds.md +++ b/book/src/clauses/implied_bounds.md @@ -405,7 +405,7 @@ Notice that we are now also requiring `Implemented(Self: Trait)` for traversing all the implied bounds transitively. This does not change anything when checking whether impls are legal, because since we assume that the where clauses hold inside the impl, we know that the corresponding -trait reference do hold. Thanks to this setup, you can see that we indeed +trait reference does hold. Thanks to this setup, you can see that we indeed require to prove the set of all bounds transitively implied by the where clauses. @@ -462,41 +462,38 @@ are effectively visiting all the transitive implied bounds, and only these. ## Implied bounds on types -We mainly talked about implied bounds for traits because this was the most -subtle regarding implementation. Implied bounds on types are simpler, -especially because if we assume that a type is well-formed, we don't use that -fact to deduce that other types are well-formed, we only use it to deduce -that e.g. some trait bounds hold. +We mainly talked about implied bounds for traits, but implied bounds on types +are very similar. Suppose we have the following definition: -For types, we just use rules like these ones: ```rust,ignore struct Type<...> where WC1, ..., WCn { ... } ``` +To prove that `Type<...>` is well-formed, we would need to prove a goal of the +form `WellFormed(Type<...>).`. The `WellFormed(Type<...>)` predicate is defined +by the rule: + ```text forall<...> { - WellFormed(Type<...>) :- WC1, ..., WCn. + WellFormed(Type<...>) :- WellFormed(WC1), ..., WellFormed(WCn). } +``` + +Conversely, if we know a type is well-formed from our environment (for example +because it appears as an argument of one of our functions), we can have implied +bounds thanks to the below set of rules: +```text forall<...> { FromEnv(WC1) :- FromEnv(Type<...>). ... FromEnv(WCn) :- FromEnv(Type<...>). } ``` -We can see that we have this asymmetry between well-formedness check, -which only verifies that the direct superbounds hold, and implied bounds which -gives access to all bounds transitively implied by the where clauses. In that -case this is ok because as we said, we don't use `FromEnv(Type<...>)` to deduce -other `FromEnv(OtherType<...>)` things, nor do we use `FromEnv(Type: Trait)` to -deduce `FromEnv(OtherType<...>)` things. So in that sense type definitions are -"less recursive" than traits, and we saw in a previous subsection that -it was the combination of asymmetry and recursive trait / impls that led to -unsoundness. As such, the `WellFormed(Type<...>)` predicate does not need -to be co-inductive. -This asymmetry optimization is useful because in a real Rust program, we have -to check the well-formedness of types very often (e.g. for each type which -appears in the body of a function). +Looking at the above rules, we see that we can never encounter a chain of +deductions of the form `WellFormed(Type<...>) :- ... :- WellFormed(Type<...>)`. +So in contrast with traits, the `WellFormed(Type<...>)` predicate does not need +to be co-inductive. diff --git a/book/src/clauses/lowering_rules.md b/book/src/clauses/lowering_rules.md index 5fb1e3e1f78..fa15a56c063 100644 --- a/book/src/clauses/lowering_rules.md +++ b/book/src/clauses/lowering_rules.md @@ -204,12 +204,12 @@ we produce the following rule: ```text // Rule WellFormed-Type forall { - WellFormed(Type) :- WC + WellFormed(Type) :- WellFormed(WC) } ``` -Note that we use `struct` for defining a type, but this should be understood -as a general type definition (it could be e.g. a generic `enum`). +Note that we use `struct` to define a type, but this should be understood as a +general type definition (it could be e.g. a generic `enum`). Conversely, we define rules which say that if we assume that a type is well-formed, we can also assume that its where clauses hold. That is,