Add variance and generalizer tests

Added tests that verify that the generalizer works and outputs the
correct constraints, and tests that verify variance is being handled
correctly.

Co-authored-by: David Ross <daboross@daboross.net>

Author: 2 people

tests/test/subtype.rs

@@ -72,20 +72,49 @@ fn ref_lifetime_variance() {
 }
 
 #[test]
-fn fn_lifetime_variance() {
+fn fn_lifetime_variance_args() {
     test! {
         program {
         }
 
         goal {
-            Subtype(for<'a, 'b> fn(&'a u32, &'b u32), for<'a> fn(&'a u32, &'a u32))
+            for<'a, 'b> fn(&'a u32, &'b u32) = for<'a> fn(&'a u32, &'a u32)
         } yields {
+            "Unique;substitution [], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }]"
+        }
+    }
+}
+
+#[test]
+fn fn_lifetime_variance_with_return_type() {
+    test! {
+        program {
+        }
+
+        goal {
+            Subtype(for<'a, 'b> fn(&'a u32, &'b u32) -> &'a u32, for<'a> fn(&'a u32, &'a u32) -> &'a u32)
+        } yields {
+            // TODO: are these results actually correct?
             "Unique; for<?U1,?U1> { substitution [], lifetime constraints [\
-            InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
-            InEnvironment { environment: Env([]), goal: '!1_0: '^0.1 }] }"
+                InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
+                InEnvironment { environment: Env([]), goal: '!1_0: '^0.1 }, \
+                InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }  \
+            ]}"
+        }
+        goal {
+            Subtype(for<'a> fn(&'a u32, &'a u32) -> &'a u32, for<'a, 'b> fn(&'a u32, &'b u32) -> &'a u32)
+        } yields {
+            "Unique; for<?U1> { substitution [], lifetime constraints [\
+                InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
+                InEnvironment { environment: Env([]), goal: '!1_1: '^0.0 }, \
+                InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }  \
+            ] }"
         }
     }
 }
+
 #[test]
 fn generalize() {
     test! {
@@ -108,6 +137,8 @@ fn generalize() {
     }
 }
 
+/// Tests that the generalizer correctly generalizes lifetimes (as opposed to
+/// just that variance in general works).
 #[test]
 fn multi_lifetime() {
     test! {
@@ -121,6 +152,160 @@ fn multi_lifetime() {
                 }
             }
         } yields {
+            // Without the generalizer, we would yield a result like this:
+            //
+            // "Unique; substitution [?0 := (&'!1_1 Uint(U32))], lifetime
+            // constraints [InEnvironment { environment: Env([]), goal: '!1_1: '!1_0
+            // }]"
+            //
+            // This is incorrect, as we shouldn't be requiring 'a and 'b to be
+            // related to eachother. Instead, U should be &'?1 u32, with constraints
+            // ?1 : 'a, ?1: 'b.
+            "Unique; for<?U1> { substitution [?0 := (&'^0.0 Uint(U32))], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '!1_0: '^0.0  }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '^0.0  }] }"
+        }
+    }
+}
+
+/// Tests that the generalizer generalizes lifetimes within a covariant struct.
+#[test]
+fn multi_lifetime_covariant_struct() {
+    test! {
+        program {
+            #[variance(Covariant)]
+            struct Foo<A> {}
+        }
+
+        goal {
+            forall<'a, 'b> {
+                exists<U> {
+                    Subtype(Foo<&'a u32>, Foo<U>),
+                    Subtype(Foo<&'b u32>, Foo<U>)
+                }
+            }
+        } yields {
+            // Result should be identical to multi_lifetime result.
+            "Unique; for<?U1> { substitution [?0 := (&'^0.0 Uint(U32))], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '!1_0: '^0.0  }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '^0.0  }] }"
+        }
+    }
+}
+
+/// Tests that the generalizer generalizes lifetimes within a contravariant
+/// struct, and that that variance contravariance is recognized.
+#[test]
+fn multi_lifetime_contravariant_struct() {
+    test! {
+        program {
+            #[variance(Contravariant)]
+            struct Foo<A> {}
+        }
+
+        goal {
+            forall<'a, 'b> {
+                exists<U> {
+                    Subtype(Foo<&'a u32>, Foo<U>),
+                    Subtype(Foo<&'b u32>, Foo<U>)
+                }
+            }
+        } yields {
+            // Result should be opposite multi_lifetime result.
+            "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 }] }"
+        }
+    }
+}
+
+/// Tests that the generalizer generalizes lifetimes within a invariant struct.
+#[test]
+fn multi_lifetime_invariant_struct() {
+    test! {
+        program {
+            #[variance(Invariant)]
+            struct Foo<A> {}
+        }
+
+        goal {
+            forall<'a, 'b> {
+                exists<U> {
+                    Subtype(Foo<&'a u32>, Foo<U>),
+                    Subtype(Foo<&'b u32>, Foo<U>)
+                }
+            }
+        } yields {
+            // Because A is invariant, we require the lifetimes to be equal
+            "Unique; substitution [?0 := (&'!1_1 Uint(U32))], lifetime
+            constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }]"
+        }
+    }
+}
+
+/// Tests that the generalizer generalizes lifetimes within slices correctly.
+#[test]
+fn multi_lifetime_slice() {
+    test! {
+        program {
+        }
+
+        goal {
+            forall<'a, 'b> {
+                exists<U> {
+                    Subtype([&'a u32], [U]),
+                    Subtype([&'b u32], [U])
+                }
+            }
+        } yields {
+            // Result should be identical to multi_lifetime result.
+            "Unique; for<?U1> { substitution [?0 := (&'^0.0 Uint(U32))], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '!1_0: '^0.0  }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '^0.0  }] }"
+        }
+    }
+}
+
+/// Tests that the generalizer generalizes lifetimes within tuples correctly.
+#[test]
+fn multi_lifetime_tuple() {
+    test! {
+        program {
+        }
+
+        goal {
+            forall<'a, 'b> {
+                exists<U> {
+                    Subtype((&'a u32, &'a u32), [U]),
+                    Subtype((&'b u32, &'b u32), [U])
+                }
+            }
+        } yields {
+            // Result should be identical to multi_lifetime result.
+            "Unique; for<?U1> { substitution [?0 := (&'^0.0 Uint(U32))], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '!1_0: '^0.0  }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '^0.0  }] }"
+        }
+    }
+}
+
+/// Tests that the generalizer generalizes lifetimes within tuples correctly.
+#[test]
+fn multi_lifetime_array() {
+    test! {
+        program {
+        }
+
+        goal {
+            forall<'a, 'b> {
+                exists<U> {
+                    Subtype([&'a u32; 16], [U]),
+                    Subtype([&'b u32; 16], [U])
+                }
+            }
+        } yields {
+            // Result should be identical to multi_lifetime result.
             "Unique; for<?U1> { substitution [?0 := (&'^0.0 Uint(U32))], lifetime constraints [\
             InEnvironment { environment: Env([]), goal: '!1_0: '^0.0  }, \
             InEnvironment { environment: Env([]), goal: '!1_1: '^0.0  }] }"