Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: check_adt / check adt

check adt
LineCoverageSource
182(check_adt_variant_names_unique(adt) => ())
19✗(scope(enter_universally(Env::default(), &adt.binder) => (env, AdtBoundData { where_clauses, variants })) with()
(prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ())
(for_all(variant in variants)
(let Variant { fields, .. } = variant)
(for_all(field in fields)
(let Field { ty, .. } = field)
(prove_goal(program, env, where_clauses, AtomicPredicate::well_formed(ty)) => ()))))
──────── ("check adt")
2759(check_adt(program, adt) => ())

59 tests exercised this rule:

Source location: src/test_util.rs:516 (all coverage from this test)

#[test]
fn rustc_expectation_is_independent_of_borrowck_modes() {
    let before = rustc_runs();
    FormalityTest::new(NLL_ONLY_ERROR)
        .rustc_err(expect_test::expect![[r#"
            error[E0499]: cannot borrow `*m` as mutable more than once at a time
             --> lib.rs
              |
            3 | pub fn foo<'a00>(mut m: &'a00 mut Map) -> &'a00 mut Map {
              |            ---- lifetime `'a00` defined here
            4 |     {
            5 |         let mut n: &'_ mut Map = &mut *m;
              |                                  ------- first mutable borrow occurs here
            6 |         if false {
            7 |             return n;
              |                    - returning this value requires that `*m` is borrowed for `'a00`
            8 |         } else {
            9 |             let mut o: &'_ mut Map = &mut *m;
              |                                      ^^^^^^^ second mutable borrow occurs here

            For more information about this error, try `rustc --explain E0499`.
            error: could not compile `Foo` (lib) due to 1 previous error
        "#]])
        .borrowck_err(BorrowCheckFailure::Nll, expect_test::expect![[r#"
            the rule "borrow of disjoint places" at (nll.rs) failed because
              condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
                &loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
                &access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target

            the rule "loan_cannot_outlive" at (nll.rs) failed because
              condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
                outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
                &lifetime.upcast() = !lt_1

            the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
              condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
              {
                  Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
                  {
                      Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
                      Lt::Variable(Variable::ExistentialVar(_)) => true,
                      Lt::Variable(Variable::BoundVar(_)) =>
                      panic!("cannot outlive a bound var"), Lt::Erased => true,
                  }, Parameter::Const(_) => panic!("cannot outlive a constant"),
              })`

            the rule "write-indirect" at (nll.rs) failed because
              pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`

            the rule "write-indirect" at (nll.rs) failed because
              condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
                place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
                place_loaned_ref = m : &!lt_1 mut Map"#]]);
    assert_eq!(rustc_runs() - before, 1);
}
Proof tree
… (200 of 3742 nodes shown)

Source location: tests/basic_tests.rs:209 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_enum_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        enum E where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:239 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_struct_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        struct S<T> where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:457 (all coverage from this test)

Proof tree

Source location: tests/borrowck.rs:214 (all coverage from this test)

fn foo() -> Datum {
    let x: Datum = Datum { value: 0_u32 };
    let y: Datum = x;
    x = Datum { value: 1_u32 };
    let z: Datum = x;
    return z;
}
Proof tree
… (200 of 3504 nodes shown)

Source location: tests/borrowck.rs:495 (all coverage from this test)

fn foo() -> Datum {
    let x: Pair = Pair {
        first: Datum { value: 1_u32 },
        second: Datum { value: 2_u32 },
    };
    let a: Datum = x.first;
    let b: Datum = x.second;
    return b;
}
Proof tree
… (200 of 3542 nodes shown)

Source location: tests/borrowck.rs:2470 (all coverage from this test)

fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
    exists<'r0, 'r1> {
        let n: &'r0 mut Map = &'r0 mut *m;
        if true {
            return n;
        } else {
            let o: &'r1 mut Map = &'r1 mut *m;
            return o;
        }
    }
}
Proof tree
… (200 of 3742 nodes shown)

Source location: tests/borrowck.rs:2690 (all coverage from this test)

fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
    exists<'r0, 'r1> {
        let n: &'r0 mut Map = &'r0 mut *m;
        if true {
        } else {
        }
        let o: &'r1 mut Map = &'r1 mut *m;
        return o;
    }
}
Proof tree
… (200 of 3713 nodes shown)

Source location: tests/borrowck.rs:2827 (all coverage from this test)

fn min_problem_case_4<'a>(list: &'a mut Map, list2: &'a mut Map) -> u32 {
    exists<'r0> {
        let num: &'r0 mut u32 = &'r0 mut (*list).value;
        list = &'a mut *list2;
        num;
        return 0_u32;
    }
}
Proof tree
… (200 of 3676 nodes shown)

Source location: tests/borrowck.rs:3288 (all coverage from this test)

fn foo<'a>(m: &'a mut Map) -> &'a mut Map {
    exists<'r0, 'r1> {
        let n: &'r0 mut Map = &'r0 mut *m;
        if false {
            return n;
        } else {
            let o: &'r1 mut Map = &'r1 mut *m;
            return o;
        }
    }
}
Proof tree
… (200 of 3742 nodes shown)

