add negative trait impls

nikomatsakis · nikomatsakis · commit 9a3f6c602a0c · 2023-03-14T12:12:45.000-04:00
diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
@@ -4,7 +4,8 @@ use fn_error_context::context;
 use formality_prove::Env;
 use formality_rust::grammar::{
     AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Fn,
-    FnBoundData, ImplItem, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem, WhereClause,
+    FnBoundData, ImplItem, NegTraitImpl, NegTraitImplBoundData, TraitBoundData, TraitImpl,
+    TraitImplBoundData, TraitItem, WhereClause,
 };
 use formality_types::{
     cast::Downcasted,
@@ -47,6 +48,25 @@ impl super::Check<'_> {
         Ok(())
     }
 
+    pub(super) fn check_neg_trait_impl(&self, i: &NegTraitImpl) -> Fallible<()> {
+        let mut env = Env::default();
+
+        let NegTraitImplBoundData {
+            trait_id,
+            self_ty,
+            trait_parameters,
+            where_clauses,
+        } = env.instantiate_universally(&i.binder);
+
+        let trait_ref = trait_id.with(self_ty, trait_parameters);
+
+        self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
+
+        self.prove_goal(&env, &where_clauses, trait_ref.not_implemented())?;
+
+        Ok(())
+    }
+
     #[requires(assumptions.iter().all(|a| a.references_only_placeholder_variables()))]
     fn check_trait_impl_item(
         &self,
diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs
@@ -85,6 +85,7 @@ impl Check<'_> {
             CrateItem::Struct(s) => self.check_adt(&s.to_adt()),
             CrateItem::Enum(e) => self.check_adt(&e.to_adt()),
             CrateItem::Fn(f) => self.check_free_fn(f),
+            CrateItem::NegTraitImpl(i) => self.check_neg_trait_impl(i),
         }
     }
 
diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs
@@ -13,6 +13,7 @@ pub struct Decls {
     pub max_size: usize,
     pub trait_decls: Vec<TraitDecl>,
     pub impl_decls: Vec<ImplDecl>,
+    pub neg_impl_decls: Vec<NegImplDecl>,
     pub alias_eq_decls: Vec<AliasEqDecl>,
     pub alias_bound_decls: Vec<AliasBoundDecl>,
 }
@@ -27,6 +28,15 @@ impl Decls {
             .filter(move |i| i.binder.peek().trait_ref.trait_id == *trait_id)
     }
 
+    pub fn neg_impl_decls<'s>(
+        &'s self,
+        trait_id: &'s TraitId,
+    ) -> impl Iterator<Item = &'s NegImplDecl> {
+        self.neg_impl_decls
+            .iter()
+            .filter(move |i| i.binder.peek().trait_ref.trait_id == *trait_id)
+    }
+
     pub fn trait_decl(&self, trait_id: &TraitId) -> &TraitDecl {
         let mut v: Vec<_> = self
             .trait_decls
@@ -65,6 +75,7 @@ impl Decls {
             max_size: Decls::DEFAULT_MAX_SIZE,
             trait_decls: vec![],
             impl_decls: vec![],
+            neg_impl_decls: vec![],
             alias_eq_decls: vec![],
             alias_bound_decls: vec![],
         }
@@ -82,6 +93,17 @@ pub struct ImplDeclBoundData {
     pub where_clause: Wcs,
 }
 
+#[term(impl $binder)]
+pub struct NegImplDecl {
+    pub binder: Binder<NegImplDeclBoundData>,
+}
+
+#[term(!$trait_ref where $where_clause)]
+pub struct NegImplDeclBoundData {
+    pub trait_ref: TraitRef,
+    pub where_clause: Wcs,
+}
+
 #[term(trait $id $binder)]
 pub struct TraitDecl {
     pub id: TraitId,
diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs
@@ -10,14 +10,11 @@ use crate::{decls::Decls, prove::prove};
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
     Decls {
-        max_size: Decls::DEFAULT_MAX_SIZE,
         trait_decls: vec![
             term("trait Eq<ty Self> where {PartialEq(Self)}"),
             term("trait PartialEq<ty Self> where {}"),
         ],
-        impl_decls: vec![],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
+        ..Decls::empty()
     }
 }
 
diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs
@@ -9,11 +9,9 @@ use super::test_prove;
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
     Decls {
-        max_size: Decls::DEFAULT_MAX_SIZE,
         trait_decls: vec![term("trait Foo<ty Self> where {}")],
         impl_decls: vec![term("impl<ty T> Foo(Vec<T>) where {}")],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
+        ..Decls::empty()
     }
 }
 
diff --git a/crates/formality-prove/src/test/expanding.rs b/crates/formality-prove/src/test/expanding.rs
@@ -10,8 +10,7 @@ fn decls() -> Decls {
         max_size: 10,
         trait_decls: vec![term("trait Debug<ty Self> where {}")],
         impl_decls: vec![term("impl<ty T> Debug(Vec<T>) where {Debug(T)}")],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
+        ..Decls::empty()
     }
 }
 
diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs
@@ -9,7 +9,6 @@ use super::test_prove;
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
     Decls {
-        max_size: Decls::DEFAULT_MAX_SIZE,
         trait_decls: vec![
             term("trait Copy<ty Self> where {}"),
             term("trait Magic<ty Self> where {Copy(Self)}"),
@@ -18,8 +17,7 @@ fn decls() -> Decls {
             term("impl<ty T> Magic(T) where {Magic(T)}"),
             term("impl<> Copy(u32) where {}"),
         ],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
+        ..Decls::empty()
     }
 }
 
diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs
@@ -9,11 +9,9 @@ use super::test_prove;
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
     Decls {
-        max_size: Decls::DEFAULT_MAX_SIZE,
         trait_decls: vec![term("trait Foo<ty Self> where {}")],
         impl_decls: vec![term("impl<ty T> Foo(Vec<T>) where {}")],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
+        ..Decls::empty()
     }
 }
 
diff --git a/crates/formality-prove/src/test/simple_impl.rs b/crates/formality-prove/src/test/simple_impl.rs
@@ -7,14 +7,12 @@ use crate::{decls::Decls, prove::prove};
 /// Simple example decls consisting only of two trait declarations.
 fn decls() -> Decls {
     Decls {
-        max_size: Decls::DEFAULT_MAX_SIZE,
         trait_decls: vec![term("trait Debug<ty Self> where {}")],
         impl_decls: vec![
             term("impl<ty T> Debug(Vec<T>) where {Debug(T)}"),
             term("impl<> Debug(u32) where {}"),
         ],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
+        ..Decls::empty()
     }
 }
 
diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs
@@ -19,11 +19,9 @@ fn exists_u_for_t() {
 #[test]
 fn for_t_exists_u() {
     let decls = Decls {
-        max_size: Decls::DEFAULT_MAX_SIZE,
         trait_decls: vec![term("trait Test<ty Self, ty T> where {}")],
         impl_decls: vec![term("impl<ty X, ty Y> Test(X, Y) where {X = Y}")],
-        alias_eq_decls: vec![],
-        alias_bound_decls: vec![],
+        ..Decls::empty()
     };
 
     let constraints = super::test_prove(decls, term("{} => {for<ty T> Test(T, T)}"));
diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs
@@ -61,6 +61,8 @@ pub enum CrateItem {
     #[cast]
     TraitImpl(TraitImpl),
     #[cast]
+    NegTraitImpl(NegTraitImpl),
+    #[cast]
     Fn(Fn),
 }
 
@@ -260,6 +262,19 @@ impl TraitImplBoundData {
     }
 }
 
+#[term(impl $binder)]
+pub struct NegTraitImpl {
+    pub binder: Binder<NegTraitImplBoundData>,
+}
+
+#[term(!$trait_id < $,trait_parameters > for $self_ty where $where_clauses { })]
+pub struct NegTraitImplBoundData {
+    pub trait_id: TraitId,
+    pub self_ty: Ty,
+    pub trait_parameters: Vec<Parameter>,
+    pub where_clauses: Vec<WhereClause>,
+}
+
 #[term]
 pub enum ImplItem {
     #[cast]
diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs
@@ -1,7 +1,8 @@
 use crate::grammar::{
     AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Crate,
-    CrateItem, ImplItem, Program, Trait, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem,
-    WhereBound, WhereBoundData, WhereClause, WhereClauseData,
+    CrateItem, ImplItem, NegTraitImpl, NegTraitImplBoundData, Program, Trait, TraitBoundData,
+    TraitImpl, TraitImplBoundData, TraitItem, WhereBound, WhereBoundData, WhereClause,
+    WhereClauseData,
 };
 use formality_prove as prove;
 use formality_types::{
@@ -18,6 +19,7 @@ impl Program {
             max_size: formality_prove::Decls::DEFAULT_MAX_SIZE,
             trait_decls: self.trait_decls(),
             impl_decls: self.impl_decls(),
+            neg_impl_decls: self.neg_impl_decls(),
             alias_eq_decls: self.alias_eq_decls(),
             alias_bound_decls: self.alias_bound_decls(),
         }
@@ -31,6 +33,13 @@ impl Program {
         self.crates.iter().flat_map(|c| c.impl_decls()).collect()
     }
 
+    fn neg_impl_decls(&self) -> Vec<prove::NegImplDecl> {
+        self.crates
+            .iter()
+            .flat_map(|c| c.neg_impl_decls())
+            .collect()
+    }
+
     fn alias_eq_decls(&self) -> Vec<prove::AliasEqDecl> {
         self.crates
             .iter()
@@ -72,10 +81,7 @@ impl Crate {
                         ),
                     })
                 }
-                CrateItem::Struct(_)
-                | CrateItem::Enum(_)
-                | CrateItem::TraitImpl(_)
-                | CrateItem::Fn(_) => None,
+                _ => None,
             })
             .collect()
     }
