Negative coverage: check_crate_item / trait impl / premise check_drop_impl_always_applicable(program, v, crate_id) => ()

Premise at line 194. Observed failure causes: failed_judgment.

5 tests failed proving this premise:

Source location: tests/drop.rs:132 (all coverage from this test)

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

            struct MyStruct<T> {
                value: T,
            }

            impl<T> Drop for MyStruct<T> where T: Clone {}
        }
    ])
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: Clone(!ty_0), via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}

Source location: tests/drop.rs:154 (all coverage from this test)

#[test]
fn drop_impl_concrete_type_param() {
    FormalityTest::new(crates![
        crate Foo {
            struct MyStruct<T> {
                value: T,
            }

            impl Drop for MyStruct<u32> {}
        }
    ])
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: MyStruct<!ty_0> = MyStruct<u32>, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:54:1: no applicable rules for prove_normalize_via { goal: MyStruct<!ty_0>, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!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: !ty_0 = u32, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:54:1: no applicable rules for prove_normalize_via { goal: !ty_0, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:54:1: no applicable rules for prove_normalize_via { goal: u32, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:54:1: no applicable rules for prove_normalize_via { goal: MyStruct<u32>, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!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: u32 = !ty_0, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:54:1: no applicable rules for prove_normalize_via { goal: u32, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:54:1: no applicable rules for prove_normalize_via { goal: !ty_0, via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}

Source location: tests/drop.rs:191 (all coverage from this test)

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

            enum MyEnum<T> {
                Value{value: T},
            }

            impl<T> Drop for MyEnum<T> where T: Clone {}
        }
    ])
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: Clone(!ty_0), via: Drop(MyEnum<!ty_0>), assumptions: {Drop(MyEnum<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}

Source location: tests/drop.rs:214 (all coverage from this test)

#[test]
fn drop_impl_foreign_adt() {
    FormalityTest::new(crates![
        crate a {
            struct MyStruct {
                value: u32,
            }
        },
        crate b {
            impl Drop for MyStruct {}
        }
    ])
    .err(expect_test::expect![[r#"
        the rule "Drop impl is always applicable" at (impls.rs) failed because
          `Drop` may only be implemented for types defined in the current crate: `MyStruct` is defined in crate `a` but the impl is in crate `b`"#]])
}

Source location: tests/drop.rs:227 (all coverage from this test)

#[test]
fn drop_impl_for_non_adt() {
    FormalityTest::new(crates![
        crate Foo {
            impl Drop for u32 {}
        }
    ])
    .err(expect_test::expect![[r#"
        the rule "Drop impl is always applicable" at (impls.rs) failed because
          Drop impl self type must be a struct or enum, got `u32`"#]])
}