Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Negative coverage: check_drop_impl_always_applicable / Drop impl is always applicable / premise check_drop_impl_in_defining_crate(program, adt_id, crate_id) => ()

Premise at line 322. Observed failure causes: inapplicable.

Drop impl is always applicable
LineCoverageSource
318(if **trait_impl.trait_id() == *"Drop")
3201(let adt_id = drop_impl_adt_id(&trait_impl)?)
3221(check_drop_impl_in_defining_crate(program, adt_id, crate_id) => ())
323(let adt = program.program().adt_item_named(adt_id)?.to_adt())
325N/A(let (env, adt_vars) = Env::default().universal_substitution(&adt.binder))
326(let adt_bound = adt.binder.instantiate_with(adt_vars)?)
327N/A(let adt_self_ty = Ty::rigid(adt_id, adt_vars))
330N/A(let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ()))
3313(super::prove_goal(&program, &env, &adt_bound.where_clauses,
Predicate::IsImplemented(drop_trait_ref.clone())) => ())
──────── ("Drop impl is always applicable")
3346(check_drop_impl_always_applicable(program, trait_impl, crate_id) => ())

1 test failed proving this premise:


Source location: tests/drop.rs:214

#[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`"#]])
}
Failed proof tree