integrate coherence mode into test

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

@@ -42,6 +42,7 @@ impl Check<'_> {
         Ok(())
     }
 
+    #[tracing::instrument(level = "Debug", skip(self))]
     fn overlap_check(&self, impl_a: &TraitImpl, impl_b: &TraitImpl) -> Fallible<()> {
         let mut env = Env::default();
 
@@ -53,7 +54,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 +63,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

@@ -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

@@ -1,4 +1,5 @@
 use formality::test_program_ok;
+use formality_macros::test;
 
 #[test]
 fn test_u32_i32_impls() {
@@ -145,10 +146,10 @@ fn test_T_where_Foo_not_u32_impls() {
 #[allow(non_snake_case)]
 fn test_non_local() {
     expect_test::expect![[r#"
-        Ok(
-            (),
+        Err(
+            "impls may overlap: `impl <ty> FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`",
         )
-    "#]] // FIXME
+    "#]]
     .assert_debug_eq(&test_program_ok(
         "[
             crate core {