Merge pull request #123 from nikomatsakis/negative-trait-impls

Negative trait impls

Author: nikomatsakis

Cargo.lock

@@ -11,6 +11,8 @@ rustc_private=true
 [dev-dependencies]
 pretty_assertions = "1.3.0"
 expect-test = "1.4.0"
+formality-macros = { version = "0.1.0", path = "crates/formality-macros" }
+formality-core = { version = "0.1.0", path = "crates/formality-core" }
 
 [dependencies]
 anyhow = "1"

Cargo.toml

@@ -1,4 +1,5 @@
 use anyhow::bail;
+use fn_error_context::context;
 use formality_prove::Env;
 use formality_rust::grammar::{Crate, TraitImpl};
 use formality_types::{
@@ -38,10 +39,21 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn orphan_check(&self, _impl_a: &TraitImpl) -> Fallible<()> {
-        Ok(())
+    #[context("orphan_check({impl_a:?})")]
+    fn orphan_check(&self, impl_a: &TraitImpl) -> Fallible<()> {
+        let mut env = Env::default();
+
+        let a = env.instantiate_universally(&impl_a.binder);
+        let trait_ref = a.trait_ref();
+
+        self.prove_goal(
+            &env.with_coherence_mode(true),
+            &a.where_clauses,
+            trait_ref.is_local(),
+        )
     }
 
+    #[tracing::instrument(level = "Debug", skip(self))]
     fn overlap_check(&self, impl_a: &TraitImpl, impl_b: &TraitImpl) -> Fallible<()> {
         let mut env = Env::default();
 
@@ -53,7 +65,7 @@ impl Check<'_> {
 
         // If the parameters from the two impls cannot be equal, then they do not overlap.
         if let Ok(()) = self.prove_not_goal(
-            &env,
+            &env.with_coherence_mode(true),
             (&a.where_clauses, &b.where_clauses),
             Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
         ) {
@@ -62,7 +74,7 @@ impl Check<'_> {
 
         // If we can disprove the where clauses, then they do not overlap.
         if let Ok(()) = self.prove_not_goal(
-            &env,
+            &env.with_coherence_mode(true),
             Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
             (&a.where_clauses, &b.where_clauses),
         ) {

crates/formality-check/src/coherence.rs

@@ -35,6 +35,8 @@ impl super::Check<'_> {
 
         self.prove_goal(&env, &where_clauses, trait_ref.is_implemented())?;
 
+        self.prove_not_goal(&env, &where_clauses, trait_ref.not_implemented())?;
+
         let trait_decl = self.program.trait_named(&trait_ref.trait_id)?;
         let TraitBoundData {
             where_clauses: _,

crates/formality-check/src/impls.rs

@@ -114,7 +114,7 @@ impl Check<'_> {
         // we've proven the negation. (This is called the "negation as failure" property,
         // and it relies on our solver being complete -- i.e., if there is a solution,
         // we'll find it, or at least return ambiguous.)
-        let mut existential_env = Env::default();
+        let mut existential_env = Env::default().with_coherence_mode(env.is_in_coherence_mode());
         let universal_to_existential: Substitution = env
             .variables()
             .iter()

crates/formality-check/src/lib.rs

@@ -3,9 +3,10 @@ use formality_types::{
     cast::Upcast,
     collections::Set,
     grammar::{
-        AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs,
-        PR,
+        AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty,
+        Wc, Wcs, PR,
     },
+    set,
 };
 
 #[term]
@@ -16,12 +17,22 @@ pub struct Decls {
     pub neg_impl_decls: Vec<NegImplDecl>,
     pub alias_eq_decls: Vec<AliasEqDecl>,
     pub alias_bound_decls: Vec<AliasBoundDecl>,
+    pub local_trait_ids: Set<TraitId>,
+    pub local_adt_ids: Set<AdtId>,
 }
 
 impl Decls {
     /// Max size used in unit tests that are not stress testing maximum size.
     pub const DEFAULT_MAX_SIZE: usize = 222;
 
+    pub fn is_local_trait_id(&self, trait_id: &TraitId) -> bool {
+        self.local_trait_ids.contains(trait_id)
+    }
+
+    pub fn is_local_adt_id(&self, adt_id: &AdtId) -> bool {
+        self.local_adt_ids.contains(adt_id)
+    }
+
     pub fn impl_decls<'s>(&'s self, trait_id: &'s TraitId) -> impl Iterator<Item = &'s ImplDecl> {
         self.impl_decls
             .iter()
@@ -78,6 +89,8 @@ impl Decls {
             neg_impl_decls: vec![],
             alias_eq_decls: vec![],
             alias_bound_decls: vec![],
+            local_trait_ids: set![],
+            local_adt_ids: set![],
         }
     }
 }

crates/formality-prove/src/decls.rs

@@ -1,13 +1,14 @@
 mod constraints;
 mod env;
+mod is_local;
 mod minimize;
 mod prove_after;
 mod prove_eq;
 mod prove_normalize;
 mod prove_via;
 mod prove_wc;
 mod prove_wc_list;
-mod zip;
+mod combinators;
 
 pub use constraints::Constraints;
 use formality_types::{cast::Upcast, collections::Set, grammar::Wcs, set, visit::Visit};

crates/formality-prove/src/prove.rs

@@ -37,3 +37,32 @@ where
         })
         .collect()
 }
+
+pub fn for_all<A, C>(
+    decls: &Decls,
+    env: &Env,
+    context: &C,
+    a: &[A],
+    op: &impl Fn(Decls, Env, C, A) -> Set<Constraints>,
+) -> Set<Constraints>
+where
+    A: Term,
+    C: Term,
+{
+    if a.is_empty() {
+        return set![Constraints::none(env.upcast())];
+    }
+
+    let a0 = a[0].clone();
+    let a_remaining: Vec<A> = a[1..].to_vec();
+    op(decls.clone(), env.clone(), context.clone(), a0)
+        .into_iter()
+        .flat_map(|c1| {
+            let context = c1.substitution().apply(context);
+            let a_remaining = c1.substitution().apply(&a_remaining);
+            for_all(&decls, c1.env(), &context, &a_remaining, op)
+                .into_iter()
+                .map(move |c2| c1.seq(c2))
+        })
+        .collect()
+}

crates/formality-prove/src/prove/zip.rs renamed to crates/formality-prove/src/prove/combinators.rs

@@ -33,6 +33,13 @@ impl Constraints {
         Self::from(env, v)
     }
 
+    pub fn with_coherence_mode(self, b: bool) -> Self {
+        Self {
+            env: self.env.with_coherence_mode(b),
+            ..self
+        }
+    }
+
     pub fn unconditionally_true(&self) -> bool {
         self.known_true && self.substitution.is_empty()
     }

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

@@ -13,12 +13,24 @@ use formality_types::{
 #[derive(Default, Debug, Clone, Hash, Ord, Eq, PartialEq, PartialOrd)]
 pub struct Env {
     variables: Vec<Variable>,
+    coherence_mode: bool,
 }
 
 impl Env {
     pub fn only_universal_variables(&self) -> bool {
         self.variables.iter().all(|v| v.is_universal())
     }
+
+    pub fn is_in_coherence_mode(&self) -> bool {
+        self.coherence_mode
+    }
+
+    pub fn with_coherence_mode(&self, b: bool) -> Env {
+        Env {
+            coherence_mode: b,
+            ..self.clone()
+        }
+    }
 }
 
 cast_impl!(Env);
@@ -199,6 +211,7 @@ impl Env {
                 .iter()
                 .map(|&v| vs.map_var(v).unwrap_or(v))
                 .collect(),
+            coherence_mode: self.coherence_mode,
         }
     }