Add documentation

src/ir/mod.rs

@@ -469,6 +469,10 @@ impl DomainGoal {
         }
     }
 
+    /// Turn a where clause into the WF version of it i.e.:
+    /// * `T: Trait` maps to `WellFormed(T: Trait)`
+    /// * `T: Trait<Item = Foo>` maps to `WellFormed(T: Trait<Item = Foo>)`
+    /// * any other clause maps to itself
     crate fn into_well_formed_clause(self) -> DomainGoal {
         match self {
             DomainGoal::Implemented(tr) => DomainGoal::WellFormed(WellFormed::TraitRef(tr)),
@@ -477,6 +481,7 @@ impl DomainGoal {
         }
     }
 
+    /// Same as `into_well_formed_clause` but with the `FromEnv` predicate instead of `WellFormed`.
     crate fn into_from_env_clause(self) -> DomainGoal {
         match self {
             DomainGoal::Implemented(tr) => DomainGoal::FromEnv(FromEnv::TraitRef(tr)),
@@ -502,13 +507,43 @@ pub struct EqGoal {
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
+/// A predicate which is true is some object is well-formed, e.g. a type or a trait ref.
+/// For example, given the following type definition:
+///
+/// ```notrust
+/// struct Set<K> where K: Hash {
+///     ...
+/// }
+/// ```
+///
+/// then we have the following rule: `WellFormed(Set<K>) :- (K: Hash)`.
+/// See the complete rules in `lower.rs`.
 pub enum WellFormed {
     Ty(Ty),
     TraitRef(TraitRef),
     Normalize(Normalize),
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
+/// A predicate which enables deriving everything which should be true if we *know* that some object
+/// is well-formed. For example, given the following trait definitions:
+///
+/// ```notrust
+/// trait Clone { ... }
+/// trait Copy where Self: Clone { ... }
+/// ```
+///
+/// then we can use `FromEnv(T: Copy)` to derive that `T: Clone`, like in:
+///
+/// ```notrust
+/// forall<T> {
+///     if (FromEnv(T: Copy)) {
+///         T: Clone
+///     }
+/// }
+/// ```
+///
+/// See the complete rules in `lower.rs`.
 pub enum FromEnv {
     Ty(Ty),
     TraitRef(TraitRef),
@@ -718,8 +753,16 @@ impl<T> UCanonical<T> {
 }
 
 impl UCanonical<InEnvironment<Goal>> {
+<<<<<<< HEAD
     /// A goal has coinductive semantics if it is of the form `T: AutoTrait`.
     crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool {
+=======
+    /// A goal has coinductive semantics if it is of the form `T: AutoTrait`, or if it is of the
+    /// form `WellFormed(T: Trait)` where `Trait` is any trait. The latter is needed for dealing
+    /// with WF requirements and cyclic traits, which generates cycles in the proof tree which must
+    /// not be rejected but instead must be treated as a success.
+    pub fn is_coinductive(&self, program: &ProgramEnvironment) -> bool {
+>>>>>>> Add documentation
         match &self.canonical.value.goal {
             Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Implemented(tr))) => {
                 let trait_datum = &program.trait_data[&tr.trait_id];

src/lower/mod.rs

@@ -1247,8 +1247,8 @@ impl ir::StructDatum {
         //
         // we generate the following clause:
         //
-        //    for<?T> WF(Foo<?T>) :- (?T: Eq).
-        //    for<?T> FromEnv(?T: Eq) :- FromEnv(Foo<?T>).
+        //    forall<T> { WF(Foo<T>) :- (T: Eq). }
+        //    forall<T> { FromEnv(T: Eq) :- FromEnv(Foo<T>). }
 
         let wf = ir::ProgramClause {
             implication: self.binders.map_ref(|bound_datum| {
@@ -1296,13 +1296,15 @@ impl ir::TraitDatum {
         //
         //    trait Ord<T> where Self: Eq<T> { ... }
         //
-        // we generate the following clauses:
+        // we generate the following clause:
         //
-        //    for<?Self, ?T> WF(?Self: Ord<?T>) :-
-        //        (?Self: Ord<?T>), WF(?Self: Eq<?T>)
+        //    forall<Self, T> {
+        //        WF(Self: Ord<T>) :- (Self: Ord<T>), WF(Self: Eq<T>)
+        //    }
         //
-        //    for<?Self, ?T> (?Self: Ord<T>) :- FromEnv(?Self: Ord<T>)
-        //    for<?Self, ?T> FromEnv(?Self: Ord<?T>) :- FromEnv(?Self: Ord<T>)
+        // and the reverse rules:
+        //    forall<Self, T> { (Self: Ord<T>) :- FromEnv(Self: Ord<T>) }
+        //    forall<Self, T> { FromEnv(Self: Ord<T>) :- FromEnv(Self: Ord<T>) }
 
         let trait_ref = self.binders.value.trait_ref.clone();
 
@@ -1387,6 +1389,9 @@ impl ir::AssociatedTyDatum {
         // `ProjectionEq` to fallback *or* normalize it. So instead we
         // handle this kind of reasoning by expanding "projection
         // equality" predicates (see `DomainGoal::expanded`).
+        //
+        // We also generate rules specific to WF requirements and implied bounds,
+        // see below.
 
         let binders: Vec<_> = self.parameter_kinds
             .iter()
@@ -1434,6 +1439,12 @@ impl ir::AssociatedTyDatum {
             },
         });
 
+        // The above application type is always well-formed, and `<T as Foo>::Assoc` will
+        // unify with `(Foo::Assoc)<T>` only if `T: Foo`, because of the above rule, so we have:
+        //
+        //    forall<T> {
+        //        WellFormed((Foo::Assoc)<T>).
+        //    }
         clauses.push(ir::ProgramClause {
             implication: ir::Binders {
                 binders: binders.clone(),
@@ -1470,6 +1481,14 @@ impl ir::AssociatedTyDatum {
             });
 
 
+        // We generate a proxy rule for the well-formedness of `T: Foo<Assoc = U>` which really
+        // means two things: `T: Foo` and `Normalize(<T as Foo>::Assoc -> U)`. So we have the
+        // following rule:
+        //
+        //    forall<T> {
+        //        WellFormed(T: Foo<Assoc = U>) :-
+        //            WellFormed(T: Foo), Normalize(<T as Foo>::Assoc -> U)
+        //    }
         clauses.push(ir::ProgramClause {
             implication: ir::Binders {
                 binders: binders.clone(),
@@ -1483,6 +1502,11 @@ impl ir::AssociatedTyDatum {
             }
         });
 
+        // We also have two proxy reverse rules, the first one being:
+        //
+        //    forall<T> {
+        //        FromEnv(T: Foo) :- FromEnv(T: Foo<Assoc = U>)
+        //    }
         clauses.push(ir::ProgramClause {
             implication: ir::Binders {
                 binders: binders.clone(),
@@ -1493,6 +1517,11 @@ impl ir::AssociatedTyDatum {
             }
         });
 
+        // And the other one being:
+        //
+        //    forall<T> {
+        //        Normalize(<T as Foo>::Assoc -> U) :- FromEnv(T: Foo<Assoc = U>)
+        //    }
         clauses.push(ir::ProgramClause {
             implication: ir::Binders {
                 binders: binders,

src/lower/test.rs

@@ -32,6 +32,8 @@ macro_rules! lowering_error {
 
 
 fn parse_and_lower(text: &str) -> Result<Program> {
+    // Use the on-demand SLG solver to avoid ambiguities on projection types encountered when
+    // using the recursive solver.
     chalk_parse::parse_program(text)?.lower(SolverChoice::on_demand_slg())
 }
 

src/lower/wf.rs

@@ -41,6 +41,7 @@ impl Program {
     }
 }
 
+/// A trait for retrieving all types appearing in some Chalk construction.
 trait FoldInputTypes {
     fn fold(&self, accumulator: &mut Vec<Ty>);
 }
@@ -77,7 +78,10 @@ impl FoldInputTypes for Ty {
                 accumulator.push(self.clone());
                 proj.parameters.fold(accumulator);
             }
-            _ => (),
+
+            // Type parameters and higher-kinded types do not carry any input types (so we can sort
+            // of assume they are always WF).
+            Ty::Var(..) | Ty::ForAll(..) => (),
         }
     }
 }
@@ -108,13 +112,15 @@ impl FoldInputTypes for DomainGoal {
             DomainGoal::Implemented(ref tr) => tr.fold(accumulator),
             DomainGoal::Normalize(ref n) => n.fold(accumulator),
             DomainGoal::UnselectedNormalize(ref n) => n.fold(accumulator),
+            DomainGoal::WellFormed(..) | DomainGoal::FromEnv(..) => panic!("unexpected where clause"),
             _ => (),
         }
     }
 }
 
 impl WfSolver {
     fn verify_struct_decl(&self, struct_datum: &StructDatum) -> bool {
+        // We retrieve all the input types of the struct fields.
         let mut input_types = Vec::new();
         struct_datum.binders.value.fields.fold(&mut input_types);
         struct_datum.binders.value.where_clauses.fold(&mut input_types);
@@ -124,7 +130,6 @@ impl WfSolver {
         }
 
         let goals = input_types.into_iter().map(|ty| WellFormed::Ty(ty).cast());
-
         let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
                         .expect("at least one goal");
 
@@ -137,6 +142,8 @@ impl WfSolver {
                         .map(|wc| wc.into_from_env_clause())
                         .collect();
 
+        // We ask that the above input types are well-formed provided that all the where-clauses
+        // on the struct definition hold.
         let goal = Goal::Implies(hypotheses, Box::new(goal))
             .quantify(QuantifierKind::ForAll, struct_datum.binders.binders.clone());
 
@@ -152,9 +159,62 @@ impl WfSolver {
             _ => return true
         };
 
+        // We retrieve all the input types of the where clauses appearing on the trait impl,
+        // e.g. in:
+        // ```
+        // impl<T, K> Foo for (Set<K>, Vec<Box<T>>) { ... }
+        // ```
+        // we would retrieve `Set<K>`, `Box<T>`, `Vec<Box<T>>`, `(Set<K>, Vec<Box<T>>)`.
+        // We will have to prove that these types are well-formed.
         let mut input_types = Vec::new();
         impl_datum.binders.value.where_clauses.fold(&mut input_types);
 
+        // We partition the input types of the type on which we implement the trait in two categories:
+        // * projection types, e.g. `<T as Iterator>::Item`: we will have to prove that these types
+        //   are well-formed, e.g. that we can show that `T: Iterator` holds
+        // * any other types, e.g. `HashSet<K>`: we will *assume* that these types are well-formed, e.g.
+        //   we will be able to derive that `K: Hash` holds without writing any where clause.
+        //
+        // Examples:
+        // ```
+        // struct HashSet<K> where K: Hash { ... }
+        //
+        // impl<K> Foo for HashSet<K> {
+        //     // Inside here, we can rely on the fact that `K: Hash` holds
+        // }
+        // ```
+        //
+        // ```
+        // impl<T> Foo for <T as Iterator>::Item {
+        //     // The impl is not well-formed, as an exception we do not assume that
+        //     // `<T as Iterator>::Item` is well-formed and instead want to prove it.
+        // }
+        // ```
+        //
+        // ```
+        // impl<T> Foo for <T as Iterator>::Item where T: Iterator {
+        //     // Now ok.
+        // }
+        // ```
+        let mut header_input_types = Vec::new();
+        trait_ref.fold(&mut header_input_types);
+        let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) =
+            header_input_types.into_iter()
+                              .partition(|ty| ty.is_projection());
+
+        // Associated type values are special because they can be parametric (independently of
+        // the impl), so we issue a special goal which is quantified using the binders of the
+        // associated type value, for example in:
+        // ```
+        // trait Foo {
+        //     type Item<'a>
+        // }
+        //
+        // impl<T> Foo for Box<T> {
+        //     type Item<'a> = Box<&'a T>;
+        // }
+        // ```
+        // we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`.
         let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| {
             let mut input_types = Vec::new();
             assoc_ty.value.value.ty.fold(&mut input_types);
@@ -176,12 +236,8 @@ impl WfSolver {
                       .iter()
                       .filter_map(compute_assoc_ty_goal);
 
-        let mut header_input_types = Vec::new();
-        trait_ref.fold(&mut header_input_types);
-        let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) =
-            header_input_types.into_iter()
-                              .partition(|ty| ty.is_projection());
-
+        // Things to prove well-formed: input types of the where-clauses, projection types
+        // appearing in the header, associated type values, and of course the trait ref.
         let goals =
             input_types.into_iter()
                        .chain(header_projection_types.into_iter())
@@ -191,6 +247,10 @@ impl WfSolver {
 
         let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
                         .expect("at least one goal");
+
+        // Assumptions: types appearing in the header which are not projection types are
+        // assumed to be well-formed, and where clauses declared on the impl are assumed
+        // to hold.
         let hypotheses =
             impl_datum.binders
                       .value

src/solve/test/mod.rs

@@ -14,6 +14,8 @@ fn parse_and_lower_program(text: &str, solver_choice: SolverChoice, skip_coheren
     -> Result<ir::Program>
 {
     if skip_coherence {
+        // We disable WF checks for the recursive solver, because of ambiguities appearing
+        // with projection types.
         chalk_parse::parse_program(text)?.lower_without_coherence()
     } else {
         chalk_parse::parse_program(text)?.lower(solver_choice)
@@ -1527,11 +1529,9 @@ fn coinductive_semantics() {
         } yields {
             "No possible solution"
         }
-
-        // `WellFormed(T)` because of the hand-written impl for `Ptr<T>`.
         goal {
             forall<T> {
-                if (WellFormed(T), T: Send) {
+                if (T: Send) {
                     List<T>: Send
                 }
             }