Negative coverage: prove_normalize / normalize-via-impl / premise decl in decls.alias_eq_decls(&a.name)
Premise at line 42. Observed failure causes: empty_collection.
normalize-via-impl| Line | Coverage | Source |
|---|---|---|
| 42 | 1 | (decl in decls.alias_eq_decls(&a.name)) |
| 43 | ✗ | (scope(enter_existentially_with_constraints(env, &decl.binder) => (env, AliasEqDeclBoundData { alias: AliasTy { name, parameters }, ty, where_clause })) with(ty, c) (assert a.name == *name) (prove(decls, env, assumptions, Predicates::all_eq(&a.parameters, ¶meters)) => c) (prove_after(decls, c, assumptions, &where_clause) => c) (let ty = c.substitution().apply(ty))) |
| ──────── ("normalize-via-impl") | ||
| 50 | 55 | (prove_normalize(decls, env, assumptions, Ty::AliasTy(a)) => Constrained(ty, c)) |
1 test failed proving this premise:
Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:41 (all coverage from this test)
#[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_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_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_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_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_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_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_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:57args
ruletest_util.rs:57prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "forall"prove_predicate.rs:35prove_predicate failedprove_predicate.rs:22args
rule "implies"prove_predicate.rs:41prove_predicate failedprove_predicate.rs:22args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-impl"prove_normalize.rs:42 (failed: empty_collection)
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:69prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:69prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-impl"prove_normalize.rs:42 (failed: empty_collection)
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-impl"prove_normalize.rs:42 (failed: empty_collection)