Add failing tests for where clauses

Author: tmandry

src/rules/wf.rs

@@ -323,7 +323,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! {