integrate orphan check

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -1,4 +1,5 @@
 use anyhow::bail;
+use fn_error_context::context;
 use formality_prove::Env;
 use formality_rust::grammar::{Crate, TraitImpl};
 use formality_types::{
@@ -38,8 +39,18 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn orphan_check(&self, _impl_a: &TraitImpl) -> Fallible<()> {
-        Ok(())
+    #[context("orphan_check({impl_a:?})")]
+    fn orphan_check(&self, impl_a: &TraitImpl) -> 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))]

tests/coherence.rs

@@ -108,7 +108,7 @@ fn test_u32_not_u32_impls() {
                 source: "failed to disprove {! Foo((rigid (scalar u32)))} given {}, got {Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }}",
             },
         )
-    "#]] // FIXME
+    "#]]
     .assert_debug_eq(&test_program_ok(
         "[
             crate core {
@@ -130,7 +130,7 @@ fn test_T_where_Foo_not_u32_impls() {
                 source: "failed to disprove {! Foo(!ty_1)} given {Foo(!ty_1)}, got {Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => (rigid (scalar u32))} }}",
             },
         )
-    "#]] // FIXME
+    "#]]
     .assert_debug_eq(&test_program_ok(
         "[
             crate core {
@@ -164,3 +164,26 @@ fn test_non_local() {
         ]",
     ));
 }
+
+#[test]
+fn test_orphan() {
+    expect_test::expect![[r#"
+        Err(
+            Error {
+                context: "orphan_check(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 [] {}
+            }
+        ]",
+    ));
+}