Use substitutions and suggestions in Solution

This commit is a major refactoring with a few goals:

- Move `Solution` to a Unique/Ambiguous model, with the ambiguous case
  encompassing multiple forms of guidance for type inference (including
  "suggestions" intended to be applied as fallback).

- Remove the notion of goal refinement, and instead use substitutions
  for communicating solutions.

- Draw a more clear line between the generic Chalk engine (which "only
  knows Prolog", i.e. doesn't know anything special about Rust) and
  lowering. Put differently, everything specific to Rust should now be
  encoded in the lowering, rather than though special cases in the Chalk
  engine. This work is somewhat incomplete: the commit removes the
  normalization fallback, which was one major special case, but doesn't
  yet replace it. A follow up PR will introduce negation and use it in
  lowering to recover this fallback.

- Consolidate the solver code so that the "strategies" for solving leaf
  goals are more clear and all co-located.

- Introduce some of the heuristics that rustc performs for inference,
  e.g. preferring `where` clauses for influencing inference. We do this
  in a way that decouples the heuristics from the rest of the solver;
  the `favor_over` method, in particular, contains the relevant logic.

Author: aturon

src/bin/repl.rs

@@ -11,7 +11,6 @@ use std::sync::Arc;
 
 use chalk::ir;
 use chalk::lower::*;
-use chalk::solve::prove::Prove;
 use chalk::solve::solver::Solver;
 
 use rustyline::error::ReadlineError;
@@ -121,9 +120,9 @@ 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);
-    match Prove::new(&mut solver, goal).solve() {
-        Ok(v) => println!("{:#?}", v),
-        Err(e) => println!("{}", e),
+    match solver.solve_goal(*goal) {
+        Ok(v) => println!("{}\n", v),
+        Err(e) => println!("No possible solution: {}\n", e),
     }
     Ok(())
 }

src/cast.rs

@@ -1,5 +1,4 @@
 use ir::*;
