Test CoreTrait_for_CoreStruct_in_Foo
Source location: tests/coherence_orphan.rs:434
#[test]
fn CoreTrait_for_CoreStruct_in_Foo() {
FormalityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
crate foo {
impl CoreTrait for CoreStruct {}
}]).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 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 CoreStruct { } }], 222)
a = CoreStruct
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 CoreStruct { } }], 222)
&goal.trait_id = CoreTrait"#]])
}
Rules proved (0)
This test records no positive coverage.
Premises failed (11)
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.
| Judgment | Rule | Premise | All tests of this premise |
|---|---|---|---|
| check_coherence | check_coherence | for_all(trait_impl in current_crate_impls) (orph… (line 19, blamed at line 20) | not counted by the judgment view |
| orphan_check | orphan_check | scope(enter_universally(Env::default(), &impl_a.… (line 35, blamed at line 37) | not counted by the judgment view |
| check_all_crates | check all prefixes | for_all(i in 0..crates.len()) (let program = cra… (line 52, blamed at line 54) | not counted by the judgment view |
| check_crate | check crate | check_coherence(program, c) => () (line 75) | 20 tests |
| is_local_trait_ref | local trait | if decls.is_local_trait_id(&goal.trait_id) (line 216) | 12 tests |
| is_local_trait_ref | local parameter | is_local_parameter(decls, env, assumptions, &goa… (line 224) | 12 tests |
| is_local_parameter | local parameter | prove_normalize(decls, env, assumptions, goal) =… (line 305) | 12 tests |
| is_local_parameter | fundamental rigid type | if is_fundamental(decls, name) (line 314) | 7 tests |
| is_local_parameter | local rigid type | if decls.is_local_adt_id(a) (line 323) | 5 tests |
| prove_predicate | trait ref is local | is_local_trait_ref(decls, env, assumptions, trai… (line 136) | 12 tests |
| prove_predicate_list | some | prove_predicate(decls, env, assumptions, wc0) =>… (line 26) | 67 tests |
Proof trees
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: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)
rule "local trait"is_local.rs:216 (failed: if_false)