Test uncovered_mut_ref_T

Source location: tests/coherence_orphan.rs:141

#[test]
fn uncovered_mut_ref_T() {
    FormalityTest::new(crates![crate core {
        trait CoreTrait<T> {}
    },
    crate foo {
        struct FooStruct {}
        impl<'a, T> CoreTrait<FooStruct> for &'a mut T where T: 'a {}
    }])
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: @ IsLocal(CoreTrait(&!lt_1 mut !ty_0, FooStruct)), via: !ty_0 : !lt_1, assumptions: {!ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: !ty_0, via: !ty_0 : !lt_1, assumptions: {!ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &!lt_1 mut !ty_0, via: !ty_0 : !lt_1, assumptions: {!ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: !ty_0, via: !ty_0 : !lt_1, assumptions: {!ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "rigid" at (is_local.rs) failed because
          condition evaluated to false: `!is_fundamental(decls, name)`
            decls = program([crate core { trait CoreTrait <ty, ty> { } }, crate foo { struct FooStruct { } impl <lt, ty> CoreTrait <FooStruct> for &^lt0_0 mut ^ty0_1 where ^ty0_1 : ^lt0_0 { } }], 222)
            name = &(mut)

        crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &!lt_1 mut !ty_0, via: !ty_0 : !lt_1, assumptions: {!ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "local trait" at (is_local.rs) failed because
          condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
            decls = program([crate core { trait CoreTrait <ty, ty> { } }, crate foo { struct FooStruct { } impl <lt, ty> CoreTrait <FooStruct> for &^lt0_0 mut ^ty0_1 where ^ty0_1 : ^lt0_0 { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

Rules proved (0)

This test records no positive coverage.

Premises failed (16)

The last column links to the premise’s page when the judgment view counts this failure against that premise. It does not when the premise is read as infallible, or when the failure was blamed inside a multi-line premise that carries no record on its own first line.

Proof trees

How to read this page