Source location: tests/borrowck.rs:3568 (all coverage from this test)

fn foo() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let p: Point = Point { x: 0_u32, y: 0_u32 };
        let b1: &'r0 mut u32 = &'r1 mut p.x;
        let b2: &'r2 mut u32 = &'r3 mut p.y;
        *b1 = 1_u32;
        *b2 = 2_u32;
        return 0_u32;
    }
}

Proof trees omitted for the remaining 49 tests; each one is on its test’s page in Coverage by test.

Source location: tests/borrowck.rs:4167 (all coverage from this test)

fn remove_last_node_recursive<'a>(node: &'a mut List) -> u32 {
    exists<'r0> {
        let next: &'r0 mut List = next_of::<'r0>(&'r0 mut *node);
        if true {
            remove_last_node_recursive::<'r0>(next);
        } else {
            *node = List { value: 0_u32 };
        }
        return 0_u32;
    }
}

Source location: tests/borrowck.rs:4214 (all coverage from this test)

fn remove_last_node_iterative<'a>(node: &'a mut List) -> u32 {
    exists<'r0, 'r1> {
        let cursor: &'r0 mut List = &'r0 mut *node;
        'l: loop {
            let next: &'r1 mut List = &'r1 mut *cursor;
            if true {
                cursor = next;
            } else {
                break 'l;
            }
        }
        *cursor = List { value: 0_u32 };
        return 0_u32;
    }
}

Source location: tests/borrowck.rs:4276 (all coverage from this test)

fn no_control_flow() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let b: X = X { value: 0_u32 };
        let p: &'r0 mut X = &'r1 mut b;
        'l: loop {
            let now: &'r2 mut X = &'r2 mut *p;
            if true {
                let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
                p = next;
            } else {
                break 'l;
            }
        }
        return 0_u32;
    }
}

Source location: tests/borrowck.rs:4326 (all coverage from this test)

fn conditional() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let b: X = X { value: 0_u32 };
        let p: &'r0 mut X = &'r1 mut b;
        'l: loop {
            let now: &'r2 mut X = &'r2 mut *p;
            if true {
                if true {
                    let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
                    p = next;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return 0_u32;
    }
}

Source location: tests/borrowck.rs:4415 (all coverage from this test)

fn conditional_with_indirection() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let b: X = X { value: 0_u32 };
        let p: &'r0 mut X = &'r1 mut b;
        'l: loop {
            let now: &'r2 mut X = &'r2 mut *p;
            if true {
                if true {
                    let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *p);
                    p = next;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return 0_u32;
    }
}

Source location: tests/borrowck.rs:4467 (all coverage from this test)

fn to_refs<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        'l: loop {
            result = &'r0 mut (*list).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
                list = n;
            } else {
                return result;
            }
        }
    }
}

