Merge pull request #165 from sunjay/compatible-overlap

nikomatsakis · web-flow · commit a63119ad2bb9 · 2018-07-18T07:25:35.000+03:00
Compatible Overlap Check in Chalk
diff --git a/src/coherence/solve.rs b/src/coherence/solve.rs
@@ -5,7 +5,7 @@ use itertools::Itertools;
 use errors::*;
 use ir::*;
 use cast::*;
-use solve::SolverChoice;
+use solve::{SolverChoice, Solution};
 
 struct DisjointSolver {
     env: Arc<ProgramEnvironment>,
@@ -83,33 +83,38 @@ impl Program {
 }
 
 impl DisjointSolver {
-    // Test if two impls are disjoint. If the test does not succeed, there is an overlap.
+    // Test if the set of types that these two impls apply to overlap. If the test succeeds, these
+    // two impls are disjoint.
     //
-    // 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.
+    // 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 apply the `compatible` modality
+    // and negate the query. Negating the query means that we are asking chalk to prove that no
+    // such overlapping impl exists. By applying `compatible { G }`, chalk attempts to prove that
+    // "there exists a compatible world where G is provable." When we negate compatible, it turns
+    // into the statement "for all compatible worlds, G is not provable." This is exactly what we
+    // want since we want to ensure that there is no overlap in *all* compatible worlds, not just
+    // that there is no overlap in *some* compatible world.
     //
     // Examples:
     //
     //  Impls:
     //      impl<T> Foo for T { }
     //      impl Foo for i32 { }
     //  Generates:
-    //      not { exists<T> { T = i32 } }
+    //      not { compatible { exists<T> { T = i32 } } }
     //
     //  Impls:
     //      impl<T1, U> Foo<T1> for Vec<U> { }
     //      impl<T2> Foo<T2> for Vec<i32> { }
     //  Generates:
-    //      not { exists<T1, U, T2> { Vec<U> = Vec<i32>, T1 = T2 } }
+    //      not { 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:
-    //      not { exists<T, U> { Vec<T> = Vec<U>, T: Bar, U: Baz } }
+    //      not { compatible { exists<T, U> { Vec<T> = Vec<U>, T: Bar, U: Baz } } }
     //
     fn disjoint(&self, lhs: &ImplDatum, rhs: &ImplDatum) -> bool {
         debug_heading!("overlaps(lhs={:#?}, rhs={:#?})", lhs, rhs);
@@ -150,15 +155,22 @@ 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();
+            .compatible()
+            .negate();
 
-        // Unless we can prove NO solution, we consider things to overlap.
         let canonical_goal = &goal.into_closed_goal();
-        let result = self.solver_choice
+        let solution = self.solver_choice
             .solve_root_goal(&self.env, canonical_goal)
-            .unwrap()
-            .is_some();
+            .unwrap(); // internal errors in the solver are fatal
+        let result = match solution {
+            // Goal was proven with a unique solution, so no impl was found that causes these two
+            // to overlap
+            Some(Solution::Unique(_)) => true,
+            // Goal was ambiguous, so there *may* be overlap
+            Some(Solution::Ambig(_)) |
+            // Goal cannot be proven, so there is some impl that causes overlap
+            None => false,
+        };
         debug!("overlaps: result = {:?}", result);
         result
     }
diff --git a/src/coherence/test.rs b/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\""
+        }
     }
 }
 
@@ -227,6 +224,39 @@ fn overlapping_negative_impls() {
     }
 }
 
