Fix unify_lifetime_var

daboross · Oct 25, 2020 · ee6b3d1 · ee6b3d1
1 parent 7967679
commit ee6b3d1
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 11 deletions.
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
@@ -831,19 +831,19 @@ impl<'t, I: Interner> Unifier<'t, I> {
             }
 
             (&LifetimeData::InferenceVar(a_var), &LifetimeData::Placeholder(b_idx)) => {
-                self.unify_lifetime_var(variance, a, b, a_var, b, b_idx.ui)
+                self.unify_lifetime_var(variance, a_var, b, b_idx.ui)
             }
 
             (&LifetimeData::Placeholder(a_idx), &LifetimeData::InferenceVar(b_var)) => {
-                self.unify_lifetime_var(variance, a, b, b_var, a, a_idx.ui)
+                self.unify_lifetime_var(variance.invert(), b_var, a, a_idx.ui)
             }
 
             (&LifetimeData::InferenceVar(a_var), &LifetimeData::Static) => {
-                self.unify_lifetime_var(variance, a, b, a_var, b, UniverseIndex::root())
+                self.unify_lifetime_var(variance, a_var, b, UniverseIndex::root())
             }
 
             (&LifetimeData::Static, &LifetimeData::InferenceVar(b_var)) => {
-                self.unify_lifetime_var(variance, a, b, b_var, a, UniverseIndex::root())
+                self.unify_lifetime_var(variance.invert(), b_var, a, UniverseIndex::root())
             }
 
             (&LifetimeData::Static, &LifetimeData::Static) => Ok(()),
@@ -871,15 +871,13 @@ impl<'t, I: Interner> Unifier<'t, I> {
     fn unify_lifetime_var(
         &mut self,
         variance: Variance,
-        a: &Lifetime<I>,
-        b: &Lifetime<I>,
         var: InferenceVar,
         value: &Lifetime<I>,
         value_ui: UniverseIndex,
     ) -> Fallible<()> {
         let var = EnaVariable::from(var);
         let var_ui = self.table.universe_of_unbound_var(var);
-        if var_ui.can_see(value_ui) {
+        if var_ui.can_see(value_ui) && matches!(variance, Variance::Invariant) {
             debug!("{:?} in {:?} can see {:?}; unifying", var, var_ui, value_ui);
             self.table
                 .unify
@@ -894,7 +892,11 @@ impl<'t, I: Interner> Unifier<'t, I> {
                 "{:?} in {:?} cannot see {:?}; pushing constraint",
                 var, var_ui, value_ui
             );
-            Ok(self.push_lifetime_eq_goals(variance, a.clone(), b.clone()))
+            Ok(self.push_lifetime_eq_goals(
+                variance,
+                var.to_lifetime(&self.interner),
+                value.clone(),
+            ))
         }
     }
 

diff --git a/tests/test/subtype.rs b/tests/test/subtype.rs
@@ -35,6 +35,7 @@ fn subtype_simple() {
 fn struct_lifetime_variance() {
     test! {
         program {
+            #[variance(Covariant)]
             struct Foo<'a> { }
         }
 
@@ -43,10 +44,8 @@ fn struct_lifetime_variance() {
                 Subtype(Foo<'a>, Foo<'b>)
             }
         } yields {
-            // FIXME: we should really just require this in one direction?
             "Unique; substitution [], lifetime constraints [\
             InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
-            InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }\
             ]"
         }
     }
@@ -81,7 +80,9 @@ fn fn_lifetime_variance() {
         goal {
             Subtype(for<'a, 'b> fn(&'a u32, &'b u32), for<'a> fn(&'a u32, &'a u32))
         } yields {
-            "Unique; substitution [], lifetime constraints []"
+            "Unique; for<?U1,?U1> { substitution [], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }, \
+            InEnvironment { environment: Env([]), goal: '^0.1: '!1_0 }] }"
         }
     }
 }
@@ -106,3 +107,23 @@ fn generalize() {
         }
     }
 }
+
+#[test]
+fn multi_lifetime() {
+    test! {
+        program {}
+
+        goal {
+            forall<'a, 'b> {
+                exists<U> {
+                    Subtype(&'a u32, U),
+                    Subtype(&'b u32, U)
+                }
+            }
+        } yields {
+            "Unique; for<?U1> { substitution [?0 := (&'^0.0 Uint(U32))], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }, \
+            InEnvironment { environment: Env([]), goal: '^0.0: '!1_1 }] }"
+        }
+    }
+}