Source location: tests/borrowck.rs:4502 (all coverage from this test)

fn to_refs2<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        'l: loop {
            result = &'r0 mut (*list).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
                list = n;
            } else {
                break 'l;
            }
        }
        return result;
    }
}

Source location: tests/borrowck.rs:4549 (all coverage from this test)

fn to_refs3<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        let cursor: &'a mut List = &'a mut *list;
        'l: loop {
            result = &'r0 mut (*cursor).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*cursor).next);
                cursor = n;
            } else {
                return result;
            }
        }
    }
}

Source location: tests/borrowck.rs:4592 (all coverage from this test)

fn next<'a>(d: &'a mut Decoder) -> &'a u32 {
    exists<'r0, 'r1> {
        'l: loop {
            let buf: &'r0 u32 = fill_buf::<'r0>(&'r0 mut (*d).buf_read);
            let s: &'r1 u32 = decode::<'r1>(buf);
            if true {
                return s;
            } else {
            }
        }
    }
}

Source location: tests/borrowck.rs:4715 (all coverage from this test)

fn next<'s>(f: &'s mut Filter) -> &'s mut u32 {
    exists<'r0, 'r1, 'r2> {
        'l: loop {
            let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter);
            if true {
                let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item);
                if keep {
                    return item;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return no_item::<'s>();
    }
}

Source location: tests/borrowck.rs:4831 (all coverage from this test)

fn use_it<'a, 'b>() -> u32 {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}

Source location: tests/borrowck.rs:4896 (all coverage from this test)

fn use_it_but_its_the_same_region<'a, 'b>() -> u32 where 'a: 'b, 'b: 'a {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}

Source location: tests/borrowck.rs:4970 (all coverage from this test)

fn f() -> u32 {
    exists<'r0> {
        let v: u32 = 0_u32;
        let w: Wrapper<'r0> = Wrapper::<'r0> { value: &'r0 v };
        return *w.value;
    }
}

Source location: tests/codegen.rs:236 (all coverage from this test)

fn main() -> () {
    let p: Pair = Pair { x: 10_i32, y: 20_i32 };
    println!(p.x);
    println!(p.y);
}

Source location: tests/codegen.rs:358 (all coverage from this test)

fn main() -> () {
    let w: Wrapper<i32> = Wrapper::<i32> { val: 42_i32 };
    println!(w.val);
}

Source location: tests/codegen.rs:374 (all coverage from this test)

fn main() -> () {
    let p: Pair = Pair { x: 10_i32, y: 20_i32 };
    exists<'a> {
        let r: & 'a i32 = & 'a p.x;
        println!(*r);
    }
}

Source location: tests/codegen.rs:391 (all coverage from this test)

fn main() -> () {
    let p: Pair = Pair { x: 10_i32, y: 20_i32 };
    exists<'a> {
        let r: & 'a Pair = & 'a p;
        println!((*r).x);
        println!((*r).y);
    }
}

Source location: tests/codegen.rs:628 (all coverage from this test)

fn main() -> () {
    println!(identity::<S>(7_u32));
}

Source location: tests/codegen.rs:693 (all coverage from this test)

fn main() -> () {
    let s: S = S { b: second(), a: first() };
    println!(s.a);
    println!(s.b);
}

Source location: tests/codegen.rs:721 (all coverage from this test)

fn main() -> () {
    let w: Wrap<<S as Value>::Item> = Wrap::<<S as Value>::Item> { value: 7_u32 };
    println!(w.value);
}

Source location: tests/codegen.rs:798 (all coverage from this test)

fn main() -> () {
    let x: <S as Outer>::Item = 7_u32;
    println!(x);
}

Source location: tests/codegen.rs:927 (all coverage from this test)

fn main() -> () {
    println!(identity::<Number>(7_u32));
    println!(identity::<Flag>(true));
    println!(identity::<Number>(9_u32));
}

Source location: tests/codegen.rs:1102 (all coverage from this test)

