This was a good read. The particular problem you were having with wanting safe mutable aliasing is very interesting!
The execution context is an interesting solution, but as you pointed out in "Limitations," preventing mutable aliasing is not just about thread safety. You hinted at it with Vec, but it isn't just limited to Vec because the notion that "mutable alias => unique access" is ubiquitous. IIRC, this property is used to elide bounds checks in iterators in a way that is safe.
Have you explored using Rc<RefCell<...>> at all? That is the "standard" way to get safe mutable aliasing (where actual mutation is guaranteed to be unique through borrow_mut), but I agree it does not meet your criteria of checking this sort of thing at compile time.