> As I understand the isolation check, it is a compile time check

You're right that if your language has an affine type system (that statically identifies some references as being unique), then you can use static type analysis to skip the runtime analysis at some call sites (those where the transferred subgraph contains only unique references).