fn main() -> () {
    let p: Pair = Pair { a: 1_u32, b: 10_u32 };
    p.b += p.a;
    println!(p.b);
}

Source location: tests/codegen.rs:1132 (all coverage from this test)

fn main() -> () {
    let p: Pair = Pair { a: 2_u32, b: 3_u32 };
    p.b *= p.a + 4_u32;
    println!(p.b);
    println!(p.a);
}

Source location: tests/coherence_orphan.rs:85 (all coverage from this test)

#[test]
fn mirror_FooStruct() {
    FormalityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Mirror {
            type Assoc : [];
        }

        impl<T> Mirror for T {
            type Assoc = T;
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Mirror>::Assoc {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/coherence_orphan.rs:99 (all coverage from this test)

#[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()
}

Source location: tests/coherence_orphan.rs:114 (all coverage from this test)

fn main() -> () {}
}])
tc_ok()
)
}

#[test]
ed_nested_mut_ref_VecT() {
alityTest::new(crates![crate core {
trait CoreTrait<T> {}
struct Vec<T> { value: T }
},
e foo {
struct FooStruct {}
impl<'a, T> CoreTrait<FooStruct> for &'a &'a mut Vec<T> where T: 'a {}
fn main() -> () {}
}])
tc_ok()
)
}

#[test]
ered_mut_ref_T() {
alityTest::new(crates![crate core {
trait CoreTrait<T> {}
},
e foo {
struct FooStruct {}
impl<'a, T> CoreTrait<FooStruct> for &'a mut T where T: 'a {}
}])
(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"#]])
}

#[test]
ered_nested_ref_T() {
alityTest::new(crates![crate core {
trait CoreTrait<T> {}
},
e foo {
struct FooStruct {}
impl<'a, T> CoreTrait<FooStruct> for &'a &'a T where T: 'a {}
}])
(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"#]])
}

#[test]
ointer_is_not_fundamental() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl CoreTrait for *mut FooStruct {}
}])
p_execute()
(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> { } }, crate foo { struct FooStruct { } impl CoreTrait for *mut FooStruct { } }], 222)
    name = * mut

crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: *mut FooStruct, 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> { } }, crate foo { struct FooStruct { } impl CoreTrait for *mut FooStruct { } }], 222)
    &goal.trait_id = CoreTrait"#]])
}

#[test]
ered_T() {
alityTest::new(crates![crate core {
        trait CoreTrait<T> {}
    },
    crate foo {
        struct FooStruct {}
        impl<T> CoreTrait<FooStruct> for 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: !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 ^ty0_0 { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
ered_ref_T() {
alityTest::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"#]])
}

#[test]
ooStruct_is_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl CoreTrait for &'static FooStruct {}
impl CoreTrait for &'static mut FooStruct {}
fn main() -> () {}
}])
tc_ok()
)
}

#[test]
d_ref_FooStruct_is_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl<'a, 'b> CoreTrait for &'a &'b mut FooStruct where 'b: 'a {}
fn main() -> () {}
}])
tc_ok()
)
}

#[test]
oreign_wrapper_of_local_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct ForeignWrapper<T> { value: T }
},
e foo {
struct FooStruct {}
impl<'a> CoreTrait for &'a ForeignWrapper<FooStruct> {}
}])
tc_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
)
(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"#]])
}

#[test]
oreStruct_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
e foo {
impl CoreTrait for &'static CoreStruct {}
}])
tc_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
)
(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"#]])
}

#[test]
_to_unit() {
alityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Unit>::Assoc {}
    }]).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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            name = tuple(0)

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: (), 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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
rait_for_CoreStruct_in_Foo() {
alityTest::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"#]])
}

#[test]
raitLocal_for_AliasToKnown_in_Foo() {
ODO: see comment in `orphan_check` from prev commit
alityTest::new(crates![crate core {
trait CoreTrait<T> {}

trait Unit {
    type Assoc : [];
}

Source location: tests/coherence_orphan.rs:129 (all coverage from this test)

fn main() -> () {}
}])
tc_ok()
)
}

