Prototype of `GhostDeref` trait at the type level

ghost_proto.rs

#![allow(dead_code)]
#![allow(unused_variables)]

trait GhostDeref {
    /* ghost */ fn ghost_deref(self) -> Self::Target;
    type Target;
}

struct Snap<T> { p: core::marker::PhantomData<(T,)>, }

impl<T> Clone for Snap<T> {
    fn clone(&self) -> Self { todo!() }
}
impl<T> Copy for Snap<T> { }
impl<T> Snap<T> {
    fn new(t: T) -> Self { todo!() }
}

struct Tracked<T> { p: core::marker::PhantomData<(T,)>, }
impl<T> Tracked<T> {
    fn new(t: T) -> Self { todo!() }
}

impl<T> GhostDeref for Snap<T> {
    type Target = T;
    fn ghost_deref(self) -> Self::Target { todo!() }
}

impl<T> GhostDeref for Tracked<T> {
    type Target = T;
    fn ghost_deref(self) -> Self::Target { todo!() }
}

struct PointsTo { p: core::marker::PhantomData<()>, }
/* ghost */ fn do_thing(l: PointsTo) -> PointsTo { todo!() }

fn foo(a: Snap<u64>, l: Tracked<PointsTo>) {
    let b: Snap<u64> = /* ghost! */ Snap::new({
        a /*auto[*/ .ghost_deref() /*]*/ + a /*auto[*/ .ghost_deref() /*]*/
    });
    let c: Snap<u64> = /* ghost! */ Snap::new({
        a /*auto[*/ .ghost_deref() /*]*/ + a /*auto[*/ .ghost_deref() /*]*/
    });
    let m: Tracked<PointsTo> = /* ghost! */ Tracked::new({
        do_thing(l /*auto[*/.ghost_deref()/*]*/)
    });
    // let n: Tracked<PointsTo> = /* ghost! */ Tracked::new({
    //     do_thing(l /*auto[*/.ghost_deref()/*]*/)
    // });
}