simplify coherence definition

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -95,25 +95,26 @@ impl Check<'_> {
 
         assert_eq!(trait_ref_a.trait_id, trait_ref_b.trait_id);
 
-        // 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 we can prove that the parameters cannot be equated *or* the where-clauses don't hold,
+        // in coherence mode, then they do not overlap.
         if let Ok(()) = self.prove_not_goal(
             &env.with_coherence_mode(true),
-            (&a.where_clauses, &b.where_clauses),
-            Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+            (),
+            (
+                Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+                &a.where_clauses,
+                &b.where_clauses,
+            ),
         ) {
-            return Ok(());
-        }
+            tracing::debug!(
+                "proved not {:?}",
+                (
+                    Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+                    &a.where_clauses,
+                    &b.where_clauses,
+                )
+            );
 
-        // 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),
-            (&a.where_clauses, &b.where_clauses),
-        ) {
             return Ok(());
         }
 
@@ -129,18 +130,28 @@ impl Check<'_> {
             .chain(&b.where_clauses)
             .flat_map(|wc| wc.invert())
             .collect();
-        if inverted.iter().any(|inverted_wc| {
+        if let Some(inverted_wc) = inverted.iter().find(|inverted_wc| {
             self.prove_goal(
                 &env,
                 (
                     Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
                     &a.where_clauses,
                     &b.where_clauses,
                 ),
-                inverted_wc,
+                &inverted_wc,
             )
             .is_ok()
         }) {
+            tracing::debug!(
+                "proved {:?} assuming {:?}",
+                &inverted_wc,
+                (
+                    Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+                    &a.where_clauses,
+                    &b.where_clauses,
+                )
+            );
+
             return Ok(());
         }
         bail!("impls may overlap: `{impl_a:?}` vs `{impl_b:?}`")

crates/formality-rust/src/prove.rs

@@ -327,6 +327,12 @@ upcast_to_wcs! {
     Relation,
 }
 
+impl ToWcs for () {
+    fn to_wcs(&self) -> Wcs {
+        Wcs::t()
+    }
+}
+
 impl<A, B> ToWcs for (A, B)
 where
     A: ToWcs,