Negative coverage: check_crate_item / trait / premise check_trait(program, Env::default(), v, crate_id) => ()

Premise at line 172. Observed failure causes: failed_judgment.

4 tests failed proving this premise:

Source location: tests/basic_tests.rs:34

#[test]
fn hello_world_fail() {
    FormalityTest::new(crates![crate Foo {
                trait Foo<T> where T: Bar<Self> {}

                trait Bar<T> where T: Baz {}

                trait Baz {}
            }]).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(Bar(!ty_0, !ty_1)), via: Bar(!ty_0, !ty_1), assumptions: {Bar(!ty_0, !ty_1)}, 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: Baz(!ty_1), via: Bar(!ty_0, !ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], 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()`"#]])
}

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

Source location: tests/basic_tests.rs:303

Source location: tests/basic_tests.rs:316

#[test]
fn trait_items_with_duplicate_associated_type_names() {
    FormalityTest::new(crates![crate core {
        trait A {
            type Assoc : [];
            type Assoc : [];
        }
    }])
    .err(expect_test::expect![[r#"
            the rule "check trait" at (traits.rs) failed because
              the associated type name `Assoc` is defined multiple times"#]]);
}