Switch to unifying non-general inference vars

rust-lang · Nov 30, 2020 · cc535ea · cc535ea
1 parent 8e0fe62
commit cc535ea
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 42 deletions.
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
@@ -96,33 +96,43 @@ impl<'t, I: Interner> Unifier<'t, I> {
 
         match (a.kind(interner), b.kind(interner)) {
             // Relating two inference variables:
+            // First, if either variable is a float or int kind, then we always
+            // unify if they match. This is because float and ints don't have
+            // subtype relationships.
+            // If both kinds are general then:
             // If `Invariant`, unify them in the underlying ena table.
             // If `Covariant` or `Contravariant`, push `SubtypeGoal`
             (&TyKind::InferenceVar(var1, kind1), &TyKind::InferenceVar(var2, kind2)) => {
-                match variance {
-                    Variance::Invariant => {
-                        if kind1 == kind2 {
+                if matches!(kind1, TyVariableKind::General) && matches!(kind2, TyVariableKind::General) {
+                    // Both variable kinds are general; so unify if invariant, otherwise push subtype goal
+                    match variance {
+                        Variance::Invariant => {
                             self.unify_var_var(var1, var2)
-                        } else if kind1 == TyVariableKind::General {
-                            self.unify_general_var_specific_ty(var1, b.clone())
-                        } else if kind2 == TyVariableKind::General {
-                            self.unify_general_var_specific_ty(var2, a.clone())
-                        } else {
-                            debug!(
-                                "Tried to unify mis-matching inference variables: {:?} and {:?}",
-                                kind1, kind2
-                            );
-                            Err(NoSolution)
+                        }
+                        Variance::Covariant => {
+                            self.push_subtype_goal(a.clone(), b.clone());
+                            Ok(())
+                        }
+                        Variance::Contravariant => {
+                            self.push_subtype_goal(b.clone(), a.clone());
+                            Ok(())
                         }
                     }
-                    Variance::Covariant => {
-                        self.push_subtype_goal(a.clone(), b.clone());
-                        Ok(())
-                    }
-                    Variance::Contravariant => {
-                        self.push_subtype_goal(b.clone(), a.clone());
-                        Ok(())
-                    }
+                } else if kind1 == kind2 {
+                    // At least one kind is not general, but they match, so unify
+                    self.unify_var_var(var1, var2)
+                } else if kind1 == TyVariableKind::General {
+                    // First kind is general, second isn't, unify
+                    self.unify_general_var_specific_ty(var1, b.clone())
+                } else if kind2 == TyVariableKind::General {
+                    // Second kind is general, first isn't, unify
+                    self.unify_general_var_specific_ty(var2, a.clone())
+                } else {
+                    debug!(
+                        "Tried to unify mis-matching inference variables: {:?} and {:?}",
+                        kind1, kind2
+                    );
+                    Err(NoSolution)
                 }
             }
 
@@ -1071,23 +1081,9 @@ impl<'t, I: Interner> Unifier<'t, I> {
 
     /// Pushes a goal of `a` being a subtype of `b`.
     fn push_subtype_goal(&mut self, a: Ty<I>, b: Ty<I>) {
-        let inverse = self.goals.iter().position(|g| {
-            if g.environment != *self.environment {
-                return false;
-            }
-            match g.goal.data(self.interner()) {
-                GoalData::SubtypeGoal(SubtypeGoal { a: a1, b: b1 }) => a == *b1 && b == *a1,
-                _ => false,
-            }
-        });
-        if let Some(inverse) = inverse {
-            self.goals.remove(inverse);
-            self.relate_ty_ty(Variance::Invariant, &a, &b).unwrap();
-        } else {
-            let subtype_goal = GoalData::SubtypeGoal(SubtypeGoal { a, b }).intern(self.interner());
-            self.goals
-                .push(InEnvironment::new(self.environment, subtype_goal));
-        }
+        let subtype_goal = GoalData::SubtypeGoal(SubtypeGoal { a, b }).intern(self.interner());
+        self.goals
+            .push(InEnvironment::new(self.environment, subtype_goal));
     }
 }
 

diff --git a/tests/test/misc.rs b/tests/test/misc.rs
@@ -764,14 +764,18 @@ fn empty_definite_guidance() {
 fn ambiguous_unification_in_fn() {
     test! {
         program {
-            trait FnOnce<Args> {}
+            trait FnOnce<Args> {
+                type Output;
+            }
 
             struct MyClosure<T> {}
-            impl<T> FnOnce<T> for MyClosure<fn(T) -> ()> {}
+            impl<T> FnOnce<(T,)> for MyClosure<fn(T) -> ()> {
+                type Output = ();
+            }
         }
         goal {
-            exists<T, U> {
-                MyClosure<fn(U) -> ()>: FnOnce<T>
+            exists<int T, U> {
+                MyClosure<fn(&'static U) -> ()>: FnOnce<(&'static T,)>
             }
         } yields {
             "Unique"