Negative coverage: prove_eq / existential / premise prove_existential_var_eq(decls, env, assumptions, v, r) => c

Premise at line 64. Observed failure causes: failed_judgment.

5 tests failed proving this premise:

Source location: crates/formality-rust/src/prove/prove/test/eq_assumptions.rs:41

#[test]
fn test_normalize_assoc_ty_existential0() {
    test_prove(
        Program::empty(),
        term("exists<A> {} => {for<T> if { <T as Iterator>::Item = u32 } <A as Iterator>::Item = u32}"),
    ).assert_err(
    expect![[r#"
        crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: <?ty_0 as Iterator>::Item = u32, via: <!ty_1 as Iterator>::Item = u32, assumptions: {<!ty_1 as Iterator>::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_1)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_1)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        the rule "normalize-via-impl" at (prove_normalize.rs) failed because
          expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`

        crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: <!ty_0 as Iterator>::Item = <?ty_1 as Iterator>::Item, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, 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: !ty_0 = ?ty_1, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_0)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: ?ty_1, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, 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: u32 = <?ty_1 as Iterator>::Item, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_0)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_0)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        the rule "normalize-via-impl" at (prove_normalize.rs) failed because
          expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`

        crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: ?ty_1 = !ty_0, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_0)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: ?ty_1, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_0)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_0)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        the rule "normalize-via-impl" at (prove_normalize.rs) failed because
          expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]);
}

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 } }"#]]);
}

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 } }"#]]);
}

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 } }"#]]);
}

Source location: crates/formality-rust/src/prove/prove/test/universes.rs:14

#[test]
fn exists_u_for_t() {
    let decls = Program::empty();
    test_prove(decls, term("exists<U> {} => {for<T> T = U}")).assert_err(expect![[r#"
        crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "existential-nonvar" at (prove_eq.rs) failed because
          pattern `None` did not match value `Some(!ty_1)`

        the rule "existential-universal" at (prove_eq.rs) failed because
          condition evaluated to false: `env.universe(p) < env.universe(v)`

        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, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}