-I do have an idea for how to solve this problem: Introduce a *fourth* "mode" or typestate, the "shared pinned" state, with an accompanying invariant.
+Notice that this is a consequence of a choice I made when building the model, namely the choice to define `Pin<'a, T>.shr` in terms of `T.shr`.
+This does *not* show that `&Pin<T>` and `&&T` have to be the same type given the public API and the contract they provide.
+Different choices in the model could lead to a different situation.
+The problem is, how else *could* we define `Pin<'a, T>.shr`, if we do not want to use `T.shr`?
+What *is* the invariant of a shared reference to a pinned reference?
+
+I do have an idea for how to answer this question: Introduce a *fourth* "mode" or typestate, the "shared pinned" state, with an accompanying invariant.