Add failing tests for where clauses

src/rules/wf.rs

@@ -325,7 +325,7 @@ impl WfSolver {
  let goal = Goal::Implies(hypotheses, Box::new(goal))
  .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone());
 
- println!("{:?}", goal);
+ debug!("WF trait goal: {:?}", goal);
 
  match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() {
  Some(sol) => sol.is_unique(),

src/solve/test.rs

@@ -669,6 +669,77 @@ fn normalize_gat_with_where_clause() {
  }
 }
 
+#[test]
+fn normalize_gat_with_where_clause2() {
+ test! {
+ program {
+ trait Bar<T> { }
+ trait Foo<T> {
+ type Item<U> where U: Bar<T>;
+ }
+
+ struct Value<T> { }
+ struct Sometype { }
+ impl<T> Foo<T> for Sometype {
+ type Item<U> = Value<U>;
+ }
+ }
+
+ goal {
+ forall<T, U> {
+ exists<V> {
+ Normalize(<Sometype as Foo<T>>::Item<U> -> V)
+ }
+ }
+ } yields {
+ "No possible solution"
+ }
+
+ goal {
+ forall<T, U> {
+ exists<V> {
+ if (U: Bar<T>) {
+ Normalize(<Sometype as Foo<T>>::Item<U> -> V)
+ }
+ }
+ }
+ } yields {
+ "Unique; substitution [?0 := Value<!2>]"
+ }
+ }
+}
+
+#[test]
+fn normalize_gat_with_higher_ranked_trait_bound() {
+ test! {
+ program {
+ trait Foo<'a, T> { }
+ struct i32 { }
+
+ trait Bar<'a, T> {
+ type Item<V>: Foo<'a, T> where V: Foo<'a, T>;
+ }
+
+ impl<'a, T> Foo<'a, T> for i32 { }
+ impl<'a, T> Bar<'a, T> for i32 {
+ type Item<V> = i32;
+ }
+ }
+
+ goal {
+ forall<'a, T, V> {
+ if (forall<'b> { V: Foo<'b, T> }) {
+ exists<U> {
+ Normalize(<i32 as Bar<'a, T>>::Item<V> -> U)
+ }
+ }
+ }
+ } yields {
+ "Unique; substitution [?0 := i32], lifetime constraints []"
+ }
+ }
+}
+
 #[test]
 fn normalize_implied_bound() {
  test! {