Unsoundness in `Pin`

Here is an example of lifetimes influencing traits, where a non-static lifetime will fail to compile

1 Like

Above I was mostly arguing that for the particular example under consideration, IMO it is wrong to blame Pin::new.

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 Pin<Ptr><T> (where 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 PinRef<P::Target>/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.

2 Likes