check negative impls per coherence rules

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -1,7 +1,7 @@
 use anyhow::bail;
 use fn_error_context::context;
 use formality_prove::Env;
-use formality_rust::grammar::{Crate, TraitImpl};
+use formality_rust::grammar::{Crate, NegTraitImpl, TraitImpl};
 use formality_types::{
     cast::Downcasted,
     grammar::{Fallible, Wc, Wcs},
@@ -15,11 +15,17 @@ impl Check<'_> {
         let all_crate_impls: Vec<TraitImpl> =
             self.program.items_from_all_crates().downcasted().collect();
         let current_crate_impls: Vec<TraitImpl> = current_crate.items.iter().downcasted().collect();
+        let current_crate_neg_impls: Vec<NegTraitImpl> =
+            current_crate.items.iter().downcasted().collect();
 
         for impl_a in &current_crate_impls {
             self.orphan_check(impl_a)?;
         }
 
+        for impl_a in &current_crate_neg_impls {
+            self.orphan_check_neg(impl_a)?;
+        }
+
         // check for duplicate impls in the current crate
         for (impl_a, i) in current_crate_impls.iter().zip(0..) {
             if current_crate_impls[i + 1..].contains(impl_a) {
@@ -54,6 +60,20 @@ impl Check<'_> {
         )
     }
 
+    #[context("orphan_check_neg({impl_a:?})")]
+    fn orphan_check_neg(&self, impl_a: &NegTraitImpl) -> Fallible<()> {
+        let mut env = Env::default();
+
+        let a = env.instantiate_universally(&impl_a.binder);
+        let trait_ref = a.trait_ref();
+
+        self.prove_goal(
+            &env.with_coherence_mode(true),
+            &a.where_clauses,
+            trait_ref.is_local(),
+        )
+    }
+
     #[tracing::instrument(level = "Debug", skip(self))]
     fn overlap_check(&self, impl_a: &TraitImpl, impl_b: &TraitImpl) -> Fallible<()> {
         let mut env = Env::default();

crates/formality-rust/src/grammar.rs

@@ -281,6 +281,12 @@ pub struct NegTraitImplBoundData {
     pub where_clauses: Vec<WhereClause>,
 }
 
+impl NegTraitImplBoundData {
+    pub fn trait_ref(&self) -> TraitRef {
+        self.trait_id.with(&self.self_ty, &self.trait_parameters)
+    }
+}
+
 #[term]
 pub enum ImplItem {
     #[cast]

tests/coherence_orphan.rs

@@ -4,7 +4,7 @@ use formality::test_program_ok;
 use formality_macros::test;
 
 #[test]
-fn test_orphan_basic() {
+fn test_orphan_CoreTrait_for_CoreStruct_in_Foo() {
     expect_test::expect![[r#"
         Err(
             Error {
@@ -26,6 +26,29 @@ fn test_orphan_basic() {
     ));
 }
 
+#[test]
+fn test_orphan_neg_CoreTrait_for_CoreStruct_in_Foo() {
+    expect_test::expect![[r#"
+        Err(
+            Error {
+                context: "orphan_check_neg(impl <> ! CoreTrait < > for (rigid (adt CoreStruct)) where [] {})",
+                source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}",
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate core {
+                trait CoreTrait<> where [] {}
+                struct CoreStruct<> where [] {}
+            },
+            crate foo {
+                impl<> !CoreTrait<> for CoreStruct<> where [] {}
+            }
+        ]",
+    ));
+}
+
 #[test]
 fn test_orphan_mirror_CoreStruct() {
     expect_test::expect![[r#"