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 let adt_id = drop_impl_adt_id(&trait_impl)?

Premise at line 302. Observed failure causes: inapplicable.

Drop impl is always applicable
LineCoverageSource
300(if **trait_impl.trait_id() == *"Drop")
3021(let adt_id = drop_impl_adt_id(&trait_impl)?)
303(let adt = program.program().adt_item_named(adt_id)?.to_adt())
305N/A(let (env, adt_vars) = Env::default().universal_substitution(&adt.binder))
306(let adt_bound = adt.binder.instantiate_with(adt_vars)?)
307N/A(let adt_self_ty = Ty::rigid(adt_id, adt_vars))
310N/A(let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ()))
3112(super::prove_goal(&program, &env, &adt_bound.where_clauses,
Predicate::IsImplemented(drop_trait_ref.clone())) => ())
──────── ("Drop impl is always applicable")
3144(check_drop_impl_always_applicable(program, trait_impl) => ())

1 test failed proving this premise:


Source location: tests/drop.rs:152

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