diff --git a/src/rules/wf.rs b/src/rules/wf.rs index 55f3cedec5a..78678495417 100644 --- a/src/rules/wf.rs +++ b/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(), diff --git a/src/solve/test.rs b/src/solve/test.rs index 8a9e4d7d43e..e806b1d2e35 100644 --- a/src/solve/test.rs +++ b/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! {