Negative coverage: check_crate / check crate / premise check_coherence(program, c) => ()

Premise at line 74. Observed failure causes: failed_judgment.

11 tests failed proving this premise:

Source location: tests/coherence_orphan.rs:12

#[test]
fn neg_CoreTrait_for_CoreStruct_in_Foo() {
    FormalityTest::new(crates![crate core {
                trait CoreTrait {}
                struct CoreStruct {}
            },
            crate foo {
                impl !CoreTrait for CoreStruct {}
            }]).err(expect_test::expect![[r#"
            the rule "fundamental rigid type" at (is_local.rs) failed because
              condition evaluated to false: `is_fundamental(decls, name)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl ! CoreTrait for CoreStruct {} }], 222)
                name = (adt CoreStruct)

            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

            the rule "local rigid type" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_adt_id(a)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl ! CoreTrait for CoreStruct {} }], 222)
                a = CoreStruct

            the rule "local trait" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl ! CoreTrait for CoreStruct {} }], 222)
                &goal.trait_id = CoreTrait"#]])
}

Source location: tests/coherence_orphan.rs:47

#[test]
fn mirror_CoreStruct() {
    FormalityTest::new(crates![crate core {
                trait CoreTrait {}
                struct CoreStruct {}

                trait Mirror {
                    type Assoc : [];
                }

                impl<T> Mirror for T {
                    type Assoc = T;
                }
            },
            crate foo {
                impl CoreTrait for <CoreStruct as Mirror>::Assoc {}
            }]).err(expect_test::expect![[r#"
            the rule "fundamental rigid type" at (is_local.rs) failed because
              condition evaluated to false: `is_fundamental(decls, name)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } trait Mirror <ty> { type Assoc : [] ; } impl <ty> Mirror for ^ty0_0 { type Assoc = ^ty1_0 ; } }, crate foo { impl CoreTrait for <CoreStruct as Mirror>::Assoc { } }], 222)
                name = (adt CoreStruct)

            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

            the rule "local rigid type" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_adt_id(a)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } trait Mirror <ty> { type Assoc : [] ; } impl <ty> Mirror for ^ty0_0 { type Assoc = ^ty1_0 ; } }, crate foo { impl CoreTrait for <CoreStruct as Mirror>::Assoc { } }], 222)
                a = CoreStruct

            the rule "local trait" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } trait Mirror <ty> { type Assoc : [] ; } impl <ty> Mirror for ^ty0_0 { type Assoc = ^ty1_0 ; } }, crate foo { impl CoreTrait for <CoreStruct as Mirror>::Assoc { } }], 222)
                &goal.trait_id = CoreTrait"#]])
}

Source location: tests/coherence_orphan.rs:109

