Correctly instantiate where clauses / bounds on GATs in wf.rs

Author: scalexm

src/fold.rs

@@ -431,6 +431,7 @@ enum_fold!(Constraint[] { LifetimeEq(a, b) });
 enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g),
                     Leaf(wc), CannotProve(a) });
 enum_fold!(ProgramClause[] { Implies(a), ForAll(a) });
+enum_fold!(InlineBound[] { TraitBound(a), ProjectionEqBound(a) });
 
 macro_rules! struct_fold {
     ($s:ident $([$($tt_args:tt)*])? { $($name:ident),* $(,)* } $($w:tt)*) => {
@@ -582,4 +583,16 @@ struct_fold!(ConstrainedSubst {
     constraints,
 });
 
+struct_fold!(TraitBound {
+    trait_id,
+    args_no_self,
+});
+
+struct_fold!(ProjectionEqBound {
+    trait_bound,
+    associated_ty_id,
+    parameters,
+    value,
+});
+
 // struct_fold!(ApplicationTy { name, parameters }); -- intentionally omitted, folded through Ty

src/ir.rs

@@ -687,7 +687,9 @@ impl DomainGoal {
     /// Same as `into_well_formed_goal` but with the `FromEnv` predicate instead of `WellFormed`.
     crate fn into_from_env_goal(self) -> DomainGoal {
         match self {
-            DomainGoal::Holds(wca) => DomainGoal::FromEnv(wca),
+            DomainGoal::Holds(wca @ WhereClauseAtom::Implemented(..)) => {
+                DomainGoal::FromEnv(wca)
+            }
             goal => goal,
         }
     }

src/ir/lowering/test.rs

@@ -378,3 +378,31 @@ fn duplicate_parameters() {
         }
     }
 }
+
+#[test]
+fn external_items() {
+    lowering_success! {
+        program {
+            extern trait Send { }
+            extern struct Vec<T> { }
+        }
+    }
+}
+
+#[test]
+fn deref_trait() {
+    lowering_success! {
+        program {
+            #[lang_deref] trait Deref { type Target; }
+        }
+    }
+
+    lowering_error! {
+        program {
+            #[lang_deref] trait Deref { }
+            #[lang_deref] trait DerefDupe { }
+        } error_msg {
+            "Duplicate lang item `DerefTrait`"
+        }
+    }
+}

src/rules.rs

@@ -520,11 +520,12 @@ impl ir::AssociatedTyDatum {
         //
         // This is really a family of clauses, one for each where clause.
         clauses.extend(self.where_clauses.iter().map(|wc| {
+            let shift = wc.binders.len();
             ir::Binders {
-                binders: binders.iter().chain(wc.binders.iter()).cloned().collect(),
+                binders: wc.binders.iter().chain(binders.iter()).cloned().collect(),
                 value: ir::ProgramClauseImplication {
                     consequence: wc.value.clone().into_from_env_goal(),
-                    conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).cast()],
+                    conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).up_shift(shift).cast()],
                 }
             }.cast()
         }));

src/rules/wf.rs

@@ -5,6 +5,8 @@ use errors::*;
 use cast::*;
 use solve::SolverChoice;
 use itertools::Itertools;
+use fold::*;
+use fold::shift::Shift;
 
 mod test;
 
@@ -207,38 +209,20 @@ impl WfSolver {
         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.
+        // We retrieve all the input types of the type on which we implement the trait: 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:
+        // Example:
         // ```
         // 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
@@ -257,49 +241,48 @@ impl WfSolver {
             let assoc_ty_datum = &self.env.associated_ty_data[&assoc_ty.associated_ty_id];
             let bounds = &assoc_ty_datum.bounds;
 
-            let trait_datum = &self.env.trait_data[&assoc_ty_datum.trait_id];
-
             let mut input_types = Vec::new();
             assoc_ty.value.value.ty.fold(&mut input_types);
 
-            let goals = input_types.into_iter()
-                                   .map(|ty| DomainGoal::WellFormedTy(ty).cast());
-                                   //.chain(bounds.iter()
-                                   //             .flat_map(|b| b.clone()
-                                   //                            .lower_with_self(assoc_ty.value.value.ty.clone()))
-                                   //             .map(|g| g.into_well_formed_goal().cast()));
-            let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
-                            //.expect("at least one goal");
-            let goal = goal //Goal::Implies(hypotheses, Box::new(goal))
-                .map(|goal| goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()));//binders);
-
-            // FIXME this is wrong (and test)!
-            let mut bound_binders = assoc_ty.value.binders.clone();
-            bound_binders.extend(trait_datum.binders.binders.iter());
+            let wf_goals =
+                input_types.into_iter()
+                           .map(|ty| DomainGoal::WellFormedTy(ty));
+            
+            let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len());
+
+            let all_parameters: Vec<_> =
+                assoc_ty.value.binders.iter()
+                                      .zip(0..)
+                                      .map(|p| p.to_parameter())
+                                      .chain(trait_ref.parameters.iter().cloned())
+                                      .collect();
+            
+            let bound_goals =
+                bounds.iter()
+                      .map(|b| Subst::apply(&all_parameters, b))
+                      .flat_map(|b| b.lower_with_self(assoc_ty.value.value.ty.clone()))
+                      .map(|g| g.into_well_formed_goal());
+            
+            let goals = wf_goals.chain(bound_goals).casted();
+            let goal = match goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) {
+                Some(goal) => goal,
+                None => return None,
+            };
 
             let hypotheses =
                 assoc_ty_datum.where_clauses
                               .iter()
