Yeah taht’s what I now thought we are talking about. Essentially, Pinned<T> is “just another newtype” around T, except that it’s magic because the compiler “forgets” the sizedness. We have some privileged API that transmutes (or so) &mut T into &mut Pinned<T> (e.g. if T: Unpin). PinBox<T>… would maybe just be Box<Pinned<T>>, and we provide an API that internally transmutes from Box<T>? (I guess someone already said it, but now I understood it, too. 
) Then getting the &mut Pinned<T> wouldn’t even be a new thing, it’d just be Box<T> as DerefMut. Reborrowing would also just work.
I feel like this works “too well” and there is probably a catch somewhere. But this does seem to provide the nice compositionality that we can add it to any kind of pointer. It does require language support up-front though (and not just as a nice-to-have future extension) to make sure Pinned<T> is considered unsized and whatnot. And what happens if T is unsized as well? &mut Pinned<dyn Trait> is something we’d want, I guess, because we care about Future being dyn-safe. This should be a fat pointer.
I only have a very faint idea how this could look like in the model—unsized types are something I avoided so far—but it’d probably still involve having dedicated modes. After all, we have to say what Pinned<T>.own is, and it’s not going to be T.own; I guess it’d be T.pin.
Actually, I just made an interesting observation… I’ve been wondering for a while whether T.own should really operate on lists of bytes, like it does now. Maybe it should work on a pointer instead. That’d make it more uniform with T.shr and also avoid the problems (that also came up in my posts) that lists of bytes are rather annoying to work with; usually you want to see them as corresponding to something higher-level that just can be laid out in memory. So, let’s say T.own(bytes: List<Byte>) changes to T.own(ptr: Pointer). Now (if we ignore sizedness), we still are able to move all types, so we will want to have an axiom that lets us extract, from T.own, ownership of the memory behind ptr. But ownership of how much memory? size_of<T>() many bytes, of course! Now, what if we don’t know the size? Well, in that case it seems we cannot even ask for the ownership we want, so the axiom doesn’t happen… so the type is immovable! This ignores entirely the possibility of determining the size at run-time, obviously. But I guess what I am saying is that, in the formal model we can make the same observation as what has been made above (and maybe I shouldn’t be surprised): !DynSized types are inherently immovable. Their T.own degenerates to just a predicate over a pointer with no restrictions (other than some relationship to sharing), which is exactly what T.pin is. Suddenly, "Move iff DynSized" seems much less ad-hoc to me. Both are essentially just “we can say something about the pointer (T.own(ptr)), but we have no idea whatsoever what we can do with it (no axioms that T.own has to satisfy)”.
So, the fact that Move implies DynSized shouldn’t be surprising, that’s just practically necessary. It still seems funny that we’d want to consider types that actually are movable, to be not movable. But what is a size good for if we don’t want to move? Well, we need it for layout, but Pinned would not be used in type definitions—i.e., (Foo, Pinned<Bar>) is not a thing we even want. It’s just used behind a pointer indirection. Layout computation never even sees this type. From all I can see, it should behave just like an extern type, except that we probably (?) don’t want to allow extern types to have type parameters.