#[test]
fn uncovered_T() {
    FormalityTest::new(crates![crate core {
                trait CoreTrait<T> {}
            },
            crate foo {
                struct FooStruct {}
                impl<T> CoreTrait<FooStruct> for T {}
            }]).err(expect_test::expect![[r#"
            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: !ty_0, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: !ty_0, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

            the rule "local trait" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
                decls = program([crate core { trait CoreTrait <ty, ty> { } }, crate foo { struct FooStruct { } impl <ty> CoreTrait <FooStruct> for ^ty0_0 { } }], 222)
                &goal.trait_id = CoreTrait"#]])
}

Source location: tests/coherence_orphan.rs:136

#[test]
fn alias_to_unit() {
    FormalityTest::new(crates![crate core {
                trait CoreTrait {}

                trait Unit {
                    type Assoc : [];
                }

                impl<T> Unit for T {
                    type Assoc = ();
                }
            },
            crate foo {
                struct FooStruct {}
                impl CoreTrait for <FooStruct as Unit>::Assoc {}
            }]).err(expect_test::expect![[r#"
            the rule "fundamental rigid type" at (is_local.rs) failed because
              condition evaluated to false: `is_fundamental(decls, name)`
                decls = program([crate core { trait CoreTrait <ty> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
                name = tuple(0)

            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

            the rule "local trait" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
                decls = program([crate core { trait CoreTrait <ty> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
                &goal.trait_id = CoreTrait"#]])
}

Source location: tests/coherence_orphan.rs:158

#[test]
fn CoreTrait_for_CoreStruct_in_Foo() {
    FormalityTest::new(crates![crate core {
                trait CoreTrait {}
                struct CoreStruct {}
            },
            crate foo {
                impl CoreTrait for CoreStruct {}
            }]).err(expect_test::expect![[r#"
            the rule "fundamental rigid type" at (is_local.rs) failed because
              condition evaluated to false: `is_fundamental(decls, name)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for CoreStruct { } }], 222)
                name = (adt CoreStruct)

            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

            the rule "local rigid type" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_adt_id(a)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for CoreStruct { } }], 222)
                a = CoreStruct

            the rule "local trait" at (is_local.rs) failed because
              condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
                decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for CoreStruct { } }], 222)
                &goal.trait_id = CoreTrait"#]])
}

Source location: tests/coherence_overlap.rs:161

#[test]
fn foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait() {
    FormalityTest::new(crates![crate core {
        trait CoreTrait {}
        struct CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .err(expect_test::expect![[r#"
            the rule "check_coherence" at (coherence.rs) failed because
              impls may overlap:
              impl <ty> FooTrait for ^ty0_0 where ^ty0_0 : CoreTrait { }
              impl FooTrait for CoreStruct { }"#]])
}

Source location: tests/coherence_overlap.rs:189

#[test]
fn u32_T_where_T_Is_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl<T> Foo for T where T: Is {}

        trait Is {}
        impl Is for u32 {}
    }])
    .err(expect_test::expect![[r#"
            the rule "check_coherence" at (coherence.rs) failed because
              impls may overlap:
              impl Foo for u32 { }
              impl <ty> Foo for ^ty0_0 where ^ty0_0 : Is { }"#]])
}

Source location: tests/coherence_overlap.rs:239

#[test]
fn u32_T_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl<T> Foo for T {}
    }])
    .err(expect_test::expect![[r#"
            the rule "check_coherence" at (coherence.rs) failed because
              impls may overlap:
              impl Foo for u32 { }
              impl <ty> Foo for ^ty0_0 { }"#]])
}

Source location: tests/coherence_overlap.rs:257

#[test]
fn T_and_T_bar() {
    FormalityTest::new(crates![crate core {
        trait Foo { }

        trait Bar { }

        impl<T> Foo for T { }

        impl<T> Foo for T where T: Bar { }
    }])
    .err(expect_test::expect![[r#"
            the rule "check_coherence" at (coherence.rs) failed because
              impls may overlap:
              impl <ty> Foo for ^ty0_0 { }
              impl <ty> Foo for ^ty0_0 where ^ty0_0 : Bar { }"#]])
}

Source location: tests/coherence_overlap.rs:277

#[test]
fn T_and_Local_Bar_T() {
    FormalityTest::new(crates![crate core {
        trait Foo { }

        trait Bar<U> { }

        impl<T> Foo for T { }

        impl<T> Foo for T where LocalType: Bar<T> { }

        struct LocalType { }
    }])
    .err(expect_test::expect![[r#"
            the rule "check_coherence" at (coherence.rs) failed because
              impls may overlap:
              impl <ty> Foo for ^ty0_0 { }
              impl <ty> Foo for ^ty0_0 where LocalType : Bar <^ty0_0> { }"#]])
}

Source location: tests/coherence_overlap.rs:333

#[test]
fn is_local_with_unconstrained_self_ty_blanket_impl() {
    // TODO: this test should pass imho
    FormalityTest::new(crates![crate core {
                trait Project {
                    type Assoc: [];
                }

                impl<T> Project for T {
                    type Assoc = ();
                }

                trait Foo<U> { }
            },
            crate foo {
                struct LocalType {}
                impl Foo<LocalType> for () {}

                trait Overlap<U> {}
                impl<T, U> Overlap<U> for T
                where
                    <T as Project>::Assoc: Foo<U> {}
                impl<T> Overlap<LocalType> for T {}
            }]).err(expect_test::expect![[r#"
            the rule "check_coherence" at (coherence.rs) failed because
              impls may overlap:
              impl <ty, ty> Overlap <^ty0_1> for ^ty0_0 where <^ty0_0 as Project>::Assoc : Foo <^ty0_1> { }
              impl <ty> Overlap <LocalType> for ^ty0_0 { }"#]])
}

Proof trees omitted for the remaining 1 tests.