From f3302f526b96f363c14fef6baa8fb7dceedf9453 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 1215aa08fab..397084cef4d 100644 --- a/src/rules/wf.rs +++ b/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(), diff --git a/src/solve/test.rs b/src/solve/test.rs index 86aaf5c2008..eb52de1781b 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! {