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_trait_impl / check_trait_impl / premise check_safety_matches(&trait_decl, &trait_impl) => ()

Premise at line 33. Observed failure causes: failed_judgment.

check_trait_impl
LineCoverageSource
22N/A(let TraitImpl { binder, safety: _ } = &trait_impl)
23N/A(let (env, bound_data) = Env::default().instantiate_universally(binder))
24N/A(let TraitImplBoundData { trait_id, self_ty, trait_parameters, where_clauses, impl_items } = bound_data)
25N/A(let trait_ref = trait_id.with(self_ty, trait_parameters))
27✗(super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ())
282(super::prove_goal(program, env, where_clauses, Predicate::is_implemented(trait_ref)) => ())
292(super::prove_not_goal(program, env, where_clauses, Predicate::not_implemented(trait_ref)) => ())
31✗(let trait_decl = program.program().trait_named(&trait_ref.trait_id)?)
32✗(let TraitBoundData { where_clauses: _, trait_items } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?)
332(check_safety_matches(&trait_decl, &trait_impl) => ())
352(check_duplicate_impl_items(impl_items) => ())
36✗(for_all(impl_item in impl_items)
(check_trait_impl_item(program, env, where_clauses, trait_items, impl_item, crate_id) => ()))
392(check_all_required_items_present(trait_items, impl_items) => ())
──────── ("check_trait_impl")
42127(check_trait_impl(program, trait_impl, crate_id) => ())

2 tests failed proving this premise:

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

#[test]
fn unsafe_trait_mismatch() {
    FormalityTest::new(crates![crate baguette {
        unsafe trait Foo {}
        impl Foo for u32 {}
    }])
    .rustc_err(expect_test::expect![[r#"
        error[E0200]: the trait `Foo` requires an `unsafe impl` declaration
         --> lib.rs
          |
        3 | impl Foo for u32 {}
          | ^^^^^^^^^^^^^^^^
          |
          = note: the trait `Foo` enforces invariants that the compiler can't check. Review the trait documentation and make sure this implementation upholds those invariants before adding the `unsafe` keyword
        help: add `unsafe` to this trait implementation
          |
        3 | unsafe impl Foo for u32 {}
          | ++++++

        For more information about this error, try `rustc --explain E0200`.
        error: could not compile `baguette` (lib) due to 1 previous error
    "#]])
    .err(expect_test::expect![[r#"
            the rule "safety matches" at (impls.rs) failed because
              condition evaluated to false: `trait_decl.safety == trait_impl.safety`"#]])
}
Failed proof tree

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

#[test]
fn safe_trait_mismatch() {
    FormalityTest::new(crates![crate baguette {
        trait Foo {}
        unsafe impl Foo for u32 {}
    }])
    .rustc_err(expect_test::expect![[r#"
        error[E0199]: implementing the trait `Foo` is not unsafe
         --> lib.rs
          |
        3 | unsafe impl Foo for u32 {}
          | ^^^^^^^^^^^^^^^^^^^^^^^
          |
        help: remove `unsafe` from this trait implementation
          |
        3 - unsafe impl Foo for u32 {}
        3 + impl Foo for u32 {}
          |

        For more information about this error, try `rustc --explain E0199`.
        error: could not compile `baguette` (lib) due to 1 previous error
    "#]])
    .err(expect_test::expect![[r#"
            the rule "safety matches" at (impls.rs) failed because
              condition evaluated to false: `trait_decl.safety == trait_impl.safety`"#]])
}
Failed proof tree