From 77246f30259696e5787f78f69b2bbc3899adaee3 Mon Sep 17 00:00:00 2001 From: Aaron Turon Date: Mon, 5 Jun 2017 11:38:18 -0700 Subject: [PATCH] Clarify treatment of unification ambiguity and overhaul treatment of normalization fallback. --- src/bin/repl.rs | 9 ++-- src/fold/mod.rs | 2 +- src/ir/debug.rs | 1 - src/ir/mod.rs | 17 +++--- src/lower/mod.rs | 77 ++++++++------------------- src/solve/fulfill.rs | 15 ++++-- src/solve/infer/mod.rs | 2 +- src/solve/infer/unify.rs | 15 ++++-- src/solve/mod.rs | 37 ++++++++++++- src/solve/solver.rs | 111 ++++++++++++++++++++++++++++++--------- src/solve/test.rs | 67 ++++++++++++++++++----- src/zip.rs | 2 +- 12 files changed, 237 insertions(+), 118 deletions(-) diff --git a/src/bin/repl.rs b/src/bin/repl.rs index cb216aafeb6..6b4dde10fa6 100644 --- a/src/bin/repl.rs +++ b/src/bin/repl.rs @@ -86,7 +86,7 @@ fn process(command: &str, rl: &mut rustyline::Editor<()>, prog: &mut Option Result<()> { match command { "print" => println!("{}", prog.text), - "lowered" => println!("{:?}", prog.ir), + "lowered" => println!("{:#?}", prog.env), _ => goal(command, prog)?, } Ok(()) @@ -120,11 +120,8 @@ fn goal(text: &str, prog: &Program) -> Result<()> { let goal = chalk_parse::parse_goal(text)?.lower(&*prog.ir)?; let overflow_depth = 10; let mut solver = Solver::new(&prog.env, overflow_depth); - let goal = ir::Canonical { - value: ir::InEnvironment::new(&ir::Environment::new(), *goal), - binders: vec![], - }; - match solver.solve_goal(goal) { + let goal = ir::InEnvironment::new(&ir::Environment::new(), *goal); + match solver.solve_closed_goal(goal) { Ok(v) => println!("{}\n", v), Err(e) => println!("No possible solution: {}\n", e), } diff --git a/src/fold/mod.rs b/src/fold/mod.rs index 5e03c3b4007..f37d083eae5 100644 --- a/src/fold/mod.rs +++ b/src/fold/mod.rs @@ -196,7 +196,7 @@ macro_rules! enum_fold { } enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold); -enum_fold!(DomainGoal[] { Implemented(a), RawNormalize(a), Normalize(a), WellFormed(a) }); +enum_fold!(DomainGoal[] { Implemented(a), Normalize(a), WellFormed(a) }); enum_fold!(WellFormed[] { Ty(a), TraitRef(a) }); enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) }); enum_fold!(Constraint[] { LifetimeEq(a, b) }); diff --git a/src/ir/debug.rs b/src/ir/debug.rs index 937d8e4aff8..48244f7b4fb 100644 --- a/src/ir/debug.rs +++ b/src/ir/debug.rs @@ -149,7 +149,6 @@ impl Debug for DomainGoal { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { match *self { DomainGoal::Normalize(ref n) => write!(fmt, "{:?}", n), - DomainGoal::RawNormalize(ref n) => write!(fmt, "raw {{ {:?} }}", n), DomainGoal::Implemented(ref n) => { write!(fmt, "{:?}: {:?}{:?}", diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 0a568142ec7..afc74d09c71 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -129,8 +129,8 @@ impl Environment { push_clause(where_clause); } } - DomainGoal::RawNormalize(Normalize { ref projection, ty: _ }) => { - // raw { >::Foo ===> V } + DomainGoal::Normalize(Normalize { ref projection, ty: _ }) => { + // >::Foo ===> V // ---------------------------------------------------------- // T: Trait @@ -396,9 +396,6 @@ pub struct TraitRef { #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] pub enum DomainGoal { Implemented(TraitRef), - /// A projection we know definitively via an impl or where clause - RawNormalize(Normalize), - /// A general projection, which might employ fallback Normalize(Normalize), WellFormed(WellFormed), } @@ -414,7 +411,8 @@ impl DomainGoal { conditions: vec![], }, binders: vec![], - } + }, + fallback_clause: false, } } } @@ -478,6 +476,9 @@ impl Binders { #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct ProgramClause { pub implication: Binders, + + /// Is this a fallback clause which should get lower priority? + pub fallback_clause: bool, } /// Represents one clause of the form `consequence :- conditions`. @@ -592,6 +593,10 @@ impl Substitution { Substitution { tys, lifetimes } } + + pub fn is_empty(&self) -> bool { + self.tys.is_empty() && self.lifetimes.is_empty() + } } #[derive(Clone, Debug, PartialEq, Eq)] diff --git a/src/lower/mod.rs b/src/lower/mod.rs index ab910b0498d..0854d264d34 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -381,10 +381,7 @@ impl LowerWhereClause for WhereClause { ir::DomainGoal::Implemented(trait_ref.lower(env)?) } WhereClause::ProjectionEq { ref projection, ref ty } => { - // NB: here we generate a RawNormalize, because we want to make - // make a maximally-strong assumption (and not allow fallback to - // trigger). - ir::DomainGoal::RawNormalize(ir::Normalize { + ir::DomainGoal::Normalize(ir::Normalize { projection: projection.lower(env)?, ty: ty.lower(env)?, }) @@ -406,18 +403,11 @@ impl LowerWhereClause for WhereClause { impl LowerWhereClause for WhereClause { fn lower(&self, env: &Env) -> Result { Ok(match *self { - WhereClause::Implemented { .. } => { + WhereClause::Implemented { .. } | + WhereClause::ProjectionEq { .. } => { let g: ir::DomainGoal = self.lower(env)?; g.cast() } - WhereClause::ProjectionEq { ref projection, ref ty } => { - // NB: here we generate a full Normalize clause, allowing for - // fallback to trigger when we're trying to *prove* a goal - ir::DomainGoal::Normalize(ir::Normalize { - projection: projection.lower(env)?, - ty: ty.lower(env)?, - }).cast() - } WhereClause::TyWellFormed { ref ty } => { ir::WellFormed::Ty(ty.lower(env)?).cast() } @@ -806,7 +796,8 @@ impl ir::ImplDatum { consequence: bound.trait_ref.clone().cast(), conditions: bound.where_clauses.clone().cast(), } - }) + }), + fallback_clause: false, } } } @@ -824,7 +815,7 @@ impl ir::AssociatedTyValue { /// /// ```notrust /// forall<'a, T> { - /// (Vec: Iterable =raw Iter<'a, T>>) :- + /// (Vec: Iterable = Iter<'a, T>>) :- /// (Vec: Iterable), // (1) /// (T: 'a) // (2) /// } @@ -868,13 +859,14 @@ impl ir::AssociatedTyValue { implication: ir::Binders { binders: all_binders.clone(), value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::RawNormalize(ir::Normalize { + consequence: ir::DomainGoal::Normalize(ir::Normalize { projection: projection.clone(), ty: self.value.value.ty.clone() }), conditions: conditions.clone(), } - } + }, + fallback_clause: false, }; vec![normalization] @@ -932,7 +924,8 @@ impl ir::StructDatum { .map(|wc| wc.cast()) .collect(), } - }) + }), + fallback_clause: false, }; vec![wf] @@ -972,7 +965,8 @@ impl ir::TraitDatum { tys.chain(where_clauses).collect() } } - }) + }), + fallback_clause: false, }; vec![wf] @@ -981,8 +975,9 @@ impl ir::TraitDatum { impl ir::AssociatedTyDatum { fn to_program_clauses(&self) -> Vec { - // For each associated type, we define normalization including a - // "fallback" if we can't resolve a projection using an impl/where clauses. + // For each associated type, we define a normalization "fallback" for + // projecting when we don't have constraints to say anything interesting + // about an associated type. // // Given: // @@ -992,8 +987,7 @@ impl ir::AssociatedTyDatum { // // we generate: // - // ?T: Foo :- ?T: Foo. - // ?T: Foo> :- not { exists { ?T: Foo } }. + // ::Assoc ==> (Foo::Assoc). let binders: Vec<_> = self.parameter_kinds.iter().map(|pk| pk.map(|_| ())).collect(); let parameters: Vec<_> = binders.iter().zip(0..).map(|p| p.to_parameter()).collect(); @@ -1002,52 +996,25 @@ impl ir::AssociatedTyDatum { parameters: parameters.clone(), }; - let raw = { - let binders: Vec<_> = binders.iter() - .cloned() - .chain(Some(ir::ParameterKind::Ty(()))) - .collect(); - let ty = ir::Ty::Var(binders.len() - 1); - let normalize = ir::Normalize { projection: projection.clone(), ty }; - - ir::ProgramClause { - implication: ir::Binders { - binders, - value: ir::ProgramClauseImplication { - consequence: normalize.clone().cast(), - conditions: vec![ir::DomainGoal::RawNormalize(normalize).cast()], - } - } - } - }; - let fallback = { // Construct an application from the projection. So if we have `::Item`, // we would produce `(Iterator::Item)`. let app = ir::ApplicationTy { name: ir::TypeName::AssociatedType(self.id), parameters }; let ty = ir::Ty::Apply(app); - let raw = ir::DomainGoal::RawNormalize(ir::Normalize { - projection: projection.clone().up_shift(1), - ty: ir::Ty::Var(0), - }); - let exists_binders = ir::Binders { - binders: vec![ir::ParameterKind::Ty(())], - value: Box::new(raw.cast()), - }; - let exists = ir::Goal::Quantified(ir::QuantifierKind::Exists, exists_binders); - ir::ProgramClause { implication: ir::Binders { binders, value: ir::ProgramClauseImplication { consequence: ir::Normalize { projection: projection.clone(), ty }.cast(), - conditions: vec![ir::Goal::Not(Box::new(exists))] + // TODO: should probably include the TraitRef here + conditions: vec![], } - } + }, + fallback_clause: true, } }; - vec![raw, fallback] + vec![fallback] } } diff --git a/src/solve/fulfill.rs b/src/solve/fulfill.rs index 98e00533e3e..f8adb8faa58 100644 --- a/src/solve/fulfill.rs +++ b/src/solve/fulfill.rs @@ -23,6 +23,10 @@ impl Outcome { } } +pub struct UnifyOutcome { + pub ambiguous: bool, +} + /// A goal that must be resolved #[derive(Clone, Debug, PartialEq, Eq)] enum Obligation { @@ -115,7 +119,7 @@ impl<'s> Fulfill<'s> { /// /// Wraps `InferenceTable::unify`; any resulting normalizations are added /// into our list of pending obligations with the given environment. - pub fn unify(&mut self, environment: &Arc, a: &T, b: &T) -> Result<()> + pub fn unify(&mut self, environment: &Arc, a: &T, b: &T) -> Result where T: ?Sized + Zip + Debug { let UnificationResult { goals, constraints, ambiguous } = @@ -127,7 +131,7 @@ impl<'s> Fulfill<'s> { self.constraints.extend(constraints); self.obligations.extend(goals.into_iter().map(Obligation::Prove)); self.ambiguous = self.ambiguous || ambiguous; - Ok(()) + Ok(UnifyOutcome { ambiguous }) } /// Create obligations for the given goal in the given environment. This may @@ -173,7 +177,8 @@ impl<'s> Fulfill<'s> { self.push_goal(environment, *subgoal2); } Goal::Not(subgoal) => { - self.obligations.push(Obligation::Refute(InEnvironment::new(environment, *subgoal))); + let in_env = InEnvironment::new(environment, *subgoal); + self.obligations.push(Obligation::Refute(in_env)); } Goal::Leaf(wc) => { self.obligations.push(Obligation::Prove(InEnvironment::new(environment, wc))); @@ -218,7 +223,7 @@ impl<'s> Fulfill<'s> { } // Negate the result - if let Ok(solution) = self.solver.solve_goal(canonicalized.quantified) { + if let Ok(solution) = self.solver.solve_closed_goal(canonicalized.quantified.value) { match solution { Solution::Unique(_) => Err("refutation failed")?, Solution::Ambig(_) => Ok(NegativeSolution::Ambiguous), @@ -355,7 +360,7 @@ impl<'s> Fulfill<'s> { // need to determine how to package up what we learned about type // inference as an ambiguous solution. - if subst.is_trivial(&mut self.infer) { + if subst.is_trivial_within(&mut self.infer) { // In this case, we didn't learn *anything* definitively. So now, we // go one last time through the positive obligations, this time // applying even *tentative* inference suggestions, so that we can diff --git a/src/solve/infer/mod.rs b/src/solve/infer/mod.rs index d78a56b96cd..73958204111 100644 --- a/src/solve/infer/mod.rs +++ b/src/solve/infer/mod.rs @@ -159,7 +159,7 @@ impl Lifetime { impl Substitution { /// Check whether this substitution is the identity substitution in the /// given inference context. - pub fn is_trivial(&self, in_infer: &mut InferenceTable) -> bool { + pub fn is_trivial_within(&self, in_infer: &mut InferenceTable) -> bool { for ty in self.tys.values() { if let Some(var) = ty.inference_var() { if in_infer.probe_var(var).is_some() { diff --git a/src/solve/infer/unify.rs b/src/solve/infer/unify.rs index efdee4d5062..f3a5a7f5f31 100644 --- a/src/solve/infer/unify.rs +++ b/src/solve/infer/unify.rs @@ -43,8 +43,9 @@ pub struct UnificationResult { pub constraints: Vec>, /// When unifying two skolemized (forall-quantified) type names, we can - /// neither confirm nor deny their equality, so we return an ambiguous - /// result. + /// neither confirm nor deny their equality, since we interpret the + /// unification request as talking about *all possible + /// substitutions*. Instead, we return an ambiguous result. pub ambiguous: bool, } @@ -115,8 +116,16 @@ impl<'t> Unifier<'t> { (&Ty::Apply(ref apply1), &Ty::Apply(ref apply2)) => { if apply1.name != apply2.name { if apply1.name.is_for_all() || apply2.name.is_for_all() { + // we're being asked to prove something like `!0 = !1` + // or `!0 = i32`. We interpret this as being asked + // whether that holds *for all subtitutions*. Thus, the + // answer is always *maybe* (ambiguous). That means we get: + // + // forall { T = U } // Ambig + // forall { not { T = U } } // Ambig + self.ambiguous = true; - return Ok(()); + return Ok(()) } else { bail!("cannot equate `{:?}` and `{:?}`", apply1.name, apply2.name); } diff --git a/src/solve/mod.rs b/src/solve/mod.rs index fa09d45642b..a0d33fdd4cc 100644 --- a/src/solve/mod.rs +++ b/src/solve/mod.rs @@ -66,8 +66,10 @@ impl Solution { use self::Guidance::*; if self == other { return self } + if self.is_empty_unique() { return self } + if other.is_empty_unique() { return other } - // unless we have two matching Unique solutions, we always downgrade to Ambig: + // Otherwise, always downgrade to Ambig: let guidance = match (self.into_guidance(), other.into_guidance()) { (Definite(ref subst1), Definite(ref subst2)) if subst1 == subst2 => @@ -91,8 +93,10 @@ impl Solution { use self::Guidance::*; if self == other { return self } + if self.is_empty_unique() { return self } + if other.is_empty_unique() { return other } - // unless we have two matching Unique solutions, we always downgrade to Ambig: + // Otherwise, always downgrade to Ambig: let guidance = match (self.into_guidance(), other.into_guidance()) { (Definite(subst), _) | (Suggested(subst), _) => Suggested(subst), @@ -101,6 +105,24 @@ impl Solution { Solution::Ambig(guidance) } + /// Implements Prolog-style failure: if we see no hope of reaching a + /// definite solution from `self` -- even if there might in principle be one + /// -- and there *is* an option by falling back to `other`, we go with + /// `other`. + pub fn fallback_to(self, other: Solution) -> Solution { + use self::Guidance::*; + + if self == other { return self } + if let Solution::Ambig(guidance) = self { + match guidance { + Definite(subst) | Suggested(subst) => Solution::Ambig(Suggested(subst)), + Unknown => other, + } + } else { + self + } + } + /// View this solution purely in terms of type inference guidance fn into_guidance(self) -> Guidance { match self { @@ -146,6 +168,17 @@ impl Solution { _ => false, } } + + /// We use emptiness, rather than triviality, to deduce that alternative + /// solutions **cannot meaningfully differ** + pub fn is_empty_unique(&self) -> bool { + match *self { + Solution::Unique(ref subst) => { + subst.binders.is_empty() && subst.value.subst.is_empty() + } + _ => false, + } + } } impl fmt::Display for Solution { diff --git a/src/solve/solver.rs b/src/solve/solver.rs index f1044a9e2a5..210a79615e3 100644 --- a/src/solve/solver.rs +++ b/src/solve/solver.rs @@ -16,6 +16,24 @@ pub struct Solver { stack: Vec, } +/// An extension trait for merging `Result`s +trait MergeWith { + fn merge_with(self, other: Self, f: F) -> Self where F: FnOnce(T, T) -> T; +} + +impl MergeWith for Result { + fn merge_with(self: Result, other: Result, f: F) -> Result + where F: FnOnce(T, T) -> T + { + match (self, other) { + (Err(_), Ok(v)) | + (Ok(v), Err(_)) => Ok(v), + (Ok(v1), Ok(v2)) => Ok(f(v1, v2)), + (Err(_), Err(e)) => Err(e) + } + } +} + impl Solver { pub fn new(program: &Arc, overflow_depth: usize) -> Self { Solver { @@ -25,9 +43,9 @@ impl Solver { } } - /// Attempt to solve a *closed*, canonicalized goal. The substitution - /// returned in the solution will be for the fully decomposed goal. For - /// example, given the program + /// Attempt to solve a *closed* goal. The substitution returned in the + /// solution will be for the fully decomposed goal. For example, given the + /// program /// /// ```ignore /// struct u8 { } @@ -39,11 +57,9 @@ impl Solver { /// and the goal `exists { forall { SomeType: Foo } }`, a unique /// solution is produced with substitution `?0 := u8`. The `?0` is drawn /// from the number of the instantiated existential. - pub fn solve_goal(&mut self, goal: Canonical>) -> Result { + pub fn solve_closed_goal(&mut self, goal: InEnvironment) -> Result { let mut fulfill = Fulfill::new(self); - let Canonical { value, binders } = goal; - let InEnvironment { environment, goal } = fulfill.instantiate(binders, &value); - fulfill.push_goal(&environment, goal); + fulfill.push_goal(&goal.environment, goal.goal); // We use this somewhat hacky approach to get our hands on the // instantiated variables after pushing our initial goal. This @@ -92,19 +108,30 @@ impl Solver { // "Domain" goals (i.e., leaf goals that are Rust-specific) are // always solved via some form of implication. We can either // apply assumptions from our environment (i.e. where clauses), - // or from the lowered program. We try each approach in turn: + // or from the lowered program, which includes fallback + // clauses. We try each approach in turn: let env_clauses = value .environment .elaborated_clauses(&self.program) .map(DomainGoal::into_program_clause); - let env_solution = self.solve_from_clauses(&binders, &value, env_clauses); + let env_solution = self.solve_from_clauses(&binders, &value, env_clauses, true); + + let prog_clauses: Vec<_> = self.program.program_clauses.iter() + .cloned() + .filter(|clause| !clause.fallback_clause) + .collect(); + let prog_solution = self.solve_from_clauses(&binders, &value, prog_clauses, false); - let prog_clauses = self.program.program_clauses.clone(); - let prog_solution = - self.solve_from_clauses(&binders, &value, prog_clauses.into_iter()); + // These fallback clauses are used when we're sure we'll never + // reach Unique via another route + let fallback: Vec<_> = self.program.program_clauses.iter() + .cloned() + .filter(|clause| clause.fallback_clause) + .collect(); + let fallback_solution = self.solve_from_clauses(&binders, &value, fallback, false); - // Now that we have both outcomes, we attempt to combine + // Now that we have all the outcomes, we attempt to combine // them. Here, we apply a heuristic (also found in rustc): if we // have possible solutions via both the environment *and* the // program, we favor the environment; this only impacts type @@ -112,12 +139,9 @@ impl Solver { // made in a given context are more likely to be relevant than // general `impl`s. - match (env_solution, prog_solution) { - (Err(_), Ok(solution)) | - (Ok(solution), Err(_)) => Ok(solution), - (Ok(env), Ok(prog)) => Ok(env.favor_over(prog)), - (Err(_), Err(e)) => Err(e) - } + env_solution + .merge_with(prog_solution, |env, prog| env.favor_over(prog)) + .merge_with(fallback_solution, |merged, fallback| merged.fallback_to(fallback)) } }; @@ -149,15 +173,17 @@ impl Solver { binders: &[ParameterKind], goal: &InEnvironment, clauses: C, + from_env: bool, ) -> Result where - C: Iterator, + C: IntoIterator, { let mut cur_solution = None; - for ProgramClause { implication } in clauses { + for ProgramClause { implication, .. } in clauses { debug_heading!("clause={:?}", implication); - if let Ok(solution) = self.solve_via_implication(binders, goal.clone(), implication) { + let res = self.solve_via_implication(binders, goal.clone(), implication, from_env); + if let Ok(solution) = res { debug!("ok: solution={:?}", solution); cur_solution = Some( match cur_solution { @@ -178,19 +204,54 @@ impl Solver { binders: &[ParameterKind], goal: InEnvironment, clause: Binders, + from_env: bool, ) -> Result { let mut fulfill = Fulfill::new(self); let subst = Substitution::from_binders(&binders); let (goal, (clause, subst)) = fulfill.instantiate(binders.iter().cloned(), &(goal, (clause, subst))); - let implication = + let ProgramClauseImplication { consequence, conditions} = fulfill.instantiate_in(goal.environment.universe, clause.binders, &clause.value); // first, see if the implication's conclusion might solve our goal - fulfill.unify(&goal.environment, &goal.goal, &implication.consequence)?; + if fulfill.unify(&goal.environment, &goal.goal, &consequence)?.ambiguous && from_env { + // here, using this environmental assumption would require unifying a skolemized + // variable, which can only appear in an *environment*, never the + // program. We view the program as providing a "closed world" of + // possible types and impls, and thus we can safely abandon this + // route of proving our goal. + // + // You can see this at work in the following example, where the + // assumption in the `if` is ignored since it cannot actually be applied. + // + // ``` + // program { + // struct i32 { } + // struct u32 { } + // + // trait Foo { } + // + // impl Foo for T { } + // } + // + // goal { + // forall { + // exists { + // if (i32: Foo) { + // T: Foo + // } + // } + // } + // } yields { + // "Unique" + // } + // ``` + + Err("using the implication would require changing a forall variable")?; + } // if so, toss in all of its premises - for condition in implication.conditions { + for condition in conditions { fulfill.push_goal(&goal.environment, condition); } diff --git a/src/solve/test.rs b/src/solve/test.rs index 02b1c19342a..a075adc8d3b 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -40,11 +40,8 @@ fn solve_goal(program_text: &str, let overflow_depth = 3; let mut solver = Solver::new(&env, overflow_depth); - let goal = ir::Canonical { - value: ir::InEnvironment::new(&ir::Environment::new(), *goal), - binders: vec![], - }; - let result = match solver.solve_goal(goal) { + let goal = ir::InEnvironment::new(&ir::Environment::new(), *goal); + let result = match solver.solve_closed_goal(goal) { Ok(v) => format!("{}", v), Err(e) => format!("No possible solution: {}", e), }; @@ -145,7 +142,7 @@ fn prove_forall() { goal { forall { T: Marker } } yields { - "No possible solution" + "Ambiguous; no inference guidance" } // If we assume `T: Marker`, then obviously `T: Marker`. @@ -168,7 +165,7 @@ fn prove_forall() { goal { forall { Vec: Clone } } yields { - "No possible solution" + "Ambig" } // Here, we do know that `T: Clone`, so we can. @@ -253,7 +250,7 @@ fn max_depth() { } #[test] -fn normalize() { +fn normalize_basic() { test! { program { trait Iterator { type Item; } @@ -291,7 +288,7 @@ fn normalize() { } } } yields { - "Unique; substitution [?0 := u32], lifetime constraints []" + "Ambiguous; suggested substitution [?0 := u32]" } goal { @@ -305,6 +302,28 @@ fn normalize() { } yields { "Unique; substitution [?0 := (Iterator::Item)]" } + + goal { + forall { + if (T: Iterator) { + ::Item = ::Item + } + } + } yields { + "Unique" + } + + goal { + forall { + if (T: Iterator) { + exists { + ::Item = ::Item + } + } + } + } yields { + "Unique" + } } } @@ -859,7 +878,7 @@ fn mixed_indices_normalize_application() { } } } yields { - "Ambig" + "Unique" } } } @@ -1195,9 +1214,7 @@ fn negation_free_vars() { } } -// TODO: get this test working! #[test] -#[ignore] fn where_clause_trumps() { test! { program { @@ -1218,3 +1235,29 @@ fn where_clause_trumps() { } } } + +#[test] +fn inapplicable_assumption_does_not_shadow() { + test! { + program { + struct i32 { } + struct u32 { } + + trait Foo { } + + impl Foo for T { } + } + + goal { + forall { + exists { + if (i32: Foo) { + T: Foo + } + } + } + } yields { + "Unique" + } + } +} diff --git a/src/zip.rs b/src/zip.rs index 8b63925af3d..d5b5cebcb88 100644 --- a/src/zip.rs +++ b/src/zip.rs @@ -155,6 +155,6 @@ macro_rules! enum_zip { } } -enum_zip!(DomainGoal { Implemented, RawNormalize, Normalize, WellFormed }); +enum_zip!(DomainGoal { Implemented, Normalize, WellFormed }); enum_zip!(LeafGoal { DomainGoal, EqGoal }); enum_zip!(WellFormed { Ty, TraitRef });