+#[test]
+fn downstream_impl_of_fundamental_43355() {
+    // Regression test for issue 43355 which exposed an unsoundness in the original implementation
+    // with regards to how fundamental types were handled for potential downstream impls. This case
+    // fails exactly the way we want it to using chalk's overlap check rules.
+    // https://github.com/rust-lang/rust/issues/43355
+    lowering_error! {
+        program {
+            #[upstream]
+            #[fundamental]
+            struct Box<T> { }
+
+            trait Trait1<X> { }
+            trait Trait2<X> { }
+
+            struct A { }
+
+            impl<X, T> Trait1<X> for T where T: Trait2<X> { }
+            impl<X> Trait1<Box<X>> for A { }
+
+            // So how do these impls overlap? Consider a downstream crate that adds this code:
+            //
+            //     struct B;
+            //     impl Trait2<Box<B>> for A {}
+            //
+            // This makes the first impl now apply to A, which means that both of these impls now
+            // overlap for A even though they didn't overlap in the original crate where A is defined.
+        } error_msg {
+            "overlapping impls of trait \"Trait1\""
+        }
+    }
+}
+
 #[test]
 fn orphan_check() {
     // These tests are largely adapted from the compile-fail coherence-*.rs tests from rustc
diff --git a/src/rules.rs b/src/rules.rs
@@ -319,6 +319,8 @@ impl StructDatum {
         //
         //    forall<T> { IsLocal(Box<T>) :- IsLocal(T) }
         //    forall<T> { IsUpstream(Box<T>) :- IsUpstream(T) }
+        //    // Generated for both upstream and local fundamental types
+        //    forall<T> { DownstreamType(Box<T>) :- DownstreamType(T) }
 
         let wf = self.binders.map_ref(|bound_datum| {
             ProgramClauseImplication {
@@ -343,6 +345,32 @@ impl StructDatum {
 
         let mut clauses = vec![wf, is_fully_visible];
 
+        // Fundamental types often have rules in the form of:
+        //     Goal(FundamentalType<T>) :- Goal(T)
+        // This macro makes creating that kind of clause easy
+        macro_rules! fundamental_rule {
+            ($goal:ident) => {
+                // Fundamental types must always have at least one type parameter for this rule to
+                // make any sense. We currently do not have have any fundamental types with more than
+                // one type parameter, nor do we know what the behaviour for that should be. Thus, we
+                // are asserting here that there is only a single type parameter until the day when
+                // someone makes a decision about how that should behave.
+                assert_eq!(self.binders.value.self_ty.len_type_parameters(), 1,
+                    "Only fundamental types with a single parameter are supported");
+
+                clauses.push(self.binders.map_ref(|bound_datum| ProgramClauseImplication {
+                    consequence: DomainGoal::$goal(bound_datum.self_ty.clone().cast()),
+                    conditions: vec![
+                    DomainGoal::$goal(
+                        // This unwrap is safe because we asserted above for the presence of a type
+                        // parameter
+                        bound_datum.self_ty.first_type_parameter().unwrap()
+                    ).cast(),
+                    ],
+                }).cast());
+            };
+        }
+
         // Types that are not marked `#[upstream]` satisfy IsLocal(TypeName)
         if !self.binders.value.flags.upstream {
             // `IsLocalTy(Ty)` depends *only* on whether the type is marked #[upstream] and nothing else
@@ -355,33 +383,6 @@ impl StructDatum {
         } else if self.binders.value.flags.fundamental {
             // If a type is `#[upstream]`, but is also `#[fundamental]`, it satisfies IsLocal
             // if and only if its parameters satisfy IsLocal
-
-            // Fundamental types must always have at least one type parameter for this rule to
-            // make any sense. We currently do not have have any fundamental types with more than
-            // one type parameter, nor do we know what the behaviour for that should be. Thus, we
-            // are asserting here that there is only a single type parameter until the day when
-            // someone makes a decision about how that should behave.
-            assert_eq!(self.binders.value.self_ty.len_type_parameters(), 1,
-                "Only fundamental types with a single parameter are supported");
-
-            // Fundamental types often have rules in the form of:
-            //     Goal(FundamentalType<T>) :- Goal(T)
-            // This macro makes creating that kind of clause easy
-            macro_rules! fundamental_rule {
-                ($goal:ident) => {
-                    clauses.push(self.binders.map_ref(|bound_datum| ProgramClauseImplication {
-                        consequence: DomainGoal::$goal(bound_datum.self_ty.clone().cast()),
-                        conditions: vec![
-                        DomainGoal::$goal(
-                            // This unwrap is safe because we asserted above for the presence of a type
-                            // parameter
-                            bound_datum.self_ty.first_type_parameter().unwrap()
-                        ).cast(),
-                        ],
-                    }).cast());
-                };
-            }
-
             fundamental_rule!(IsLocal);
             fundamental_rule!(IsUpstream);
         } else {
@@ -395,6 +396,10 @@ impl StructDatum {
             clauses.push(is_upstream);
         }
 
+        if self.binders.value.flags.fundamental {
+            fundamental_rule!(DownstreamType);
+        }
+
         let condition = DomainGoal::FromEnv(
             FromEnv::Ty(self.binders.value.self_ty.clone().cast())
         );
@@ -481,6 +486,25 @@ impl TraitDatum {
         //          IsFullyVisible(U),
         //          IsLocal(V)
         //    }
+        //
+        // The overlap check uses compatible { ... } mode to ensure that it accounts for impls that
+        // may exist in some other *compatible* world. For every upstream trait, we add a rule to
+        // account for the fact that upstream crates are able to compatibly add impls of upstream
+        // traits for upstream types.
+        //
+        //     // For `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }`
+        //     forall<Self, T, U, V> {
+        //         Implemented(Self: Foo<T, U, V>) :-
+        //             Implemented(Self: Eq<T>), // where clauses
+        //             Compatible,               // compatible modality
+        //             IsUpstream(Self),
+        //             IsUpstream(T),
+        //             IsUpstream(U),
+        //             IsUpstream(V),
+        //             CannotProve,              // returns ambiguous
+        //     }
+
+        let mut clauses = Vec::new();
 
         let trait_ref = self.binders.value.trait_ref.clone();
 
@@ -503,8 +527,32 @@ impl TraitDatum {
                 },
             }
         }).cast();
+        clauses.push(wf);
+
+        // The number of parameters will always be at least 1 because of the Self parameter
+        // that is automatically added to every trait. This is important because otherwise
+        // the added program clauses would not have any conditions.
+        let type_parameters: Vec<_> = self.binders.value.trait_ref.type_parameters().collect();
+
+        // Add all cases for potential downstream impls that could exist
+        for i in 0..type_parameters.len() {
+            let impl_may_exist = self.binders.map_ref(|bound_datum|
+                ProgramClauseImplication {
+                    consequence: DomainGoal::Holds(WhereClause::Implemented(bound_datum.trait_ref.clone())),
+                    conditions: bound_datum.where_clauses
+                        .iter()
+                        .cloned()
+                        .casted()
+                        .chain(iter::once(DomainGoal::Compatible(()).cast()))
+                        .chain((0..i).map(|j| DomainGoal::IsFullyVisible(type_parameters[j].clone()).cast()))
+                        .chain(iter::once(DomainGoal::DownstreamType(type_parameters[i].clone()).cast()))
+                        .chain(iter::once(Goal::CannotProve(())))
+                        .collect(),
+                }
+            ).cast();
 
-        let mut clauses = vec![wf];
+            clauses.push(impl_may_exist);
+        }
 
         if !self.binders.value.flags.upstream {
             let impl_allowed = self.binders.map_ref(|bound_datum|
@@ -516,12 +564,6 @@ impl TraitDatum {
 
             clauses.push(impl_allowed);
         } else {
-            // The number of parameters will always be at least 1 because of the Self parameter
-            // that is automatically added to every trait. This is important because otherwise
-            // the added program clauses would not have any conditions.
-
-            let type_parameters: Vec<_> = self.binders.value.trait_ref.type_parameters().collect();
-
             for i in 0..type_parameters.len() {
                 let impl_maybe_allowed = self.binders.map_ref(|bound_datum|
                     ProgramClauseImplication {
@@ -535,6 +577,20 @@ impl TraitDatum {
 
                 clauses.push(impl_maybe_allowed);
             }
+
+            let impl_may_exist = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
+                consequence: DomainGoal::Holds(WhereClause::Implemented(bound_datum.trait_ref.clone())),
+                conditions: bound_datum.where_clauses
+                    .iter()
+                    .cloned()
+                    .casted()
+                    .chain(iter::once(DomainGoal::Compatible(()).cast()))
+                    .chain(bound_datum.trait_ref.type_parameters().map(|ty| DomainGoal::IsUpstream(ty).cast()))
+                    .chain(iter::once(Goal::CannotProve(())))
+                    .collect(),
+            }).cast();
+
+            clauses.push(impl_may_exist);
         }
 
         let condition = DomainGoal::FromEnv(FromEnv::Trait(trait_ref.clone()));
diff --git a/src/solve/slg/test.rs b/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)
                             )
                         }
                     }
diff --git a/src/solve/test.rs b/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! {

Original file line number	Diff line number	Diff line change
`@@ -744,10 +744,10 @@ fn example_3_3_EWFS() {`
`744`	`744`	`delayed_literals: DelayedLiteralSet {`
`745`	`745`	`delayed_literals: {`
`746`	`746`	`Negative(`
`747`		`- TableIndex(4)`
	`747`	`+ TableIndex(1)`
`748`	`748`	`),`
`749`	`749`	`Negative(`
`750`		`- TableIndex(1)`
	`750`	`+ TableIndex(6)`
`751`	`751`	`)`
`752`	`752`	`}`
`753`	`753`	`}`