Negative coverage: check_trait / check trait / premise check_trait_items_have_unique_names(&trait_items) => ()
Premise at line 22. Observed failure causes: inapplicable.
check trait| Line | Coverage | Source |
|---|---|---|
| 19 | N/A | (let Trait { safety: _, id: _, binder } = t) |
| 20 | N/A | (let (env, bound_data) = env.instantiate_universally(&binder.explicit_binder)) |
| 21 | N/A | (let TraitBoundData { where_clauses, trait_items } = bound_data) |
| 22 | 2 | (check_trait_items_have_unique_names(&trait_items) => ()) |
| 23 | 2 | (super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()) |
| 24 | ✗ | (for_all(trait_item in trait_items) (check_trait_item(program, env, where_clauses, trait_item, crate_id) => ())) |
| ──────── ("check trait") | ||
| 27 | 114 | (check_trait(program, env, t, crate_id) => ()) |
2 tests failed proving this premise:
Source location: tests/basic_tests.rs:303
Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "trait"mod.rs:172check_trait failedtraits.rs:9rule "check trait"traits.rs:22 (failed: inapplicable)
Source location: tests/basic_tests.rs:316
#[test]
fn trait_items_with_duplicate_associated_type_names() {
FormalityTest::new(crates![crate core {
trait A {
type Assoc : [];
type Assoc : [];
}
}])
.err(expect_test::expect![[r#"
the rule "check trait" at (traits.rs) failed because
the associated type name `Assoc` is defined multiple times"#]]);
}
Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "trait"mod.rs:172check_trait failedtraits.rs:9rule "check trait"traits.rs:22 (failed: inapplicable)