#[test]
ered_mut_ref_T() {
alityTest::new(crates![crate core {
trait CoreTrait<T> {}
},
e foo {
struct FooStruct {}
impl<'a, T> CoreTrait<FooStruct> for &'a mut T where T: 'a {}
}])
(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"#]])
}

#[test]
ered_nested_ref_T() {
alityTest::new(crates![crate core {
trait CoreTrait<T> {}
},
e foo {
struct FooStruct {}
impl<'a, T> CoreTrait<FooStruct> for &'a &'a T where T: 'a {}
}])
(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"#]])
}

#[test]
ointer_is_not_fundamental() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl CoreTrait for *mut FooStruct {}
}])
p_execute()
(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> { } }, crate foo { struct FooStruct { } impl CoreTrait for *mut FooStruct { } }], 222)
    name = * mut

crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: *mut FooStruct, 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> { } }, crate foo { struct FooStruct { } impl CoreTrait for *mut FooStruct { } }], 222)
    &goal.trait_id = CoreTrait"#]])
}

#[test]
ered_T() {
alityTest::new(crates![crate core {
        trait CoreTrait<T> {}
    },
    crate foo {
        struct FooStruct {}
        impl<T> CoreTrait<FooStruct> for 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: !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 ^ty0_0 { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
ered_ref_T() {
alityTest::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"#]])
}

#[test]
ooStruct_is_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl CoreTrait for &'static FooStruct {}
impl CoreTrait for &'static mut FooStruct {}
fn main() -> () {}
}])
tc_ok()
)
}

#[test]
d_ref_FooStruct_is_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl<'a, 'b> CoreTrait for &'a &'b mut FooStruct where 'b: 'a {}
fn main() -> () {}
}])
tc_ok()
)
}

#[test]
oreign_wrapper_of_local_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct ForeignWrapper<T> { value: T }
},
e foo {
struct FooStruct {}
impl<'a> CoreTrait for &'a ForeignWrapper<FooStruct> {}
}])
tc_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
)
(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"#]])
}

#[test]
oreStruct_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
e foo {
impl CoreTrait for &'static CoreStruct {}
}])
tc_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
)
(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"#]])
}

#[test]
_to_unit() {
alityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Unit>::Assoc {}
    }]).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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            name = tuple(0)

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: (), 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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
rait_for_CoreStruct_in_Foo() {
alityTest::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"#]])
}

#[test]
raitLocal_for_AliasToKnown_in_Foo() {
ODO: see comment in `orphan_check` from prev commit
alityTest::new(crates![crate core {
trait CoreTrait<T> {}

trait Unit {
    type Assoc : [];
}

Source location: tests/coherence_orphan.rs:286 (all coverage from this test)

fn main() -> () {}
}])
tc_ok()
)
}

#[test]
d_ref_FooStruct_is_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl<'a, 'b> CoreTrait for &'a &'b mut FooStruct where 'b: 'a {}
fn main() -> () {}
}])
tc_ok()
)
}

#[test]
oreign_wrapper_of_local_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct ForeignWrapper<T> { value: T }
},
e foo {
struct FooStruct {}
impl<'a> CoreTrait for &'a ForeignWrapper<FooStruct> {}
}])
tc_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
)
(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"#]])
}

#[test]
oreStruct_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
e foo {
impl CoreTrait for &'static CoreStruct {}
}])
tc_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
)
(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"#]])
}

#[test]
_to_unit() {
alityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Unit>::Assoc {}
    }]).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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            name = tuple(0)

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: (), 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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
rait_for_CoreStruct_in_Foo() {
alityTest::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"#]])
}

#[test]
raitLocal_for_AliasToKnown_in_Foo() {
ODO: see comment in `orphan_check` from prev commit
alityTest::new(crates![crate core {
trait CoreTrait<T> {}

trait Unit {
    type Assoc : [];
}

Source location: tests/coherence_orphan.rs:300 (all coverage from this test)

fn main() -> () {}
}])
tc_ok()
)
}

