Clarify treatment of unification ambiguity and overhaul treatment of

aturon · aturon · commit 77246f302596 · 2017-06-06T17:38:36.000-07:00
normalization fallback.
diff --git 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<Prog
         ir::set_current_program(&prog.ir, || -> 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
@@ -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
@@ -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
@@ -129,8 +129,8 @@ impl Environment {
                         push_clause(where_clause);
                     }
                 }
-                DomainGoal::RawNormalize(Normalize { ref projection, ty: _ }) => {
-                    // raw { <T as Trait<U>>::Foo ===> V }
+                DomainGoal::Normalize(Normalize { ref projection, ty: _ }) => {
+                    // <T as Trait<U>>::Foo ===> V
                     // ----------------------------------------------------------
                     // T: Trait<U>
 
@@ -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<T> Binders<T> {
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct ProgramClause {
     pub implication: Binders<ProgramClauseImplication>,
+
+    /// 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
@@ -381,10 +381,7 @@ impl LowerWhereClause<ir::DomainGoal> 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<ir::DomainGoal> for WhereClause {
 impl LowerWhereClause<ir::LeafGoal> for WhereClause {
     fn lower(&self, env: &Env) -> Result<ir::LeafGoal> {
         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<T>: Iterable<IntoIter<'a> =raw Iter<'a, T>>) :-
+    ///     (Vec<T>: Iterable<IntoIter<'a> = Iter<'a, T>>) :-
     ///         (Vec<T>: 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<ir::ProgramClause> {
-        // 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<Assoc = ?U> :- ?T: Foo<Assoc =raw ?U>.
-        //    ?T: Foo<Assoc = (Foo::Assoc)<?T>> :- not { exists<U> { ?T: Foo<Assoc =raw U> } }.
+        //    <?T as Foo>::Assoc ==> (Foo::Assoc)<?T>.
 
         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 `<T as Iterator>::Item`,
             // we would produce `(Iterator::Item)<T>`.
             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
@@ -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<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<()>
+    pub fn unify<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<UnifyOutcome>
         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
@@ -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
@@ -43,8 +43,9 @@ pub struct UnificationResult {
     pub constraints: Vec<InEnvironment<Constraint>>,
 
     /// 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> { T = U } // Ambig
+                        //     forall<T, U> { 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
diff --git a/src/solve/solver.rs b/src/solve/solver.rs
diff --git a/src/solve/test.rs b/src/solve/test.rs
diff --git a/src/zip.rs b/src/zip.rs

Original file line number	Diff line number	Diff line change
`@@ -196,7 +196,7 @@ macro_rules! enum_fold {`
`196`	`196`	`}`
`197`	`197`
`198`	`198`	`enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);`
`199`		`-enum_fold!(DomainGoal[] { Implemented(a), RawNormalize(a), Normalize(a), WellFormed(a) });`
	`199`	`+enum_fold!(DomainGoal[] { Implemented(a), Normalize(a), WellFormed(a) });`
`200`	`200`	`enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });`
`201`	`201`	`enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });`
`202`	`202`	`enum_fold!(Constraint[] { LifetimeEq(a, b) });`
Original file line number	Diff line number	Diff line change
`@@ -129,8 +129,8 @@ impl Environment {`
`129`	`129`	`push_clause(where_clause);`
`130`	`130`	`}`
`131`	`131`	`}`
`132`		`- DomainGoal::RawNormalize(Normalize { ref projection, ty: _ }) => {`
`133`		`- // raw { <T as Trait<U>>::Foo ===> V }`
	`132`	`+ DomainGoal::Normalize(Normalize { ref projection, ty: _ }) => {`
	`133`	`+ // <T as Trait<U>>::Foo ===> V`
`134`	`134`	`// ----------------------------------------------------------`
`135`	`135`	`// T: Trait<U>`
`136`	`136`
`@@ -396,9 +396,6 @@ pub struct TraitRef {`
`396`	`396`	`#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]`
`397`	`397`	`pub enum DomainGoal {`
`398`	`398`	`Implemented(TraitRef),`
`399`		`- /// A projection we know definitively via an impl or where clause`
`400`		`- RawNormalize(Normalize),`
`401`		`- /// A general projection, which might employ fallback`
`402`	`399`	`Normalize(Normalize),`
`403`	`400`	`WellFormed(WellFormed),`
`404`	`401`	`}`
`@@ -414,7 +411,8 @@ impl DomainGoal {`
`414`	`411`	`conditions: vec![],`
`415`	`412`	`},`
`416`	`413`	`binders: vec![],`
`417`		`- }`
	`414`	`+ },`
	`415`	`+ fallback_clause: false,`
`418`	`416`	`}`
`419`	`417`	`}`
`420`	`418`	`}`
`@@ -478,6 +476,9 @@ impl<T> Binders<T> {`
`478`	`476`	`#[derive(Clone, Debug, PartialEq, Eq, Hash)]`
`479`	`477`	`pub struct ProgramClause {`
`480`	`478`	`pub implication: Binders<ProgramClauseImplication>,`
	`479`	`+`
	`480`	`+ /// Is this a fallback clause which should get lower priority?`
	`481`	`+ pub fallback_clause: bool,`
`481`	`482`	`}`
`482`	`483`
`483`	`484`	/// Represents one clause of the form `consequence :- conditions`.
`@@ -592,6 +593,10 @@ impl Substitution {`
`592`	`593`
`593`	`594`	`Substitution { tys, lifetimes }`
`594`	`595`	`}`
	`596`	`+`
	`597`	`+ pub fn is_empty(&self) -> bool {`
	`598`	`+ self.tys.is_empty() && self.lifetimes.is_empty()`
	`599`	`+ }`
`595`	`600`	`}`
`596`	`601`
`597`	`602`	`#[derive(Clone, Debug, PartialEq, Eq)]`