Here is an example of lifetimes influencing traits, where a non-static lifetime will fail to compile
Above I was mostly arguing that for the particular example under consideration, IMO it is wrong to blame
But after trying to convince myself of the correctness of
Pin::new, I agree with you: that is highly non-trivial! This seems to rely on coherence as we are arguing about "
P::Deref for our current
P" when establishing the invariant of
Pin<P>. It might be the case that even with unsafe marker traits, we will still need some amount of coherence-based reasoning.
One thing I am wondering about: assuming we use unsafe marker traits but keep
Pin::new as-is, is there still a soundness hole?
I tried to come up with a precise invariant for
Pin<P> that is defined generically in
P, but I think that is out of reach of our current formal models. The issue here is the conceptual mismatch that I already mentioned before stabilization: really we want
Ptr is "higher-kinded": it has kind
Type -> Type) instead of
Pin<Ptr<T>>. I have some idea for how to define the invariant for the former, but no good handle on the latter.
My best guess for this invariant is something like "the
Deref impl, if it exists, returns a shared reference to a pinned
P::Target; and the
DerefMut impl, if it exists, returns a mutable reference to a pinned
&mut P::Target. (We have no Rust type syntax for directly expressing "shared/mutable reference to pinned
P::Target"; this is basically
PinMut<P::Target> from the previous non-generic approach. Those I know how to formally define.) Note how strongly this relies on coherence -- exactly what I wanted to avoid with unsafe marker traits.