add negative impls

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -3,7 +3,7 @@ use formality_prove::Env;
 use formality_rust::grammar::{Crate, TraitImpl};
 use formality_types::{
     cast::Downcasted,
-    grammar::{Fallible, Wcs},
+    grammar::{Fallible, Wc, Wcs},
 };
 use itertools::Itertools;
 
@@ -69,6 +69,27 @@ impl Check<'_> {
             return Ok(());
         }
 
+        // If we can disprove the where clauses, then they do not overlap.
+        let inverted: Vec<Wc> = a
+            .where_clauses
+            .iter()
+            .chain(&b.where_clauses)
+            .flat_map(|wc| wc.invert())
+            .collect();
+        if inverted.iter().any(|inverted_wc| {
+            self.prove_goal(
+                &env,
+                (
+                    Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+                    &a.where_clauses,
+                    &b.where_clauses,
+                ),
+                inverted_wc,
+            )
+            .is_ok()
+        }) {
+            return Ok(());
+        }
         bail!("impls may overlap: `{impl_a:?}` vs `{impl_b:?}`")
     }
 }

crates/formality-check/src/lib.rs

@@ -5,13 +5,10 @@ use std::collections::VecDeque;
 use anyhow::bail;
 use formality_prove::{Decls, Env};
 use formality_rust::{
-    grammar::{Crate, CrateItem, Program, WhereClause},
+    grammar::{Crate, CrateItem, Program},
     prove::ToWcs,
 };
-use formality_types::{
-    cast::Upcast,
-    grammar::{Fallible, Substitution, Wcs},
-};
+use formality_types::grammar::{Fallible, Substitution, Wcs};
 
 /// Check all crates in the program. The crates must be in dependency order
 /// such that any prefix of the crates is a complete program.
@@ -89,19 +86,14 @@ impl Check<'_> {
         }
     }
 
-    fn prove_goal(
-        &self,
-        env: &Env,
-        assumptions: impl Upcast<Vec<WhereClause>>,
-        goal: impl ToWcs,
-    ) -> Fallible<()> {
+    fn prove_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
-        let assumptions: Vec<WhereClause> = assumptions.upcast();
+        let assumptions: Wcs = assumptions.to_wcs();
 
         assert!(env.only_universal_variables());
         assert!(env.encloses((&assumptions, &goal)));
 
-        let cs = formality_prove::prove(self.decls, env, assumptions.to_wcs(), &goal);
+        let cs = formality_prove::prove(self.decls, env, &assumptions, &goal);
         if cs.iter().any(|c| c.unconditionally_true()) {
             return Ok(());
         }

crates/formality-check/src/where_clauses.rs

@@ -1,5 +1,8 @@
 use formality_prove::Env;
-use formality_rust::grammar::{WhereClause, WhereClauseData};
+use formality_rust::{
+    grammar::{WhereClause, WhereClauseData},
+    prove::ToWcs,
+};
 use formality_types::{
     cast::Upcast,
     grammar::{Fallible, Parameter, TraitRef},
@@ -48,7 +51,7 @@ impl super::Check<'_> {
     fn prove_parameter_well_formed(
         &self,
         env: &Env,
-        assumptions: impl Upcast<Vec<WhereClause>>,
+        assumptions: impl ToWcs,
         parameter: impl Upcast<Parameter>,
     ) -> Fallible<()> {
         let parameter: Parameter = parameter.upcast();
@@ -58,7 +61,7 @@ impl super::Check<'_> {
     fn prove_trait_ref_well_formed(
         &self,
         env: &Env,
-        assumptions: impl Upcast<Vec<WhereClause>>,
+        assumptions: impl ToWcs,
         trait_ref: impl Upcast<TraitRef>,
     ) -> Fallible<()> {
         let trait_ref: TraitRef = trait_ref.upcast();

crates/formality-prove/src/prove/prove_wc.rs

@@ -53,6 +53,16 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
         )
 
+        (
+            (decls.neg_impl_decls(&trait_ref.trait_id) => i)
+            (let (env, subst) = env.existential_substitution(&i.binder))
+            (let i = i.binder.instantiate_with(&subst).unwrap())
+            (prove(&decls, env, &assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
+            (prove_after(&decls, c, &assumptions, &i.where_clause) => c)
+            ----------------------------- ("impl")
+            (prove_wc(decls, env, assumptions, Predicate::NotImplemented(trait_ref)) => c.pop_subst(&subst))
+        )
+
         (
             (decls.trait_invariants() => ti)
             (let (env, subst) = env.existential_substitution(&ti.binder))

crates/formality-rust/src/grammar.rs

@@ -5,7 +5,7 @@ use formality_types::{
     cast::Upcast,
     grammar::{
         AdtId, AssociatedItemId, Binder, CrateId, Fallible, FieldId, FnId, Lt, Parameter, TraitId,
-        TraitRef, Ty,
+        TraitRef, Ty, Wc,
     },
     term::Term,
 };
@@ -304,6 +304,23 @@ impl WhereClause {
     pub fn data(&self) -> &WhereClauseData {
         &self.data
     }
+
+    pub fn invert(&self) -> Option<Wc> {
+        match self.data() {
+            WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => Some(
+                trait_id
+                    .with(self_ty, parameters)
+                    .not_implemented()
+                    .upcast(),
+            ),
+            WhereClauseData::Outlives(_, _) => None,
+            WhereClauseData::ForAll(binder) => {
+                let (vars, where_clause) = binder.open();
+                let wc = where_clause.invert()?;
+                Some(Wc::for_all(&vars, wc))
+            }
+        }
+    }
 }
 
 #[term]

crates/formality-rust/src/prove.rs

@@ -306,6 +306,20 @@ where
     }
 }
 
+impl<A, B, C> ToWcs for (A, B, C)
+where
+    A: ToWcs,
+    B: ToWcs,
+    C: ToWcs,
+{
+    fn to_wcs(&self) -> Wcs {
+        let (a, b, c) = self;
+        let a = a.to_wcs();
+        let b = b.to_wcs();
+        let c = c.to_wcs();
+        (a, b, c).upcast()
+    }
+}
 impl ToWcs for Vec<WhereClause> {
     fn to_wcs(&self) -> Wcs {
         self.iter().flat_map(|wc| wc.to_wcs()).collect()

tests/hello_world.rs

@@ -26,7 +26,7 @@ fn test_broken() {
         Err(
             Error {
                 context: "check_trait(Foo)",
-                source: "failed to prove {@ WellFormedTraitRef(Bar(!ty_2, !ty_1))} given [!ty_2 : Bar < !ty_1 >], got {}",
+                source: "failed to prove {@ WellFormedTraitRef(Bar(!ty_2, !ty_1))} given {Bar(!ty_2, !ty_1)}, got {}",
             },
         )
     "#]].assert_debug_eq(&test_program_ok(PROGRAM_BROKEN));