Acyclic

code

pub unsafe trait Acyclic {}

// struct Rc<T: RcSafe>
// struct Arc<T: RcSafe>

// R1: structural
unsafe impl Acyclic for .. {}

// R2: no-ownership
unsafe impl<T> Acyclic for Weak<T> {}
unsafe impl<T: Copy> Acyclic for T {} // assuming we actually prohibit Copy+Drop
unsafe impl<'a, T> Acyclic for &'a mut T {}

// R3R: RefCell-inductive
unsafe impl<T> !Acyclic for RefCell<T> {}
#[inductive]
unsafe impl<T: Acyclic> Acyclic for RefCell<T> {}

// R3M: Mutex-inductive
unsafe impl<T> !Acyclic for Mutex<T> {}
#[inductive]
unsafe impl<T: Acyclic> Acyclic for Mutex<T> {}

justification

The invariant is that a type is Acyclic if it can't be part of an owning reference cycle.

If T can't be a part of a reference cycle, then RefCell<T> (or Mutex<T>) also can't be part of one. this justifies R3: inductive.

If T isn't RefCell or Mutex, then T can't be constructed as part of a reference cycle. It can only become a part of a cycle if it refers to a RefCell or Mutex that can be part of a cycle. However, if T is Acyclic and refers to a RefCell, by inductivity we know that the RefCell is already not part of a cycle. This justifies R1: structural.

Non-owning references can never be part of a cycle. This justifies R2: no-ownership.