Add more comments

src/ir/mod.rs

@@ -753,16 +753,11 @@ 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
+    crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool {
         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

@@ -1387,8 +1387,7 @@ impl ir::AssociatedTyDatum {
         // particular, whenever normalization is possible, we cannot
         // solve that projection uniquely, since we can now elaborate
         // `ProjectionEq` to fallback *or* normalize it. So instead we
-        // handle this kind of reasoning by expanding "projection
-        // equality" predicates (see `DomainGoal::expanded`).
+        // handle this kind of reasoning through the `FromEnv` predicate.
         //
         // We also generate rules specific to WF requirements and implied bounds,
         // see below.

src/lower/test.rs

@@ -32,9 +32,9 @@ 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())
+    // FIXME: Use the SLG solver to avoid ambiguities on projection types encountered
+    // when using the recursive solver.
+    chalk_parse::parse_program(text)?.lower(SolverChoice::slg())
 }
 
 fn parse_and_lower_goal(program: &Program, text: &str) -> Result<Box<Goal>> {
@@ -575,7 +575,6 @@ fn ill_formed_trait_decl() {
         }
     }
 }
-
 #[test]
 fn cyclic_traits() {
     lowering_success! {
@@ -587,23 +586,34 @@ fn cyclic_traits() {
             impl<T> A for T { }
         }
     }
-}
 
-#[test]
-fn cyclic_traits_error() {
     lowering_error! {
         program {
             trait Copy { }
 
             trait A where Self: B, Self: Copy {}
             trait B where Self: A { }
 
+            // This impl won't be able to prove that `T: Copy` holds.
             impl<T> B for T {}
+
             impl<T> A for T where T: B {}
         } error_msg {
             "trait impl for \"B\" does not meet well-formedness requirements"
         }
     }
+
+    lowering_success! {
+        program {
+            trait Copy { }
+
+            trait A where Self: B, Self: Copy {}
+            trait B where Self: A { }
+
+            impl<T> B for T where T: Copy {}
+            impl<T> A for T where T: B {}
+        }
+    }
 }
 
 #[test]
@@ -636,6 +646,7 @@ fn ill_formed_assoc_ty() {
             }
 
             impl Bar for i32 {
+                // `OnlyFoo<i32>` is ill-formed because `i32: Foo` does not hold.
                 type Value = OnlyFoo<i32>;
             }
         } error_msg {
@@ -660,6 +671,7 @@ fn implied_bounds() {
             }
 
             impl<K> Foo for Set<K> {
+                // Here, `WF(Set<K>)` implies `K: Hash` and hence `OnlyEq<K>` is WF.
                 type Value = OnlyEq<K>;
             }
         }
@@ -710,6 +722,8 @@ fn wf_requiremements_for_projection() {
             }
 
             impl<T> Foo for T {
+                // The projection is well-formed if `T: Iterator` holds, which cannot
+                // be proved here.
                 type Value = <T as Iterator>::Item;
             }
         } error_msg {
@@ -744,6 +758,8 @@ fn projection_type_in_header() {
 
             trait Bar { }
 
+            // Projection types in an impl header are not assumed to be well-formed,
+            // an explicit where clause is needed (see below).
             impl<T> Bar for <T as Foo>::Value { }
         } error_msg {
             "trait impl for \"Bar\" does not meet well-formedness requirements"

src/lower/wf.rs

@@ -13,7 +13,7 @@ struct WfSolver {
 
 impl Program {
     pub fn verify_well_formedness(&self, solver_choice: SolverChoice) -> Result<()> {
-        set_current_program(&Arc::new(self.clone()), || self.solve_wf_requirements(solver_choice))
+        tls::set_current_program(&Arc::new(self.clone()), || self.solve_wf_requirements(solver_choice))
     }
 
     fn solve_wf_requirements(&self, solver_choice: SolverChoice) -> Result<()> {
@@ -79,9 +79,15 @@ impl FoldInputTypes for Ty {
                 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(..) => (),
+            // Type parameters do not carry any input types (so we can sort of assume they are
+            // always WF).
+            Ty::Var(..) => (),
+
+            // Higher-kinded types such as `for<'a> fn(&'a u32)` introduce their own implied
+            // bounds, and these bounds will be enforced upon calling such a function. In some
+            // sense, well-formedness requirements for the input types of an HKT will be enforced
+            // lazily, so no need to include them here.
+            Ty::ForAll(..) => (),
         }
     }
 }
@@ -244,7 +250,7 @@ impl WfSolver {
                        .map(|ty| WellFormed::Ty(ty).cast())
                        .chain(assoc_ty_goals)
                        .chain(Some(WellFormed::TraitRef(trait_ref.clone())).cast());
-        
+
         let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
                         .expect("at least one goal");
 

src/solve/test/mod.rs

@@ -14,7 +14,7 @@ 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
+        // FIXME: We disable WF checks for the recursive solver, because of ambiguities appearing
         // with projection types.
         chalk_parse::parse_program(text)?.lower_without_coherence()
     } else {