cleanup and fix coherence rules

Cargo.toml

@@ -30,7 +30,7 @@ formality-check = { version = "0.1.0", path = "crates/formality-check" }
 formality-prove = { version = "0.1.0", path = "crates/formality-prove" }
 formality-core = { version = "0.1.0", path = "crates/formality-core" }
 formality-smir = { version = "0.1.0", path = "crates/formality-smir" }
-ui_test = "0.12"
+expect-test = "1.4.0"
 
 [workspace]
 members = [
@@ -42,7 +42,3 @@ members = [
     "crates/formality-prove",
     "crates/formality-smir",
 ]
-
-[[test]]
-name = "ui"
-harness = false

crates/formality-check/src/coherence.rs

@@ -24,7 +24,9 @@ impl Check<'_> {
             self.orphan_check_neg(impl_a)?;
         }
 
-        // check for duplicate impls in the current crate
+        // check for duplicate impls in the current crate;
+        // the cartesian product below would otherwise consider every impl I
+        // as overlapping with itself.
         for (impl_a, i) in current_crate_impls.iter().zip(0..) {
             if current_crate_impls[i + 1..].contains(impl_a) {
                 bail!("duplicate impl in current crate: {:?}", impl_a)

crates/formality-check/src/lib.rs

@@ -107,6 +107,7 @@ impl Check<'_> {
         bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
     }
 
+    #[tracing::instrument(level = "Debug", skip(self, assumptions, goal))]
     fn prove_not_goal(
         &self,
         env: &Env,
@@ -116,6 +117,9 @@ impl Check<'_> {
         let goal: Wcs = goal.to_wcs();
         let assumptions: Wcs = assumptions.to_wcs();
 
+        tracing::debug!("assumptions = {assumptions:?}");
+        tracing::debug!("goal = {goal:?}");
+
         assert!(env.only_universal_variables());
         assert!(env.encloses((&assumptions, &goal)));
 
@@ -146,10 +150,16 @@ impl Check<'_> {
             &existential_goal,
         );
 
-        if !cs.is_proven() {
-            return Ok(());
+        match cs.into_set() {
+            Ok(proofs) => {
+                bail!(
+                    "failed to disprove\n    {goal:?}\ngiven\n    {assumptions:?}\ngot\n{proofs:?}"
+                )
+            }
+            Err(err) => {
+                tracing::debug!("Proved not goal, error = {err}");
+                return Ok(());
+            }
         }
-
-        bail!("failed to disprove\n    {goal:?}\ngiven\n    {assumptions:?}\ngot\n{cs:?}")
     }
 }

crates/formality-core/src/judgment/proven_set.rs

@@ -91,7 +91,7 @@ impl<T: Ord + Debug> ProvenSet<T> {
         }
     }
 
-    /// Convert to a non-empty set of proven results (if ok) or an error (otherwise).
+    /// Iterate through all solutions.
     pub fn iter<'a>(&'a self) -> Box<dyn Iterator<Item = &'a T> + 'a> {
         match &self.data {
             Data::Failure(_) => Box::new(std::iter::empty()),

crates/formality-core/src/test_util.rs

@@ -50,9 +50,15 @@ pub trait ResultTestExt<T, E> {
     /// Given a `Fallible<T>` value, assert that its debug representation matches the expected value.
     /// If the result is an error it is propagated through to the return value.
     fn assert_ok(self, expect: expect_test::Expect);
+
     /// Given a `Fallible<T>` value, assert that it is an error with the given string (after normalization).
     /// Returns `Ok(())` if the assertion succeeds, or panics if the assertion fails.
     fn assert_err(self, expect: expect_test::Expect);
+
+    /// Given a `Fallible<T>` value, assert that it is an error with the given string (after normalization).
+    /// Also assert that each of the strings in `must_have` appears somewhere within.
+    /// Returns `Ok(())` if the assertion succeeds, or panics if the assertion fails.
+    fn assert_has_err(self, expect: expect_test::Expect, must_have: &[&str]);
 }
 
 impl<T, E> ResultTestExt<T, E> for Result<T, E>
@@ -74,10 +80,21 @@ where
 
     #[track_caller]
     fn assert_err(self, expect: expect_test::Expect) {
+        self.assert_has_err(expect, &[]);
+    }
+
+    #[track_caller]
+    fn assert_has_err(self, expect: expect_test::Expect, must_have: &[&str]) {
         match self {
             Ok(v) => panic!("expected `Err`, got `Ok`: {v:?}"),
             Err(e) => {
-                expect.assert_eq(&normalize_paths(format!("{e:?}")));
+                let output = normalize_paths(format!("{e:?}"));
+
+                expect.assert_eq(&output);
+
+                for s in must_have {
+                    assert!(output.contains(s), "did not find {s:?} in the output");
+                }
             }
         }
     }

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

@@ -1,5 +1,5 @@
 use crate::decls::Decls;
-use formality_core::{ProvenSet, Upcast};
+use formality_core::ProvenSet;
 use formality_types::rust::Term;
 
 use super::{Constraints, Env};
@@ -20,7 +20,7 @@ where
     assert_eq!(a.len(), b.len());
 
     if a.is_empty() && b.is_empty() {
-        return ProvenSet::singleton(Constraints::none(env.upcast()));
+        return ProvenSet::singleton(Constraints::none(env));
     }
 
     let a0 = a.remove(0);
@@ -45,7 +45,7 @@ where
     C: Term,
 {
     if a.is_empty() {
-        return ProvenSet::singleton(Constraints::none(env.upcast()));
+        return ProvenSet::singleton(Constraints::none(env));
     }
 
     let a0 = a[0].clone();

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

@@ -25,7 +25,7 @@ where
 }
 
 impl Constraints {
-    pub fn none(env: Env) -> Self {
+    pub fn none(env: impl Upcast<Env>) -> Self {
         let v: Vec<(Variable, Parameter)> = vec![];
         Self::from(env, v)
     }
@@ -42,9 +42,10 @@ impl Constraints {
     }
 
     pub fn from(
-        env: Env,
+        env: impl Upcast<Env>,
         iter: impl IntoIterator<Item = (impl Upcast<Variable>, impl Upcast<Parameter>)>,
     ) -> Self {
+        let env = env.upcast();
         let substitution: Substitution = iter.into_iter().collect();
         assert!(env.encloses(substitution.range()));
         assert!(env.encloses(substitution.domain()));
@@ -72,7 +73,7 @@ impl Constraints {
         }
     }
 
-    /// Given constraings from solving the subparts of `(A /\ B)`, yield combined constraints.
+    /// Given constraints from solving the subparts of `(A /\ B)`, yield combined constraints.
     ///
     /// # Parameters
     ///