Negative coverage: prove_via / forall / premise prove_via(decls, env, assumptions, via1, goal) => c

Premise at line 50. Observed failure causes: failed_judgment.

1 test failed proving this premise:

Source location: tests/basic_tests.rs:85

#[test]
fn basic_where_clauses_fail() {
    FormalityTest::new(crates![crate core {
                #![feature(non_lifetime_binders)]
                trait A<T> where T: B { }

                trait B { }

                trait WellFormed where for<T> u32: A<T> { }
            }]).err(expect_test::expect![[r#"
            crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: @ WellFormedTraitRef(A(u32, !ty_1)), via: A(u32, ?ty_2), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_1, ?ty_2], 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: B(!ty_0), via: A(u32, ?ty_1), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

            the rule "trait implied bound" at (prove_wc.rs) failed because
              expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}