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

Positive coverage: check_neg_trait_impl / check_neg_trait_impl

check_neg_trait_impl
LineCoverageSource
60✗(scope(enter_universally(Env::default(), binder) => (env, NegTraitImplBoundData { trait_id, self_ty, trait_parameters, where_clauses })) with()
(let trait_ref = trait_id.with(self_ty, trait_parameters))
(super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ())
(super::prove_goal(program, env, where_clauses, AtomicPredicate::not_implemented(&trait_ref)) => ())

(let trait_decl = program.program().trait_named(&trait_ref.trait_id)?)
(let TraitBoundData { where_clauses: _, trait_items: _ } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?))
──────── ("check_neg_trait_impl")
693(check_neg_trait_impl(program, NegTraitImpl { binder, safety: Safety::Safe }) => ())

3 tests exercised this rule:

Source location: tests/basic_tests.rs:179 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> !A<T> for u32 where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

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

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        #![feature(negative_impls)]
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/decl_safety.rs:36 (all coverage from this test)

#[test]
fn unsafe_trait_negative_impl() {
    FormalityTest::new(crates![crate baguette {
        #![feature(negative_impls)]
        unsafe trait Foo {}
        impl !Foo for u32 {}
    }])
    .skip_execute()
    .rustc_ok()
    .ok()
}
Proof tree
… (200 of 3392 nodes shown)

How to read this page