Negative coverage: prove_existential_var_eq / existential-nonvar / premise equate_variable(decls, env, assumptions, v, t) => c

Premise at line 95. Observed failure causes: failed_judgment.

3 tests failed proving this premise:

Source location: crates/formality-rust/src/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_normalize.rs:20: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_normalize.rs:20:1: no applicable rules for prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}

Source location: crates/formality-rust/src/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_normalize.rs:20: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_normalize.rs:20:1: no applicable rules for prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}

Source location: crates/formality-rust/src/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_normalize.rs:20: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_normalize.rs:20:1: no applicable rules for prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}