From 10de9a9d813184d471388861cc1e0014543525b7 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Tue, 22 May 2018 23:48:54 -0500 Subject: [PATCH] Add failing tests for where clauses --- src/rules/wf.rs | 2 +- src/solve/test.rs | 71 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 72 insertions(+), 1 deletion(-) 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 { } + trait Foo { + type Item where U: Bar; + } + + struct Value { } + struct Sometype { } + impl Foo for Sometype { + type Item = Value; + } + } + + goal { + forall { + exists { + Normalize(>::Item -> V) + } + } + } yields { + "No possible solution" + } + + goal { + forall { + exists { + if (U: Bar) { + Normalize(>::Item -> V) + } + } + } + } yields { + "Unique; substitution [?0 := Value]" + } + } +} + +#[test] +fn normalize_gat_with_higher_ranked_trait_bound() { + test! { + program { + trait Foo<'a, T> { } + struct i32 { } + + trait Bar<'a, T> { + type Item: 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 = i32; + } + } + + goal { + forall<'a, T, V> { + if (forall<'b> { V: Foo<'b, T> }) { + exists { + Normalize(>::Item -> U) + } + } + } + } yields { + "Unique; substitution [?0 := i32], lifetime constraints []" + } + } +} + #[test] fn normalize_implied_bound() { test! {