Converting back to overlap instead of disjoint so that we workaround

the implementation of `not` and produce `Ambiguous` when we expect to.
Needed to delete a test because it would no longer lower now that the
overlap check works correctly.

Author: sunjay

src/coherence/solve.rs

@@ -7,7 +7,7 @@ use ir::*;
 use cast::*;
 use solve::{SolverChoice, Solution};
 
-struct DisjointSolver {
+struct OverlapSolver {
     env: Arc<ProgramEnvironment>,
     solver_choice: SolverChoice,
 }
@@ -21,7 +21,7 @@ impl Program {
     where
         F: FnMut(ItemId, ItemId),
     {
-        let mut solver = DisjointSolver {
+        let mut solver = OverlapSolver {
             env: Arc::new(self.environment()),
             solver_choice,
         };
@@ -65,7 +65,7 @@ impl Program {
                 // Check if the impls overlap, then if they do, check if one specializes
                 // the other. Note that specialization can only run one way - if both
                 // specialization checks return *either* true or false, that's an error.
-                if !solver.disjoint(lhs, rhs) {
+                if solver.overlap(lhs, rhs) {
                     match (solver.specializes(lhs, rhs), solver.specializes(rhs, lhs)) {
                         (true, false) => record_specialization(l_id, r_id),
                         (false, true) => record_specialization(r_id, l_id),
@@ -82,36 +82,36 @@ impl Program {
     }
 }
 
-impl DisjointSolver {
-    // Test if two impls are disjoint. If the test does not succeed, there is an overlap.
+impl OverlapSolver {
+    // Test if the set of types that these two impls apply to overlap. If the test succeeds, these
+    // two impls overlap.
     //
     // We combine the binders of the two impls & treat them as existential
     // quantifiers. Then we attempt to unify the input types to the trait provided
     // by each impl, as well as prove that the where clauses from both impls all
-    // hold. At the end, we negate the query because we only want to return `true` if
-    // it is provable that there is no overlap.
+    // hold.
     //
     // Examples:
     //
     //  Impls:
     //      impl<T> Foo for T { }
     //      impl Foo for i32 { }
     //  Generates:
-    //      compatible { not { exists<T> { T = i32 } } }
+    //      compatible { exists<T> { T = i32 } }
     //
     //  Impls:
     //      impl<T1, U> Foo<T1> for Vec<U> { }
     //      impl<T2> Foo<T2> for Vec<i32> { }
     //  Generates:
-    //      compatible { not { exists<T1, U, T2> { Vec<U> = Vec<i32>, T1 = T2 } } }
+    //      compatible { exists<T1, U, T2> { Vec<U> = Vec<i32>, T1 = T2 } }
     //
     //  Impls:
     //      impl<T> Foo for Vec<T> where T: Bar { }
     //      impl<U> Foo for Vec<U> where U: Baz { }
     //  Generates:
-    //      compatible { not { exists<T, U> { Vec<T> = Vec<U>, T: Bar, U: Baz } } }
+    //      compatible { exists<T, U> { Vec<T> = Vec<U>, T: Bar, U: Baz } }
     //
-    fn disjoint(&self, lhs: &ImplDatum, rhs: &ImplDatum) -> bool {
+    fn overlap(&self, lhs: &ImplDatum, rhs: &ImplDatum) -> bool {
         debug_heading!("overlaps(lhs={:#?}, rhs={:#?})", lhs, rhs);
 
         let lhs_len = lhs.binders.len();
@@ -150,19 +150,19 @@ impl DisjointSolver {
             .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
             .expect("Every trait takes at least one input type")
             .quantify(QuantifierKind::Exists, binders)
-            .negate()
             .compatible();
 
         let canonical_goal = &goal.into_closed_goal();
         let solution = self.solver_choice
             .solve_root_goal(&self.env, canonical_goal)
             .unwrap(); // internal errors in the solver are fatal
         let result = match solution {
-            // Goal was proven with a unique solution, so impls are disjoint
-            Some(Solution::Unique(_)) => true,
+            // Goal was proven with a unique solution, so an impl was found that causes these two
+            // to overlap
+            Some(Solution::Unique(_)) |
             // Goal was ambiguous, so there *may* be overlap
-            Some(Solution::Ambig(_)) |
-            // Goal cannot be proven, so impls definitely overlap
+            Some(Solution::Ambig(_)) => true,
+            // Goal cannot be proven, so impls are disjoint
             None => false,
         };
         debug!("overlaps: result = {:?}", result);

src/coherence/test.rs

@@ -62,21 +62,18 @@ fn two_blanket_impls() {
 }
 
 #[test]
-// FIXME This should be an error
-// We currently assume a closed universe always, but overlaps checking should
-// assume an open universe - what if a client implemented both Bar and Baz
-//
-// In other words, this should have the same behavior as the two_blanket_impls
-// test.
 fn two_blanket_impls_open_ended() {
-    lowering_success! {
+    lowering_error! {
         program {
             trait Foo { }
             trait Bar { }
             trait Baz { }
             impl<T> Foo for T where T: Bar { }
             impl<T> Foo for T where T: Baz { }
         }
+        error_msg {
+            "overlapping impls of trait \"Foo\""
+        }
     }
 }
 

src/ir.rs

@@ -1102,11 +1102,6 @@ impl Goal {
         )
     }
 
-    /// Takes a goal `G` and turns it into `not { G }`
-    crate fn negate(self) -> Self {
-        Goal::Not(Box::new(self))
-    }
-
     /// Takes a goal `G` and turns it into `compatible { G }`
     crate fn compatible(self) -> Self {
         // compatible { G } desugars into: forall<T> { if (Compatible, DownstreamType(T)) { G } }

src/solve/slg/test.rs

@@ -744,10 +744,10 @@ fn example_3_3_EWFS() {
                     delayed_literals: DelayedLiteralSet {
                         delayed_literals: {
                             Negative(
-                                TableIndex(4)
+                                TableIndex(1)
                             ),
                             Negative(
-                                TableIndex(1)
+                                TableIndex(6)
                             )
                         }
                     }

src/solve/test.rs

@@ -1936,28 +1936,6 @@ fn mixed_semantics() {
     }
 }
 
-#[test]
-fn partial_overlap_1() {
-    test! {
-        program {
-            trait Marker {}
-            trait Foo {}
-            trait Bar {}
-
-            impl<T> Marker for T where T: Foo {}
-            impl<T> Marker for T where T: Bar {}
-        }
-
-        goal {
-            forall<T> {
-                if (T: Foo; T: Bar) { T: Marker }
-            }
-        } yields {
-            "Unique"
-        }
-    }
-}
-
 #[test]
 fn partial_overlap_2() {
     test! {