-                              .chain(impl_datum.binders.value.where_clauses.iter())  // FIXME binders (and test)!
-                              .cloned()
+                              .map(|wc| Subst::apply(&all_parameters, wc))
                               .map(|wc| wc.map(|bound| bound.into_from_env_goal()))
                               .casted()
                               .collect();
-            let bound_goal = bounds.iter()
-                                   .flat_map(|b| b.clone()
-                                   .lower_with_self(assoc_ty.value.value.ty.clone()))
-                                   .map(|g| g.into_well_formed_goal().cast())
-                                   .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
-            let bound_goal = bound_goal.map(|g| {
-                Goal::Implies(hypotheses, Box::new(g)).quantify(QuantifierKind::ForAll, bound_binders)
-            });
-
-            let goal = goal.into_iter()
-                           .chain(bound_goal.into_iter())
-                           .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
-            println!("{:?}", goal);
-
-            goal
+            
+            let goal = Goal::Implies(
+                hypotheses,
+                Box::new(goal)
+            );
+
+            Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()))
         };
 
         let assoc_ty_goals =
@@ -316,7 +299,6 @@ impl WfSolver {
         );
         let goals =
             input_types.into_iter()
-                       .chain(header_projection_types.into_iter())
                        .map(|ty| DomainGoal::WellFormedTy(ty).cast())
                        .chain(assoc_ty_goals)
                        .chain(Some(trait_ref_wf).cast());
@@ -335,12 +317,14 @@ impl WfSolver {
                       .cloned()
                       .map(|wc| wc.map(|bound| bound.into_from_env_goal()))
                       .casted()
-                      .chain(header_other_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast()))
+                      .chain(header_input_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast()))
                       .collect();
 
         let goal = Goal::Implies(hypotheses, Box::new(goal))
             .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone());
 
+        println!("{:?}", goal);
+
         match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() {
             Some(sol) => sol.is_unique(),
             None => false,

src/rules/wf/test.rs

@@ -438,16 +438,6 @@ fn generic_projection_bound() {
     }
 }
 
-#[test]
-fn external_items() {
-    lowering_success! {
-        program {
-            extern trait Send { }
-            extern struct Vec<T> { }
-        }
-    }
-}
-
 #[test]
 fn higher_ranked_trait_bounds() {
     lowering_error! {
@@ -474,6 +464,24 @@ fn higher_ranked_trait_bounds() {
     }
 }
 
+#[test]
+fn higher_ranked_trait_bound_on_gat() {
+    lowering_success! {
+        program {
+            trait Foo<'a> { }
+            struct i32 { }
+
+            trait Bar<'a> {
+                type Item<V>: Foo<'a> where forall<'b> V: Foo<'b>;
+            }
+
+            impl<'a> Bar<'a> for i32 {
+                type Item<V> = V;
+            }
+        }
+    }
+}
+
 // See `cyclic_traits`, this is essentially the same but with higher-ranked co-inductive WF goals.
 #[test]
 fn higher_ranked_cyclic_requirements() {
@@ -511,21 +519,3 @@ fn higher_ranked_cyclic_requirements() {
         }
     }
 }
-
-#[test]
-fn deref_trait() {
-    lowering_success! {
-        program {
-            #[lang_deref] trait Deref { type Target; }
-        }
-    }
-
-    lowering_error! {
-        program {
-            #[lang_deref] trait Deref { }
-            #[lang_deref] trait DerefDupe { }
-        } error_msg {
-            "Duplicate lang item `DerefTrait`"
-        }
-    }
-}