Positive coverage: prove_wf / aliases
aliases| Line | Coverage | Source |
|---|---|---|
| 83 | ✗ | (prove_alias_wf(decls, env, assumptions, name, parameters) => c) |
| ──────── ("aliases") | ||
| 85 | 1 | (prove_wf(decls, env, assumptions, AliasTy { name, parameters }) => c) |
1 test exercised this rule:
Source location: tests/coherence_overlap.rs:307
#[test]
fn is_local_unknowable_trait_ref() {
FormalityTest::new(crates![crate core {
trait Project {
type Assoc: [];
}
impl<T> Project for T {
type Assoc = T;
}
trait Foo<U> { }
},
crate foo {
struct LocalType {}
trait Overlap<U> {}
impl<T, U> Overlap<U> for T
where
<T as Project>::Assoc: Foo<U> {}
impl<T> Overlap<LocalType> for () {}
}])
.skip_execute()
.ok()
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24for_alltraits.rs:9for_alltraits.rs:24check_trait_item (associated ty in trait)traits.rs:50check_associated_ty (check associated ty)traits.rs:93prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (symmetric)prove_eq.rs:41prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-universal)prove_eq.rs:143
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79for_allimpls.rs:13for_allimpls.rs:34check_trait_impl_item (associated ty value)impls.rs:145check_associated_ty_value (check_associated_ty_value)impls.rs:232prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (parameter well formed)prove_wc.rs:162prove_wf (universal variables)prove_wf.rs:30
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_wc_list (none)prove_wc_list.rs:24
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
check_coherence (check_coherence)coherence.rs:24for_allcoherence.rs:8for_allcoherence.rs:17for_allcoherence.rs:8for_allcoherence.rs:18overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20orphan_check (orphan_check)coherence.rs:39prove_wc_list (some)prove_wc_list.rs:31prove_wc (trait ref is local)prove_wc.rs:149is_local_trait_ref (local trait)is_local.rs:212
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (adt)mod.rs:186check_adt (check adt)adts.rs:27prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (some)prove_wc_list.rs:31prove_wc (trait well formed)prove_wc.rs:143for_allcombinators.rs:69prove_wf (aliases)prove_wf.rs:84for_allcombinators.rs:69prove_wc_list (some)prove_wc_list.rs:31prove_wc (parameter well formed)prove_wc.rs:162prove_wf (universal variables)prove_wf.rs:30
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
for_allcombinators.rs:69prove_wf (universal variables)prove_wf.rs:30
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (symmetric)prove_eq.rs:41prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-universal)prove_eq.rs:143
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (symmetric)prove_eq.rs:41prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-universal)prove_eq.rs:143
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (assumption - predicate)prove_wc.rs:51prove_via (predicate-congruence-axiom)prove_via.rs:32prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
check_coherence (check_coherence)coherence.rs:24for_allcoherence.rs:8for_allcoherence.rs:17for_allcoherence.rs:8for_allcoherence.rs:18overlap_check (skip_different_trait)coherence.rs:84
for_allcoherence.rs:18overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:18overlap_check (not_goal)coherence.rs:135
for_allcoherence.rs:17for_allcoherence.rs:8for_allcoherence.rs:18overlap_check (skip_different_trait)coherence.rs:84
for_allcoherence.rs:18overlap_check (not_goal)coherence.rs:135
for_allcoherence.rs:18overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20orphan_check (orphan_check)coherence.rs:39prove_wc_list (some)prove_wc_list.rs:31prove_wc (trait ref is local)prove_wc.rs:149is_local_trait_ref (local trait)is_local.rs:212
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
for_allcoherence.rs:20orphan_check (orphan_check)coherence.rs:39prove_wc_list (some)prove_wc_list.rs:31prove_wc (trait ref is local)prove_wc.rs:149is_local_trait_ref (local trait)is_local.rs:212
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24