@@ -105,10 +111,36 @@ impl Crate {
                         ),
                     })
                 }
-                CrateItem::Struct(_)
-                | CrateItem::Enum(_)
-                | CrateItem::Trait(_)
-                | CrateItem::Fn(_) => None,
+                _ => None,
+            })
+            .collect()
+    }
+
+    fn neg_impl_decls(&self) -> Vec<prove::NegImplDecl> {
+        self.items
+            .iter()
+            .flat_map(|item| match item {
+                CrateItem::NegTraitImpl(NegTraitImpl { binder }) => {
+                    let (
+                        vars,
+                        NegTraitImplBoundData {
+                            trait_id,
+                            self_ty,
+                            trait_parameters,
+                            where_clauses,
+                        },
+                    ) = binder.open();
+                    Some(prove::NegImplDecl {
+                        binder: Binder::new(
+                            &vars,
+                            prove::NegImplDeclBoundData {
+                                trait_ref: trait_id.with(self_ty, trait_parameters),
+                                where_clause: where_clauses.to_wcs(),
+                            },
+                        ),
+                    })
+                }
+                _ => None,
             })
             .collect()
     }
diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs
@@ -19,6 +19,9 @@ pub enum Predicate {
     #[cast]
     IsImplemented(TraitRef),
 
+    #[grammar(!$v0)]
+    NotImplemented(TraitRef),
+
     #[grammar(@WellFormedTraitRef($v0))]
     WellFormedTraitRef(TraitRef),
 }
@@ -40,6 +43,12 @@ impl std::ops::BitAnd for Coinductive {
     }
 }
 
+impl TraitRef {
+    pub fn not_implemented(self) -> Predicate {
+        Predicate::NotImplemented(self)
+    }
+}
+
 impl Ty {
     pub fn well_formed(&self) -> Relation {
         Relation::WellFormed(self.upcast())
@@ -63,6 +72,7 @@ impl Parameter {
 #[term]
 pub enum Skeleton {
     IsImplemented(TraitId),
+    NotImplemented(TraitId),
     WellFormed,
     WellFormedTraitRef(TraitId),
 
@@ -83,6 +93,13 @@ impl Predicate {
                 Skeleton::IsImplemented(trait_id.clone()),
                 parameters.clone(),
             ),
+            Predicate::NotImplemented(TraitRef {
+                trait_id,
+                parameters,
+            }) => (
+                Skeleton::NotImplemented(trait_id.clone()),
+                parameters.clone(),
+            ),
             Predicate::WellFormedTraitRef(TraitRef {
                 trait_id,
                 parameters,

Original file line number	Diff line number	Diff line change
`@@ -85,6 +85,7 @@ impl Check<'_> {`
`85`	`85`	`CrateItem::Struct(s) => self.check_adt(&s.to_adt()),`
`86`	`86`	`CrateItem::Enum(e) => self.check_adt(&e.to_adt()),`
`87`	`87`	`CrateItem::Fn(f) => self.check_free_fn(f),`
	`88`	`+ CrateItem::NegTraitImpl(i) => self.check_neg_trait_impl(i),`
`88`	`89`	`}`
`89`	`90`	`}`
`90`	`91`
Original file line number	Diff line number	Diff line change
`@@ -9,11 +9,9 @@ use super::test_prove;`
`9`	`9`	`/// Simple example decls consisting only of two trait declarations.`
`10`	`10`	`fn decls() -> Decls {`
`11`	`11`	`Decls {`
`12`		`- max_size: Decls::DEFAULT_MAX_SIZE,`
`13`	`12`	`trait_decls: vec![term("trait Foo<ty Self> where {}")],`
`14`	`13`	`impl_decls: vec![term("impl<ty T> Foo(Vec<T>) where {}")],`
`15`		`- alias_eq_decls: vec![],`
`16`		`- alias_bound_decls: vec![],`
	`14`	`+ ..Decls::empty()`
`17`	`15`	`}`
`18`	`16`	`}`
`19`	`17`
Original file line number	Diff line number	Diff line change
`@@ -10,8 +10,7 @@ fn decls() -> Decls {`
`10`	`10`	`max_size: 10,`
`11`	`11`	`trait_decls: vec![term("trait Debug<ty Self> where {}")],`
`12`	`12`	`impl_decls: vec![term("impl<ty T> Debug(Vec<T>) where {Debug(T)}")],`
`13`		`- alias_eq_decls: vec![],`
`14`		`- alias_bound_decls: vec![],`
	`13`	`+ ..Decls::empty()`
`15`	`14`	`}`
`16`	`15`	`}`
`17`	`16`