add comments

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -46,24 +46,31 @@ impl Check<'_> {
         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(),
-        )
+        self.prove_is_local_trait_ref(&env.with_coherence_mode(true), &a.where_clauses, trait_ref)
     }
 
     #[tracing::instrument(level = "Debug", skip(self))]
     fn overlap_check(&self, impl_a: &TraitImpl, impl_b: &TraitImpl) -> Fallible<()> {
         let mut env = Env::default();
 
+        // Example:
+        //
+        // Given two impls...
+        //
+        //   impl<P_a..> SomeTrait<T_a...> for T_a0 where Wc_a { }
+        //   impl<P_b..> SomeTrait<T_b...> for T_b0 where Wc_b { }
+
+        // ∀P_a, ∀P_b....
         let a = env.instantiate_universally(&impl_a.binder);
         let b = env.instantiate_universally(&impl_b.binder);
 
+        // ...get the trait refs from each impl...
         let trait_ref_a = a.trait_ref();
         let trait_ref_b = b.trait_ref();
 
         // If the parameters from the two impls cannot be equal, then they do not overlap.
+        //
+        // If we can prove `∀P_a, ∀P_b. not (T_a = T_b, Wc_a, Wc_b)`, then they do not overlap.
         if let Ok(()) = self.prove_not_goal(
             &env.with_coherence_mode(true),
             (&a.where_clauses, &b.where_clauses),
@@ -73,6 +80,8 @@ impl Check<'_> {
         }
 
         // If we can disprove the where clauses, then they do not overlap.
+        //
+        // If we can prove `∀P_a, ∀P_b. not [(T_a = T_b) => (Wc_a, Wc_b)]`, then they do not overlap.
         if let Ok(()) = self.prove_not_goal(
             &env.with_coherence_mode(true),
             Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
@@ -82,6 +91,11 @@ impl Check<'_> {
         }
 
         // If we can disprove the where clauses, then they do not overlap.
+        //
+        // Given some inverted where-clause Wc_i from (invert(Wc_a), invert(Wc_b))...e.g.
+        // if `T: Debug` is in `Wc_a`, then `Wc_i` might be `T: !Debug`.
+        //
+        // If we can prove `∀P_a, ∀P_b, (T_a = T_b, Wc_a, Wc_b) => Wc_i`, then contradiction, no overlap.
         let inverted: Vec<Wc> = a
             .where_clauses
             .iter()

crates/formality-check/src/lib.rs

@@ -8,7 +8,10 @@ use formality_rust::{
     grammar::{Crate, CrateItem, Program},
     prove::ToWcs,
 };
-use formality_types::grammar::{Fallible, Substitution, Wcs};
+use formality_types::{
+    cast::Upcast,
+    grammar::{Fallible, Substitution, TraitRef, 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.
@@ -98,7 +101,27 @@ impl Check<'_> {
             return Ok(());
         }
 
-        bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
+        bail!("failed to prove {goal:?} given {assumptions:?}; got {cs:?}")
+    }
+
+    fn prove_is_local_trait_ref(
+        &self,
+        env: &Env,
+        assumptions: impl ToWcs,
+        goal: impl Upcast<TraitRef>,
+    ) -> Fallible<()> {
+        let goal: TraitRef = goal.upcast();
+        let assumptions: Wcs = assumptions.to_wcs();
+
+        assert!(env.only_universal_variables());
+        assert!(env.encloses((&assumptions, &goal)));
+
+        let cs = formality_prove::prove_is_local_trait_ref(self.decls, env, &assumptions, &goal);
+        if cs.iter().any(|c| c.unconditionally_true()) {
+            return Ok(());
+        }
+
+        bail!("failed to prove {goal:?} is local, given {assumptions:?}; got {cs:?}")
     }
 
     fn prove_not_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {

crates/formality-prove/src/lib.rs

@@ -6,6 +6,7 @@ mod prove;
 
 pub use decls::*;
 pub use prove::prove;
+pub use prove::prove_is_local_trait_ref;
 pub use prove::Env;
 
 #[cfg(test)]

crates/formality-prove/src/prove.rs

@@ -1,3 +1,4 @@
+mod combinators;
 mod constraints;
 mod env;
 mod is_local;
@@ -8,7 +9,6 @@ mod prove_normalize;
 mod prove_via;
 mod prove_wc;
 mod prove_wc_list;
-mod combinators;
 
 pub use constraints::Constraints;
 use formality_types::{cast::Upcast, collections::Set, grammar::Wcs, set, visit::Visit};
@@ -19,6 +19,8 @@ use crate::decls::Decls;
 pub use self::env::Env;
 use self::prove_wc_list::prove_wc_list;
 
+pub use is_local::prove_is_local_trait_ref;
+
 /// Top-level entry point for proving things; other rules recurse to this one.
 pub fn prove(
     decls: impl Upcast<Decls>,

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

@@ -42,7 +42,7 @@ use crate::{
 pub fn may_be_remote(decls: Decls, env: Env, assumptions: Wcs, goal: TraitRef) -> Set<Constraints> {
     assert!(env.is_in_coherence_mode());
 
-    let c = is_local_trait_ref(decls, &env, assumptions, goal);
+    let c = prove_is_local_trait_ref(decls, &env, assumptions, goal);
 
     if c.is_empty() {
         // Cannot possibly be local, so always remote.
@@ -59,7 +59,7 @@ pub fn may_be_remote(decls: Decls, env: Env, assumptions: Wcs, goal: TraitRef) -
 }
 
 judgment_fn! {
-    pub fn is_local_trait_ref(
+    pub fn prove_is_local_trait_ref(
         decls: Decls,
         env: Env,
         assumptions: Wcs,
@@ -70,7 +70,7 @@ judgment_fn! {
         (
             (if decls.is_local_trait_id(&goal.trait_id))
             --- ("local trait")
-            (is_local_trait_ref(decls, env, _assumptions, goal) => Constraints::none(env))
+            (prove_is_local_trait_ref(decls, env, _assumptions, goal) => Constraints::none(env))
         )
 
         (
@@ -80,7 +80,7 @@ judgment_fn! {
             (let goal = c1.substitution().apply(&goal))
             (for_all(&decls, &env, &assumptions, &goal.parameters[..i], &not_downstream) => c2)
             --- ("local parameter")
-            (is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2))
+            (prove_is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2))
         )
     }
 }

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

@@ -6,11 +6,7 @@ use formality_types::{
 use crate::{
     decls::Decls,
     prove::{
-        env::Env,
-        is_local::{is_local_trait_ref, may_be_remote},
-        prove,
-        prove_after::prove_after,
-        prove_eq::prove_eq,
+        env::Env, is_local::may_be_remote, prove, prove_after::prove_after, prove_eq::prove_eq,
         prove_via::prove_via,
     },
 };
@@ -100,11 +96,5 @@ judgment_fn! {
             ----------------------------- ("trait well formed")
             (prove_wc(decls, env, assumptions, Predicate::WellFormedTraitRef(trait_ref)) => c)
         )
-
-        (
-            (is_local_trait_ref(decls, env, assumptions, trait_ref) => c)
-            ----------------------------- ("trait ref is local")
-            (prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c)
-        )
     }
 }

crates/formality-prove/src/test.rs

@@ -3,12 +3,13 @@ use std::sync::Arc;
 use formality_macros::term;
 use formality_types::{
     collections::Set,
-    grammar::{Binder, Wcs},
+    grammar::{Binder, TraitRef, Wcs},
 };
 
 use crate::{
     decls::Decls,
     prove::{prove, Constraints, Env},
+    prove_is_local_trait_ref,
 };
 
 mod eq_assumptions;
@@ -31,6 +32,8 @@ enum TestAssertion {
     Exists(Binder<Arc<TestAssertion>>),
     #[grammar($v0 => $v1)]
     Prove(Wcs, Wcs),
+    #[grammar($v0 => @IsLocal($v1))]
+    IsLocal(Wcs, TraitRef),
 }
 
 /// `t` represents some set of existential bindings combined with (assumptions, goals).
@@ -60,6 +63,10 @@ fn test_prove(decls: Decls, mut assertion: Arc<TestAssertion>) -> Set<Constraint
                 return prove(decls, env, assumptions, goals);
             }
 
+            TestAssertion::IsLocal(assumptions, goal) => {
+                return prove_is_local_trait_ref(decls, env, assumptions, goal);
+            }
+
             TestAssertion::CoherenceMode(assertion1) => {
                 env = env.with_coherence_mode(true);
                 assertion = assertion1.clone();

crates/formality-types/src/grammar/formulas.rs

@@ -24,9 +24,6 @@ pub enum Predicate {
 
     #[grammar(@WellFormedTraitRef($v0))]
     WellFormedTraitRef(TraitRef),
-
-    #[grammar(@IsLocal($v0))]
-    IsLocal(TraitRef),
 }
 
 /// A coinductive predicate is one that can be proven via a cycle.
@@ -78,7 +75,6 @@ pub enum Skeleton {
     NotImplemented(TraitId),
     WellFormed,
     WellFormedTraitRef(TraitId),
-    IsLocal(TraitId),
 
     Equals,
     Sub,
@@ -111,10 +107,6 @@ impl Predicate {
                 Skeleton::WellFormedTraitRef(trait_id.clone()),
                 parameters.clone(),
             ),
-            Predicate::IsLocal(TraitRef {
-                trait_id,
-                parameters,
-            }) => (Skeleton::IsLocal(trait_id.clone()), parameters.clone()),
         }
     }
 }
@@ -127,10 +119,6 @@ impl TraitRef {
     pub fn well_formed(&self) -> Predicate {
         Predicate::WellFormedTraitRef(self.clone())
     }
-
-    pub fn is_local(&self) -> Predicate {
-        Predicate::IsLocal(self.clone())
-    }
 }
 
 /// Relations are built-in goals which are implemented in custom Rust logic.

tests/coherence.rs

@@ -183,7 +183,7 @@ fn test_orphan_basic() {
         Err(
             Error {
                 context: "orphan_check(impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })",
-                source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}",
+                source: "failed to prove CoreTrait((rigid (adt CoreStruct))) is local, given {}; got {}",
             },
         )
     "#]]