#[test]
oreign_wrapper_of_local_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct ForeignWrapper<T> { value: T }
},
e foo {
struct FooStruct {}
impl<'a> CoreTrait for &'a ForeignWrapper<FooStruct> {}
}])
tc_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
)
(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"#]])
}

#[test]
oreStruct_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
e foo {
impl CoreTrait for &'static CoreStruct {}
}])
tc_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
)
(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"#]])
}

#[test]
_to_unit() {
alityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Unit>::Assoc {}
    }]).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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            name = tuple(0)

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: (), 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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
rait_for_CoreStruct_in_Foo() {
alityTest::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"#]])
}

#[test]
raitLocal_for_AliasToKnown_in_Foo() {
ODO: see comment in `orphan_check` from prev commit
alityTest::new(crates![crate core {
trait CoreTrait<T> {}

trait Unit {
    type Assoc : [];
}

Source location: tests/coherence_orphan.rs:472 (all coverage from this test)

#[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()
}

Source location: tests/coherence_overlap.rs:237 (all coverage from this test)

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        #![feature(negative_impls)]
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/coherence_overlap.rs:587 (all coverage from this test)

#[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()
}

Source location: tests/drop.rs:23 (all coverage from this test)

Source location: tests/drop.rs:43 (all coverage from this test)

Source location: tests/drop.rs:61 (all coverage from this test)

Source location: tests/drop.rs:108 (all coverage from this test)

Source location: tests/drop.rs:128 (all coverage from this test)

Source location: tests/field_projections.rs:17 (all coverage from this test)

fn test(ptr: Ptr) -> () {
    let x: () = *ptr;
}

Source location: tests/mir_typeck.rs:259 (all coverage from this test)

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1_u32, is_true: false };
    v2.value = 2_u32;
    return v1;
}

Source location: tests/mir_typeck.rs:276 (all coverage from this test)

fn foo() -> () {
    let s1: S1<u8>;
}

Source location: tests/mir_typeck.rs:1142 (all coverage from this test)

fn foo<'a>(v1: &'a Pair) -> u32 {
    exists<'r0> {
        let v2: u32 = (*v1).value;
        return v2;
    }
}

Source location: tests/references.rs:36 (all coverage from this test)

Source location: tests/well_formed_struct.rs:17 (all coverage from this test)

fn main() -> () {
    exists<'y> {
        let a: u32 = 22_u32;
        let f: Foo<'y> = Foo::<'y> { y: &'y a };
    }
}

Source location: tests/well_formed_trait_ref.rs:19 (all coverage from this test)

#[test]
fn dependent_where_clause() {
    FormalityTest::new(crates![crate foo {
        trait Trait1 {}

        trait Trait2 {}

        struct S1<T> where T: Trait1 {
            dummy: T,
        }

        struct S2<T> where T: Trait1, S1<T> : Trait2 {
            dummy: T,
        }
    }])
    .skip_execute()
    .ok()
}

Source location: tests/well_formed_trait_ref.rs:56 (all coverage from this test)

#[test]
fn lifetime_param() {
    FormalityTest::new(crates![crate foo {
        trait Trait1<'a> {}

        struct S1 {}

        struct S2<'a> where S1: Trait1<'a> {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/well_formed_trait_ref.rs:71 (all coverage from this test)

#[test]
fn static_lifetime_param() {
    FormalityTest::new(crates![crate foo {
        trait Trait1<'a> {}

        struct S1 {}

        impl Trait1<'static> for S1 {}

        struct S2 where S1: Trait1<'static> {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/well_formed_trait_ref.rs:86 (all coverage from this test)

#[test]
fn const_param() {
    FormalityTest::new(crates![crate foo {
        trait Trait1<const C> where type_of_const C is u32 {}

        struct S1 {}

        impl Trait1<u32(3)> for S1 {}

        struct S2 where S1: Trait1<u32(3)> {}
    }])
    .skip_execute()
    .ok()
}

How to read this page