Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Negative coverage: is_local_trait_ref / local parameter / premise for_all(decls, env, assumptions, &goal.parameters[..*i], &is_not_downstream) => c2

Premise at line 224. Observed failure causes: failed_judgment.

local parameter
LineCoverageSource
218(i in 0 .. goal.parameters.len())
2196(is_local_parameter(decls, env, assumptions, &goal.parameters[*i]) => c1)
222N/A(let assumptions = c1.substitution().apply(assumptions))
223N/A(let goal = c1.substitution().apply(goal))
2241(for_all(decls, env, assumptions, &goal.parameters[..*i], &is_not_downstream) => c2)
──────── ("local parameter")
2269(is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2))

1 test failed proving this premise:


Source location: tests/coherence_orphan.rs:109

#[test]
fn uncovered_T() {
    FormalityTest::new(crates![crate core {
                trait CoreTrait<T> {}
            },
            crate foo {
                struct FooStruct {}
                impl<T> CoreTrait<FooStruct> for T {}
            }]).err(expect_test::expect![[r#"
            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: !ty_0, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

            crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19:1: no applicable rules for prove_normalize { p: !ty_0, assumptions: {}, env: Env { variables: [!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 <ty> CoreTrait <FooStruct> for ^ty0_0 { } }], 222)
                &goal.trait_id = CoreTrait"#]])
}
Failed proof tree