Negative coverage: is_not_downstream / fundamental type / premise for_all(decls, env, assumptions, parameters, &is_not_downstream) => c
Premise at line 270. Observed failure causes: failed_judgment.
fundamental type| Line | Coverage | Source |
|---|---|---|
| 269 | ✗ | (if is_fundamental(decls, name)) |
| 270 | 3 | (for_all(decls, env, assumptions, parameters, &is_not_downstream) => c) |
| ──────── ("fundamental type") | ||
| 272 | 2 | (is_not_downstream(decls, env, assumptions, RigidTy { name, parameters }) => c) |
3 tests failed proving this premise:
Source location: tests/coherence_orphan.rs:141 (all coverage from this test)
#[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"#]])
}Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:75check_coherence failedcoherence.rs:7args
rule "check_coherence"coherence.rs:20orphan_check failedcoherence.rs:30args
rule "orphan_check"coherence.rs:37prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "trait ref is local"prove_predicate.rs:136is_local_trait_ref failedis_local.rs:206args
rule "local parameter"is_local.rs:229is_not_downstream failedis_local.rs:236args
rule "fundamental type"is_local.rs:270failedcombinators.rs:63args
rulecombinators.rs:63is_not_downstream failedis_local.rs:236args
rule "via normalize"is_local.rs:276prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
Source location: tests/coherence_orphan.rs:172 (all coverage from this test)
#[test]
fn uncovered_nested_ref_T() {
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
},
crate foo {
struct FooStruct {}
impl<'a, T> CoreTrait<FooStruct> for &'a &'a 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 &!lt_1 !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 !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 &!lt_1 !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 &^lt0_0 ^ty0_1 where ^ty0_1 : ^lt0_0 { } }], 222)
name = &(shared)
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &!lt_1 !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 &^lt0_0 ^ty0_1 where ^ty0_1 : ^lt0_0 { } }], 222)
name = &(shared)
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &!lt_1 &!lt_1 !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 &^lt0_0 ^ty0_1 where ^ty0_1 : ^lt0_0 { } }], 222)
&goal.trait_id = CoreTrait"#]])
}Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:75check_coherence failedcoherence.rs:7args
rule "check_coherence"coherence.rs:20orphan_check failedcoherence.rs:30args
rule "orphan_check"coherence.rs:37prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "trait ref is local"prove_predicate.rs:136is_local_trait_ref failedis_local.rs:206args
rule "local parameter"is_local.rs:229is_not_downstream failedis_local.rs:236args
rule "fundamental type"is_local.rs:270failedcombinators.rs:63args
rulecombinators.rs:63is_not_downstream failedis_local.rs:236args
rule "fundamental type"is_local.rs:270failedcombinators.rs:63args
rulecombinators.rs:63is_not_downstream failedis_local.rs:236args
rule "via normalize"is_local.rs:276prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "rigid"is_local.rs:262 (failed: if_false)rule "via normalize"is_local.rs:276prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
Source location: tests/coherence_orphan.rs:254 (all coverage from this test)
#[test]
fn uncovered_ref_T() {
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
},
crate foo {
struct FooStruct {}
impl<T> CoreTrait<FooStruct> for &'static T {}
}]).err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_normalize.rs:22: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_normalize.rs:22:1: no applicable rules for prove_normalize { p: &' static !ty_0, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:22: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 "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 <ty> CoreTrait <FooStruct> for &' static ^ty0_0 { } }], 222)
name = &(shared)
crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &' static !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 &' static ^ty0_0 { } }], 222)
&goal.trait_id = CoreTrait"#]])
}Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:75check_coherence failedcoherence.rs:7args
rule "check_coherence"coherence.rs:20orphan_check failedcoherence.rs:30args
rule "orphan_check"coherence.rs:37prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "trait ref is local"prove_predicate.rs:136is_local_trait_ref failedis_local.rs:206args
rule "local parameter"is_local.rs:229is_not_downstream failedis_local.rs:236args
rule "fundamental type"is_local.rs:270failedcombinators.rs:63args
rulecombinators.rs:63is_not_downstream failedis_local.rs:236args
rule "via normalize"is_local.rs:276prove_normalize failedprove_normalize.rs:22args