Recently we have seen a renewed interest in programming languages that tame the complexity of state and concurrency through refined type systems with more fine-grained control over effects. In addition to simplifying reasoning and eliminating whole classes of bugs, statically controlling effects opens the door to advanced compiler optimisations, such as automatic parallelisation. The flip-side of this refined typing is that these languages often have to include trusted library code that violate the static typing discipline, in ways that are claimed to be unobservable to clients. In this paper we define a logical relation for a language with an ML-like type system refined with effect annotations that supports reasoning about contextual equivalence of potentially ill-typed terms. Using this relation we can formally justify such claims about breaking typing in unobservable ways. The logical relation also supports type-based optimizations, such as automatically parallelizing expressions whose effects are suitably disjoint. The logical relation is defined in Iris, a state-of-the-art higher-order separation logic. This allows us to fall back to a powerful program logic to prove semantic well-typedness in cases where the static typing discipline is too imprecise.