Negative coverage: prove_existential_var_eq / existential-nonvar / premise equate_variable(decls, env, assumptions, v, t) => c
Premise at line 97. Observed failure causes: failed_judgment.
existential-nonvar| Line | Coverage | Source |
|---|---|---|
| 96 | 2 | (if let None = t.downcast::<Variable>()) |
| 97 | 3 | (equate_variable(decls, env, assumptions, v, t) => c) |
| ──────── ("existential-nonvar") | ||
| 99 | 31 | (prove_existential_var_eq(decls, env, assumptions, v, t) => c) |
3 tests failed proving this premise:
Source location: crates/formality-rust/src/prove/prove/test/occurs_check.rs:24
#[test]
fn direct_cycle() {
test_prove(decls(), term("exists<A> {} => {A = Vec<A>}")).assert_err(expect![[r#"
failed at (proven_set.rs) because
`?ty_0` occurs in `Vec<?ty_0>`
crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}Failed proof tree
prove failedtest_util.rs:60ruletest_util.rs:60prove_wc_list failedprove_wc_list.rs:11rule "some"prove_wc_list.rs:29prove_wc failedprove_wc.rs:23rule "eq"prove_wc.rs:127prove_eq failedprove_eq.rs:25rule "existential"prove_eq.rs:64prove_existential_var_eq failedprove_eq.rs:78rule "existential-nonvar"prove_eq.rs:97equate_variable failedprove_eq.rs:97ruleproven_set.rs:57 (failed: inapplicable)
Source location: crates/formality-rust/src/prove/prove/test/occurs_check.rs:48
#[test]
fn indirect_cycle_1() {
test_prove(decls(), term("exists<A, B> {} => {A = Vec<B>, B = A}")).assert_err(expect![[r#"
failed at (proven_set.rs) because
`?ty_0` occurs in `Vec<?ty_0>`
crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}Failed proof tree
prove failedtest_util.rs:60ruletest_util.rs:60prove_wc_list failedprove_wc_list.rs:11rule "some"prove_wc_list.rs:30prove_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 "eq"prove_wc.rs:127prove_eq failedprove_eq.rs:25rule "existential"prove_eq.rs:64prove_existential_var_eq failedprove_eq.rs:78rule "existential-nonvar"prove_eq.rs:97equate_variable failedprove_eq.rs:97ruleproven_set.rs:57 (failed: inapplicable)
Source location: crates/formality-rust/src/prove/prove/test/occurs_check.rs:60
#[test]
fn indirect_cycle_2() {
test_prove(decls(), term("exists<A, B> {} => {B = A, A = Vec<B>}")).assert_err(expect![[r#"
failed at (proven_set.rs) because
`?ty_0` occurs in `Vec<?ty_0>`
crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}Failed proof tree
prove failedtest_util.rs:60ruletest_util.rs:60prove_wc_list failedprove_wc_list.rs:11rule "some"prove_wc_list.rs:30prove_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 "eq"prove_wc.rs:127prove_eq failedprove_eq.rs:25rule "existential"prove_eq.rs:64prove_existential_var_eq failedprove_eq.rs:78rule "existential-nonvar"prove_eq.rs:97equate_variable failedprove_eq.rs:97ruleproven_set.rs:57 (failed: inapplicable)