Merge pull request #191 from scalexm/subtype

Add a variance parameter to `HhGoal::Unify`

Author: nikomatsakis

chalk-engine/src/context.rs

@@ -103,6 +103,11 @@ pub trait Context: Clone + Debug {
     /// A vector of program clauses.
     type ProgramClauses: Debug;
 
+    /// How to relate two kinds when unifying: for example in rustc, we
+    /// may want to unify parameters either for the sub-typing relation or for
+    /// the equality relation.
+    type Variance;
+
     /// The successful result from unification: contains new subgoals
     /// and things that can be attached to an ex-clause.
     type UnificationResult;
@@ -307,6 +312,7 @@ pub trait UnificationOps<C: Context, I: Context> {
     fn unify_parameters(
         &mut self,
         environment: &I::Environment,
+        variance: I::Variance,
         a: &I::Parameter,
         b: &I::Parameter,
     ) -> Fallible<I::UnificationResult>;

chalk-engine/src/hh.rs

@@ -10,7 +10,7 @@ pub enum HhGoal<C: Context> {
     Implies(C::ProgramClauses, C::Goal),
     And(C::Goal, C::Goal),
     Not(C::Goal),
-    Unify(C::Parameter, C::Parameter),
+    Unify(C::Variance, C::Parameter, C::Parameter),
     DomainGoal(C::DomainGoal),
 
     /// Indicates something that cannot be proven to be true or false

chalk-engine/src/simplify.rs

@@ -47,8 +47,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
                         .subgoals
                         .push(Literal::Negative(I::goal_in_environment(&environment, subgoal)));
                 }
-                HhGoal::Unify(a, b) => {
-                    let result = infer.unify_parameters(&environment, &a, &b)?;
+                HhGoal::Unify(variance, a, b) => {
+                    let result = infer.unify_parameters(&environment, variance, &a, &b)?;
                     infer.into_ex_clause(result, &mut ex_clause)
                 }
                 HhGoal::DomainGoal(domain_goal) => {

chalk-solve/src/solve/slg/implementation.rs

@@ -58,6 +58,7 @@ impl context::Context for SlgContext {
     type GoalInEnvironment = InEnvironment<Goal>;
     type Substitution = Substitution;
     type RegionConstraint = InEnvironment<Constraint>;
+    type Variance = ();
 
     fn goal_in_environment(environment: &Arc<Environment>, goal: Goal) -> InEnvironment<Goal> {
         InEnvironment::new(environment, goal)
@@ -176,7 +177,7 @@ impl context::InferenceTable<SlgContext, SlgContext> for TruncatingInferenceTabl
             Goal::Implies(dg, subgoal) => HhGoal::Implies(dg, *subgoal),
             Goal::And(g1, g2) => HhGoal::And(*g1, *g2),
             Goal::Not(g1) => HhGoal::Not(*g1),
-            Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => HhGoal::Unify(a, b),
+            Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => HhGoal::Unify((), a, b),
             Goal::Leaf(LeafGoal::DomainGoal(domain_goal)) => HhGoal::DomainGoal(domain_goal),
             Goal::CannotProve(()) => HhGoal::CannotProve,
         }
@@ -276,6 +277,7 @@ impl context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTabl
     fn unify_parameters(
         &mut self,
         environment: &Arc<Environment>,
+        _: (),
         a: &Parameter,
         b: &Parameter,
     ) -> Fallible<UnificationResult> {