Negative coverage: overlap_check_impl / different trait / premise if impl_a.trait_id() != impl_b.trait_id()

Premise at line 79. Observed failure causes: if_false.

6 tests failed proving this premise:

Source location: tests/coherence_overlap.rs:251 (all coverage from this test)

#[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 "different trait" at (coherence.rs) failed because
          condition evaluated to false: `impl_a.trait_id() != impl_b.trait_id()`

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! CoreTrait(!ty_0), via: !ty_0 = CoreStruct, assumptions: {!ty_0 = CoreStruct, CoreTrait(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! CoreTrait(!ty_0), via: CoreTrait(!ty_0), assumptions: {!ty_0 = CoreStruct, CoreTrait(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "negative impl" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.neg_impl_decls(&trait_ref.trait_id)`

        the rule "not goal" at (coherence.rs) failed because
          failed to prove {!ty_1 = CoreStruct, CoreTrait(!ty_1)} given {}, got [Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }]

        the rule "same impl" at (coherence.rs) failed because
          condition evaluated to false: `impl_a == impl_b`
            impl_a = impl <ty> FooTrait for ^ty0_0 where ^ty0_0 : CoreTrait { }
            impl_b = impl FooTrait for CoreStruct { }"#]])
}

Source location: tests/coherence_overlap.rs:292 (all coverage from this test)

#[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 "different trait" at (coherence.rs) failed because
          condition evaluated to false: `impl_a.trait_id() != impl_b.trait_id()`

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Is(!ty_0), via: Is(!ty_0), assumptions: {u32 = !ty_0, Is(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Is(!ty_0), via: u32 = !ty_0, assumptions: {u32 = !ty_0, Is(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "negative impl" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.neg_impl_decls(&trait_ref.trait_id)`

        the rule "not goal" at (coherence.rs) failed because
          failed to prove {u32 = !ty_1, Is(!ty_1)} given {}, got [Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }]

        the rule "same impl" at (coherence.rs) failed because
          condition evaluated to false: `impl_a == impl_b`
            impl_a = impl Foo for u32 { }
            impl_b = impl <ty> Foo for ^ty0_0 where ^ty0_0 : Is { }"#]])
}

Source location: tests/coherence_overlap.rs:355 (all coverage from this test)

#[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 "different trait" at (coherence.rs) failed because
          condition evaluated to false: `impl_a.trait_id() != impl_b.trait_id()`

        the rule "inverted" at (coherence.rs) failed because
          expression evaluated to an empty collection: `a.where_clauses.iter().chain(&b.where_clauses).flat_map(|wc| wc.invert())`

        the rule "not goal" at (coherence.rs) failed because
          failed to prove {u32 = !ty_1} given {}, got [Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }]

        the rule "same impl" at (coherence.rs) failed because
          condition evaluated to false: `impl_a == impl_b`
            impl_a = impl Foo for u32 { }
            impl_b = impl <ty> Foo for ^ty0_0 { }"#]])
}

Source location: tests/coherence_overlap.rs:382 (all coverage from this test)

#[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 "different trait" at (coherence.rs) failed because
          condition evaluated to false: `impl_a.trait_id() != impl_b.trait_id()`

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Bar(!ty_1), via: !ty_0 = !ty_1, assumptions: {!ty_0 = !ty_1, Bar(!ty_1)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Bar(!ty_1), via: Bar(!ty_1), assumptions: {!ty_0 = !ty_1, Bar(!ty_1)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "negative impl" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.neg_impl_decls(&trait_ref.trait_id)`

        the rule "not goal" at (coherence.rs) failed because
          failed to prove {!ty_1 = !ty_2, Bar(!ty_2)} given {}, got [Constraints { env: Env { variables: [!ty_1, !ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }]

        the rule "same impl" at (coherence.rs) failed because
          condition evaluated to false: `impl_a == impl_b`
            impl_a = impl <ty> Foo for ^ty0_0 { }
            impl_b = impl <ty> Foo for ^ty0_0 where ^ty0_0 : Bar { }"#]])
}

Source location: tests/coherence_overlap.rs:415 (all coverage from this test)

#[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 "different trait" at (coherence.rs) failed because
          condition evaluated to false: `impl_a.trait_id() != impl_b.trait_id()`

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Bar(LocalType, !ty_1), via: !ty_0 = !ty_1, assumptions: {!ty_0 = !ty_1, Bar(LocalType, !ty_1)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Bar(LocalType, !ty_1), via: Bar(LocalType, !ty_1), assumptions: {!ty_0 = !ty_1, Bar(LocalType, !ty_1)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "negative impl" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.neg_impl_decls(&trait_ref.trait_id)`

        the rule "not goal" at (coherence.rs) failed because
          failed to prove {!ty_1 = !ty_2, Bar(LocalType, !ty_2)} given {}, got [Constraints { env: Env { variables: [!ty_1, !ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }]

        the rule "same impl" at (coherence.rs) failed because
          condition evaluated to false: `impl_a == impl_b`
            impl_a = impl <ty> Foo for ^ty0_0 { }
            impl_b = impl <ty> Foo for ^ty0_0 where LocalType : Bar <^ty0_0> { }"#]])
}

Source location: tests/coherence_overlap.rs:484 (all coverage from this test)

#[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 "different trait" at (coherence.rs) failed because
                  condition evaluated to false: `impl_a.trait_id() != impl_b.trait_id()`

                crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Foo(<!ty_0 as Project>::Assoc, !ty_2), via: !ty_0 = !ty_1, assumptions: {!ty_0 = !ty_1, !ty_2 = LocalType, Foo(<!ty_0 as Project>::Assoc, !ty_2)}, env: Env { variables: [!ty_0, !ty_2, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

                crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Foo(<!ty_0 as Project>::Assoc, !ty_2), via: !ty_2 = LocalType, assumptions: {!ty_0 = !ty_1, !ty_2 = LocalType, Foo(<!ty_0 as Project>::Assoc, !ty_2)}, env: Env { variables: [!ty_0, !ty_2, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

                crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: ! Foo(<!ty_0 as Project>::Assoc, !ty_2), via: Foo(<!ty_0 as Project>::Assoc, !ty_2), assumptions: {!ty_0 = !ty_1, !ty_2 = LocalType, Foo(<!ty_0 as Project>::Assoc, !ty_2)}, env: Env { variables: [!ty_0, !ty_2, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

                the rule "negative impl" at (prove_wc.rs) failed because
                  expression evaluated to an empty collection: `decls.neg_impl_decls(&trait_ref.trait_id)`

                the rule "not goal" at (coherence.rs) failed because
                  failed to prove {!ty_1 = !ty_3, !ty_2 = LocalType, Foo(<!ty_1 as Project>::Assoc, !ty_2)} given {}, got [Constraints { env: Env { variables: [!ty_1, !ty_2, !ty_3], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }]

                the rule "same impl" at (coherence.rs) failed because
                  condition evaluated to false: `impl_a == impl_b`
                    impl_a = impl <ty, ty> Overlap <^ty0_1> for ^ty0_0 where <^ty0_0 as Project>::Assoc : Foo <^ty0_1> { }
                    impl_b = impl <ty> Overlap <LocalType> for ^ty0_0 { }"#]])
}