Does `MaybeDangling<&[mut] T>` make any requirements about the pointer's provenance?

[RalfJung]

Concretely, is this code well-defined?

fn main() {
    // Under the current models, we do not forbid writing through
    // `MaybeDangling<&i32>`. That's not yet finally decided, but meanwhile
    // ensure we document this and notice when it changes.

    unsafe {
        let mutref = &mut 0;
        write_through_shr(mem::transmute(mutref));
    }

    fn write_through_shr(x: MaybeDangling<&i32>) {
        unsafe {
            let y: *mut i32 = mem::transmute(x);
            y.write(1);
        }
    }
}

This "launders" a mutable reference through a MaybeDangling<&i32>. Miri says this is okay since MaybeDangling suppresses retags, meaning the provenance returned by the transmute in write_through_shr is exactly the same as the one that was passed into the transmute in main -- it is a Tree Borrows tag that has write permission.

To me, this is a natural consequence of the RFC:

MaybeDangling is a way to "truncate" T to its by-value invariant, which changes nothing for most types, but means that references and boxes are allowed as long as their bit patterns are fine

The above code not being UB means that we can not add LLVM attributes like captures(readonly) to MaybeDangling<&i32> arguments.

@WaffleLapkin was quite surprised by this, so let's make sure we have consensus on how to resolve this question.

If we wanted to make this code UB, I can imagine two ways of achieving that:

• We actually still do retags inside MaybeDangling, but we make those retags behave differently so that they don't fail for dangling pointers. IMO this is a bad idea; I think Rust should have a type that entirely suppresses the implicit move constructor that comes with references and boxes (i.e., the retags), and I think MaybeDangling is the most natural candidate for that type.
• When checking whether a shared reference is valid, we require its tag to not have write permission (with some suitable exception for UnsafeCell). This would make transmutes from mutable references to shared references UB, unless we somehow make it so that we only check this validity requirement after all retags (if any) have happened. But even then this would lead to the odd situation where transmuting &mut T to &T is fine but transmuting it to MaybeDangling<&T> is UB, which seems broken for a type that is intended to let unsafe code do more stuff and avoid UB.

I think the 2nd point is how many people already think shared references work, e.g. I think it is the reason for @nikic's surprise here: the assumption is that the type itself requires the reference to be read-only. But currently that's not what the aliasing model candidates say; they say that shared references become read-only when they get retagged, but without a retag we can't say anything about their permissions.

@rust-lang/opsem what do you think?