Positive coverage: is_not_downstream / rigid
rigid| Line | Coverage | Source |
|---|---|---|
| ──────── ("rigid") | ||
| 254 | 2 | (is_not_downstream(_decls, env, _assumptions, RigidTy { .. }) => Constraints::none(env)) |
2 tests exercised this rule:
Source location: tests/coherence_orphan.rs:98
#[test]
fn covered_VecT() {
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
struct Vec<T> {}
},
crate foo {
struct FooStruct {}
impl<T> CoreTrait<FooStruct> for Vec<T> {}
}])
.skip_execute()
.ok()
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (adt)mod.rs:201args
check_adt (check adt)adts.rs:27args
prove_wc_list (none)prove_wc_list.rs:21args
check_coherence (check_coherence)coherence.rs:24args
for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (adt)mod.rs:201args
check_adt (check adt)adts.rs:27args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (rigid)prove_eq.rs:48args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
check_coherence (check_coherence)coherence.rs:24args
for_allcoherence.rs:8for_allcoherence.rs:17args
for_allcoherence.rs:8for_allcoherence.rs:18args
overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20args
orphan_check (orphan_check)coherence.rs:39args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait ref is local)prove_wc.rs:147args
is_local_trait_ref (local parameter)is_local.rs:221args
is_local_parameter (local rigid type)is_local.rs:305args
for_allcombinators.rs:69is_not_downstream (rigid)is_local.rs:253args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: tests/coherence_orphan.rs:196
#[test]
fn CoreTraitLocal_for_AliasToKnown_in_Foo() {
// TODO: see comment in `orphan_check` from prev commit
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
trait Unit {
type Assoc : [];
}
impl<T> Unit for T {
type Assoc = ();
}
},
crate foo {
struct FooStruct {}
impl CoreTrait<FooStruct> for <() as Unit>::Assoc {}
}])
.skip_execute()
.ok()
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_alltraits.rs:9for_alltraits.rs:24args
check_trait_item (associated ty in trait)traits.rs:50args
check_associated_ty (check associated ty)traits.rs:93args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
for_allimpls.rs:13for_allimpls.rs:34args
check_trait_impl_item (associated ty value)impls.rs:145args
check_associated_ty_value (check_associated_ty_value)impls.rs:232args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (parameter well formed)prove_wc.rs:160args
prove_wf (tuples)prove_wf.rs:50args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (none)prove_wc_list.rs:21args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
check_coherence (check_coherence)coherence.rs:24args
for_allcoherence.rs:8for_allcoherence.rs:17args
for_allcoherence.rs:8for_allcoherence.rs:18args
overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20args
orphan_check (orphan_check)coherence.rs:39args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait ref is local)prove_wc.rs:147args
is_local_trait_ref (local trait)is_local.rs:208args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (adt)mod.rs:201args
check_adt (check adt)adts.rs:27args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
check_coherence (check_coherence)coherence.rs:24args
for_allcoherence.rs:8for_allcoherence.rs:17args
for_allcoherence.rs:8for_allcoherence.rs:18args
overlap_check (skip_different_trait)coherence.rs:84
for_allcoherence.rs:18args
overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20args
orphan_check (orphan_check)coherence.rs:39args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait ref is local)prove_wc.rs:147args
is_local_trait_ref (local parameter)is_local.rs:221args
is_local_parameter (local rigid type)is_local.rs:305args
for_allcombinators.rs:69is_not_downstream (via normalize)is_local.rs:261args
prove_normalize (normalize-via-impl)prove_normalize.rs:50args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
is_not_downstream (rigid)is_local.rs:253args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args