Revert parts of "add comments"

I didn't mean to push these changes.

This reverts commit 75ae1aa.

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -46,7 +46,11 @@ impl Check<'_> {
         let a = env.instantiate_universally(&impl_a.binder);
         let trait_ref = a.trait_ref();
 
-        self.prove_is_local_trait_ref(&env.with_coherence_mode(true), &a.where_clauses, trait_ref)
+        self.prove_goal(
+            &env.with_coherence_mode(true),
+            &a.where_clauses,
+            trait_ref.is_local(),
+        )
     }
 
     #[tracing::instrument(level = "Debug", skip(self))]

crates/formality-check/src/lib.rs

@@ -8,10 +8,7 @@ use formality_rust::{
     grammar::{Crate, CrateItem, Program},
     prove::ToWcs,
 };
-use formality_types::{
-    cast::Upcast,
-    grammar::{Fallible, Substitution, TraitRef, 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.
@@ -101,27 +98,7 @@ impl Check<'_> {
             return Ok(());
         }
 
-        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:?}")
+        bail!("failed to prove {goal:?} 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,7 +6,6 @@ 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,4 +1,3 @@
-mod combinators;
 mod constraints;
 mod env;
 mod is_local;
@@ -9,6 +8,7 @@ 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,8 +19,6 @@ 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 = prove_is_local_trait_ref(decls, &env, assumptions, goal);
+    let c = 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 prove_is_local_trait_ref(
+    pub fn 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")
-            (prove_is_local_trait_ref(decls, env, _assumptions, goal) => Constraints::none(env))
+            (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")
-            (prove_is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2))
+            (is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2))
         )
     }
 }

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

@@ -6,7 +6,11 @@ use formality_types::{
 use crate::{
     decls::Decls,
     prove::{
-        env::Env, is_local::may_be_remote, prove, prove_after::prove_after, prove_eq::prove_eq,
+        env::Env,
+        is_local::{is_local_trait_ref, may_be_remote},
+        prove,
+        prove_after::prove_after,
+        prove_eq::prove_eq,
         prove_via::prove_via,
     },
 };
@@ -96,5 +100,11 @@ 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,13 +3,12 @@ use std::sync::Arc;
 use formality_macros::term;
 use formality_types::{
     collections::Set,
-    grammar::{Binder, TraitRef, Wcs},
+    grammar::{Binder, Wcs},
 };
 
 use crate::{
     decls::Decls,
     prove::{prove, Constraints, Env},
-    prove_is_local_trait_ref,
 };
 
 mod eq_assumptions;
@@ -32,8 +31,6 @@ 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).
@@ -63,10 +60,6 @@ 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,6 +24,9 @@ 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.
@@ -75,6 +78,7 @@ pub enum Skeleton {
     NotImplemented(TraitId),
     WellFormed,
     WellFormedTraitRef(TraitId),
+    IsLocal(TraitId),
 
     Equals,
     Sub,
@@ -107,6 +111,10 @@ impl Predicate {
                 Skeleton::WellFormedTraitRef(trait_id.clone()),
                 parameters.clone(),
             ),
+            Predicate::IsLocal(TraitRef {
+                trait_id,
+                parameters,
+            }) => (Skeleton::IsLocal(trait_id.clone()), parameters.clone()),
         }
     }
 }
@@ -119,6 +127,10 @@ 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 CoreTrait((rigid (adt CoreStruct))) is local, given {}; got {}",
+                source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}",
             },
         )
     "#]]