-use solve::Solution;
 
 pub trait Cast<T>: Sized {
     fn cast(self) -> T;
@@ -23,59 +22,62 @@ macro_rules! reflexive_impl {
 }
 
 reflexive_impl!(TraitRef);
-reflexive_impl!(WhereClause);
-reflexive_impl!(WhereClauseGoal);
+reflexive_impl!(LeafGoal);
+reflexive_impl!(DomainGoal);
 
-impl Cast<WhereClause> for TraitRef {
-    fn cast(self) -> WhereClause {
-        WhereClause::Implemented(self)
+impl Cast<DomainGoal> for TraitRef {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::Implemented(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for TraitRef {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::Implemented(self)
+impl Cast<LeafGoal> for TraitRef {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self.cast())
     }
 }
 
-impl Cast<WhereClause> for Normalize {
-    fn cast(self) -> WhereClause {
-        WhereClause::Normalize(self)
+impl Cast<DomainGoal> for Normalize {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::Normalize(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for Normalize {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::Normalize(self)
+impl Cast<LeafGoal> for Normalize {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self.cast())
     }
 }
 
-impl Cast<WhereClauseGoal> for WellFormed {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::WellFormed(self)
+impl Cast<DomainGoal> for WellFormed {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::WellFormed(self)
+    }
+}
+
+impl Cast<LeafGoal> for WellFormed {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self.cast())
     }
 }
 
 impl Cast<Goal> for WellFormed {
     fn cast(self) -> Goal {
-        let wcg: WhereClauseGoal = self.cast();
+        let wcg: LeafGoal = self.cast();
         wcg.cast()
     }
 }
 
 impl Cast<Goal> for Normalize {
     fn cast(self) -> Goal {
-        let wcg: WhereClauseGoal = self.cast();
+        let wcg: LeafGoal = self.cast();
         wcg.cast()
     }
 }
 
-impl Cast<WhereClauseGoal> for WhereClause {
-    fn cast(self) -> WhereClauseGoal {
-        match self {
-            WhereClause::Implemented(a) => a.cast(),
-            WhereClause::Normalize(a) => a.cast(),
-        }
+impl Cast<LeafGoal> for DomainGoal {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self)
     }
 }
 
@@ -85,27 +87,21 @@ impl Cast<Goal> for TraitRef {
     }
 }
 
-impl Cast<Goal> for WhereClause {
+impl Cast<Goal> for DomainGoal {
     fn cast(self) -> Goal {
         Goal::Leaf(self.cast())
     }
 }
 
-impl Cast<Goal> for WhereClauseGoal {
+impl Cast<Goal> for LeafGoal {
     fn cast(self) -> Goal {
         Goal::Leaf(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for Unify<Ty> {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::UnifyTys(self)
-    }
-}
-
-impl Cast<WhereClauseGoal> for Unify<Lifetime> {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::UnifyLifetimes(self)
+impl Cast<LeafGoal> for EqGoal {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::EqGoal(self)
     }
 }
 
@@ -126,10 +122,8 @@ macro_rules! map_impl {
 }
 
 map_impl!(impl[T: Cast<U>, U] Cast<Option<U>> for Option<T>);
-map_impl!(impl[T: Cast<U>, U] Cast<Query<U>> for Query<T>);
-map_impl!(impl[T: Cast<U>, U] Cast<Solution<U>> for Solution<T>);
+map_impl!(impl[T: Cast<U>, U] Cast<Canonical<U>> for Canonical<T>);
 map_impl!(impl[T: Cast<U>, U] Cast<InEnvironment<U>> for InEnvironment<T>);
-map_impl!(impl[T: Cast<U>, U] Cast<Constrained<U>> for Constrained<T>);
 map_impl!(impl[T: Cast<U>, U, E] Cast<Result<U, E>> for Result<T, E>);
 
 impl<T, U> Cast<Vec<U>> for Vec<T>

src/fold/mod.rs

@@ -2,6 +2,7 @@ use errors::*;
 use ir::*;
 use std::fmt::Debug;
 use std::sync::Arc;
+use std::collections::BTreeMap;
 
 mod instantiate;
 mod shifted;
@@ -139,6 +140,23 @@ impl Fold for Lifetime {
     }
 }
 
+impl Fold for Substitution {
+    type Result = Substitution;
+    fn fold_with(&self, folder: &mut Folder, binders: usize) -> Result<Self::Result> {
+        let mut tys = BTreeMap::new();
+        let mut lifetimes = BTreeMap::new();
+
+        for (var, ty) in &self.tys {
+            tys.insert(*var, ty.fold_with(folder, binders)?);
+        }
+        for (var, lt) in &self.lifetimes {
+            lifetimes.insert(*var, lt.fold_with(folder, binders)?);
+        }
+
+        Ok(Substitution { tys, lifetimes })
+    }
+}
+
 macro_rules! copy_fold {
     ($t:ty) => {
         impl Fold for $t {
@@ -178,10 +196,9 @@ macro_rules! enum_fold {
 }
 
 enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
-enum_fold!(WhereClause[] { Implemented(a), Normalize(a) });
+enum_fold!(DomainGoal[] { Implemented(a), Normalize(a), WellFormed(a) });
 enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });
-enum_fold!(WhereClauseGoal[] { Implemented(a), Normalize(a), UnifyTys(a),
-                               UnifyLifetimes(a), WellFormed(a) });
+enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
 enum_fold!(Constraint[] { LifetimeEq(a, b) });
 enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Leaf(wc) });
 
@@ -206,6 +223,6 @@ struct_fold!(AssociatedTyValue { associated_ty_id, value });
 struct_fold!(AssociatedTyValueBound { ty, where_clauses });
 struct_fold!(Environment { universe, clauses });
 struct_fold!(InEnvironment[F] { environment, goal } where F: Fold);
-struct_fold!(Unify[T] { a, b } where T: Fold);
-struct_fold!(Constrained[F] { value, constraints } where F: Fold);
+struct_fold!(EqGoal { a, b });
 struct_fold!(ProgramClauseImplication { consequence, conditions });
+struct_fold!(ConstrainedSubst { subst, constraints });

src/ir/debug.rs

@@ -145,35 +145,27 @@ impl Debug for Normalize {
     }
 }
 
-impl Debug for WhereClause {
+impl Debug for DomainGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match *self {
-            WhereClause::Normalize(ref n) => write!(fmt, "{:?}", n),
-            WhereClause::Implemented(ref n) => {
+            DomainGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
+            DomainGoal::Implemented(ref n) => {
                 write!(fmt,
                        "{:?}: {:?}{:?}",
                        n.parameters[0],
                        n.trait_id,
                        Angle(&n.parameters[1..]))
             }
+            DomainGoal::WellFormed(ref n) => write!(fmt, "{:?}", n),
         }
     }
 }
 
-impl Debug for WhereClauseGoal {
+impl Debug for LeafGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match *self {
-            WhereClauseGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::Implemented(ref n) => {
-                write!(fmt,
-                       "{:?}: {:?}{:?}",
-                       n.parameters[0],
-                       n.trait_id,
-                       Angle(&n.parameters[1..]))
-            }
-            WhereClauseGoal::UnifyTys(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::UnifyLifetimes(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::WellFormed(ref n) => write!(fmt, "{:?}", n),
+            LeafGoal::EqGoal(ref eq) => write!(fmt, "{:?}", eq),
+            LeafGoal::DomainGoal(ref dom) => write!(fmt, "{:?}", dom),
         }
     }
 }
@@ -188,7 +180,7 @@ impl Debug for WellFormed {
     }
 }
 
-impl<T: Debug> Debug for Unify<T> {
+impl Debug for EqGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         write!(fmt, "({:?} = {:?})", self.a, self.b)
     }