more coherence

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -60,6 +60,15 @@ impl Check<'_> {
             return Ok(());
         }
 
+        // If we can disprove the where clauses, then they do not overlap.
+        if let Ok(()) = self.prove_not_goal(
+            &env,
+            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:?}`")
     }
 }

tests/coherence.rs

@@ -55,3 +55,44 @@ fn test_u32_T_impls() {
     ]",
     ));
 }
+
+#[test]
+fn test_u32_T_where_T_Not_impls() {
+    expect_test::expect![[r#"
+        Ok(
+            (),
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+        crate Foo {
+            trait Foo<> where [] {}
+            impl<> Foo<> for u32 where [] {}
+            impl<ty T> Foo<> for T where [T: Not<>] {}
+
+            trait Not<> where [] {}
+        }
+    ]",
+    ));
+}
+
+#[test]
+fn test_u32_T_where_T_Is_impls() {
+    expect_test::expect![[r#"
+        Err(
+            "impls may overlap: `impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`",
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+        crate Foo {
+            trait Foo<> where [] {}
+            impl<> Foo<> for u32 where [] {}
+            impl<ty T> Foo<> for T where [T: Is<>] {}
+
+            trait Is<> where [] {}
+            impl<> Is<> for u32 where [] {}
+        }
+    ]",
+    ));
+}