Negative coverage: is_local_parameter / fundamental rigid type / premise for_all(decls, env, assumptions, type_params, &is_local_parameter) => c
Premise at line 316. Observed failure causes: failed_judgment.
fundamental rigid type| Line | Coverage | Source |
|---|---|---|
| 314 | 7 | (if is_fundamental(decls, name)) |
| 315 | N/A | (let type_params: Vec<Parameter> = parameters.iter().filter(|p| !matches!(p, Parameter::Lt(_))).cloned().collect()) |
| 316 | 5 | (for_all(decls, env, assumptions, type_params, &is_local_parameter) => c) |
| ──────── ("fundamental rigid type") | ||
| 318 | 2 | (is_local_parameter(decls, env, assumptions, RigidTy { name, parameters }) => c) |
5 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:224is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:316is_local_parameter failedis_local.rs:293args
rule "local parameter"is_local.rs:305prove_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:224is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:316is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:316is_local_parameter failedis_local.rs:293args
rule "local parameter"is_local.rs:305prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "local parameter"is_local.rs:305prove_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:224is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:316is_local_parameter failedis_local.rs:293args
rule "local parameter"is_local.rs:305prove_normalize failedprove_normalize.rs:22args
Source location: tests/coherence_orphan.rs:329 (all coverage from this test)
#[test]
fn ref_foreign_wrapper_of_local_is_not_local() {
FormalityTest::new(crates![crate core {
trait CoreTrait {}
struct ForeignWrapper<T> { value: T }
},
crate foo {
struct FooStruct {}
impl<'a> CoreTrait for &'a ForeignWrapper<FooStruct> {}
}])
.rustc_err(expect_test::expect![[r#"
error[E0117]: only traits defined in the current crate can be implemented for arbitrary types
--> lib.rs
|
5 | impl<'a00> CoreTrait for &'a00 ForeignWrapper<FooStruct> {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^-------------------------------
| |
| `mycore::ForeignWrapper` is not defined in the current crate
|
= note: impl doesn't have any local type before any uncovered type parameters
= note: for more information see https://doc.rust-lang.org/reference/items/implementations.html#orphan-rules
= note: define and implement a trait or new type instead
For more information about this error, try `rustc --explain E0117`.
error: could not compile `foo` (lib) due to 1 previous error
"#]])
.err(expect_test::expect![[r#"
the rule "fundamental rigid type" at (is_local.rs) failed because
condition evaluated to false: `is_fundamental(decls, name)`
decls = program([crate core { trait CoreTrait <ty> { } struct ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
name = (adt ForeignWrapper)
crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: ForeignWrapper<FooStruct>, assumptions: {}, env: Env { variables: [!lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "local rigid type" at (is_local.rs) failed because
condition evaluated to false: `decls.is_local_adt_id(a)`
decls = program([crate core { trait CoreTrait <ty> { } struct ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
a = ForeignWrapper
crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &!lt_0 ForeignWrapper<FooStruct>, assumptions: {}, env: Env { variables: [!lt_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> { } struct ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 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:224is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:316is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:314 (failed: if_false)rule "local parameter"is_local.rs:305prove_normalize failedprove_normalize.rs:22args
rule "local rigid type"is_local.rs:323 (failed: if_false)
Source location: tests/coherence_orphan.rs:375 (all coverage from this test)
#[test]
fn ref_CoreStruct_is_not_local() {
FormalityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
crate foo {
impl CoreTrait for &'static CoreStruct {}
}])
.rustc_err(expect_test::expect![[r#"
error[E0117]: only traits defined in the current crate can be implemented for arbitrary types
--> lib.rs
|
3 | impl CoreTrait for &'static CoreStruct {}
| ^^^^^^^^^^^^^^^^^^^-------------------
| |
| `mycore::CoreStruct` is not defined in the current crate
|
= note: impl doesn't have any local type before any uncovered type parameters
= note: for more information see https://doc.rust-lang.org/reference/items/implementations.html#orphan-rules
= note: define and implement a trait or new type instead
For more information about this error, try `rustc --explain E0117`.
error: could not compile `foo` (lib) due to 1 previous error
"#]])
.err(expect_test::expect![[r#"
the rule "fundamental rigid type" at (is_local.rs) failed because
condition evaluated to false: `is_fundamental(decls, name)`
decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for &' static CoreStruct { } }], 222)
name = (adt CoreStruct)
crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "local rigid type" at (is_local.rs) failed because
condition evaluated to false: `decls.is_local_adt_id(a)`
decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for &' static CoreStruct { } }], 222)
a = CoreStruct
crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &' static CoreStruct, assumptions: {}, env: Env { variables: [], 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> { } struct CoreStruct { } }, crate foo { impl CoreTrait for &' static CoreStruct { } }], 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:224is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:316is_local_parameter failedis_local.rs:293args
rule "fundamental rigid type"is_local.rs:314 (failed: if_false)rule "local parameter"is_local.rs:305prove_normalize failedprove_normalize.rs:22args
rule "local rigid type"is_local.rs:323 (failed: if_false)