Negative coverage: prove_normalize / normalize-via-impl / premise decl in decls.alias_eq_decls(&a.name)
Premise at line 39. Observed failure causes: empty_collection.
normalize-via-impl| Line | Coverage | Source |
|---|---|---|
| 39 | 1 | (decl in decls.alias_eq_decls(&a.name)) |
| 40 | N/A | (let (env, subst) = env.existential_substitution(&decl.binder)) |
| 41 | N/A | (let decl = decl.binder.instantiate_with(&subst).unwrap()) |
| 42 | N/A | (let AliasEqDeclBoundData { alias: AliasTy { name, parameters }, ty, where_clause } = decl) |
| 43 | ✗ | (assert a.name == *name) |
| 44 | ✗ | (prove(decls, env, assumptions, Wcs::all_eq(&a.parameters, ¶meters)) => c) |
| 45 | ✗ | (prove_after(decls, c, assumptions, &where_clause) => c) |
| 46 | N/A | (let ty = c.substitution().apply(ty)) |
| 47 | N/A | (let c = c.pop_subst(&subst)) |
| 48 | ✗ | (assert c.env().encloses(&ty)) |
| ──────── ("normalize-via-impl") | ||
| 50 | 27 | (prove_normalize(decls, env, assumptions, TyData::AliasTy(a)) => Constrained(ty, c)) |
1 test 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)`"#]]);
}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 "forall"prove_wc.rs:37prove_wc failedprove_wc.rs:23rule "implies"prove_wc.rs:43prove_wc failedprove_wc.rs:23rule "eq"prove_wc.rs:127prove_eq failedprove_eq.rs:25rule "normalize-l"prove_eq.rs:70prove_normalize failedprove_normalize.rs:19rule "normalize-via-impl"prove_normalize.rs:39 (failed: empty_collection)
rule "symmetric"prove_eq.rs:40prove_eq failedprove_eq.rs:25rule "normalize-l"prove_eq.rs:71prove_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 "normalize-l"prove_eq.rs:71prove_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 "symmetric"prove_eq.rs:40prove_eq failedprove_eq.rs:25rule "normalize-l"prove_eq.rs:70prove_normalize failedprove_normalize.rs:19rule "normalize-via-impl"prove_normalize.rs:39 (failed: empty_collection)
rule "symmetric"prove_eq.rs:40prove_eq failedprove_eq.rs:25rule "normalize-l"prove_eq.rs:70prove_normalize failedprove_normalize.rs:19rule "normalize-via-impl"prove_normalize.rs:39 (failed: empty_collection)