Negative coverage: check_adt / check adt / premise prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()
Premise at line 21. Observed failure causes: failed_judgment.
check adt| Line | Coverage | Source |
|---|---|---|
| 18 | 2 | (check_adt_variant_names_unique(adt) => ()) |
| 19 | N/A | (let (env, bound_data) = Env::default().instantiate_universally(&adt.binder)) |
| 20 | N/A | (let AdtBoundData { where_clauses, variants } = bound_data) |
| 21 | 1 | (prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()) |
| 22 | ✗ | (for_all(variant in variants) (let Variant { fields, .. } = variant) (for_all(field in fields) (let Field { ty, .. } = field) (prove_goal(program, env, where_clauses, Relation::well_formed(ty)) => ()))) |
| ──────── ("check adt") | ||
| 28 | 31 | (check_adt(program, adt) => ()) |
1 test failed proving this premise:
Source location: tests/well_formed_trait_ref.rs:37
#[test]
fn missing_dependent_where_clause() {
FormalityTest::new(crates![crate foo {
trait Trait1 {}
trait Trait2 {}
struct S1<T> where T: Trait1 {
dummy: T,
}
struct S2<T> where S1<T> : Trait2 {
dummy: 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(Trait2(S1<!ty_0>)), via: Trait2(S1<!ty_0>), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!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: Trait1(!ty_0), via: Trait2(S1<!ty_0>), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!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 "adt"mod.rs:185check_adt failedadts.rs:11rule "check adt"adts.rs:21prove 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:139prove_wf failedprove_wf.rs:14rule "ADT"prove_wf.rs:67prove_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)