Negative coverage: check_trait / check trait / premise super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()
Premise at line 23. Observed failure causes: failed_judgment.
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:34
#[test]
fn hello_world_fail() {
FormalityTest::new(crates![crate Foo {
trait Foo<T> where T: Bar<Self> {}
trait Bar<T> where T: Baz {}
trait Baz {}
}]).err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), via: Bar(!ty_0, !ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: Baz(!ty_1), via: Bar(!ty_0, !ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "trait implied bound" at (prove_wc.rs) failed because
expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}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:23prove failedfunction.rs:250rulefunction.rs:250prove_wc_list failedprove_wc_list.rs:11rule "some"prove_wc_list.rs:29prove_wc failedprove_wc.rs:23rule "assumption - predicate"prove_wc.rs:50prove_via failedprove_via.rs:9
rule "trait well formed"prove_wc.rs:142prove_after failedprove_after.rs:8rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19ruleprove_after.rs:19prove_wc_list failedprove_wc_list.rs:11rule "some"prove_wc_list.rs:29prove_wc failedprove_wc.rs:23rule "assumption - predicate"prove_wc.rs:50prove_via failedprove_via.rs:9
rule "trait implied bound"prove_wc.rs:117 (failed: empty_collection)
Source location: tests/basic_tests.rs:85
#[test]
fn basic_where_clauses_fail() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
trait WellFormed where for<T> u32: A<T> { }
}]).err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: @ WellFormedTraitRef(A(u32, !ty_1)), via: A(u32, ?ty_2), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: B(!ty_0), via: A(u32, ?ty_1), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "trait implied bound" at (prove_wc.rs) failed because
expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}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:23prove failedfunction.rs:250rulefunction.rs:250prove_wc_list failedprove_wc_list.rs:11rule "some"prove_wc_list.rs:29prove_wc failedprove_wc.rs:23rule "forall"prove_wc.rs:37prove_wc failedprove_wc.rs:23rule "assumption - predicate"prove_wc.rs:50prove_via failedprove_via.rs:9rule "forall"prove_via.rs:50prove_via failedprove_via.rs:9
rule "trait well formed"prove_wc.rs:142prove_after failedprove_after.rs:8rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19ruleprove_after.rs:19prove_wc_list failedprove_wc_list.rs:11rule "some"prove_wc_list.rs:29prove_wc failedprove_wc.rs:23rule "assumption - predicate"prove_wc.rs:50prove_via failedprove_via.rs:9rule "forall"prove_via.rs:50prove_via failedprove_via.rs:9
rule "trait implied bound"prove_wc.rs:117 (failed: empty_collection)