Most strongly typed languages have such escape hatches ("Unsafe" in haskell, "Obj" in OCaml, "trustme" in Idris,....) . It's something you always need at some point when the typing is not sufficient to properly account for what you are doing.

For instance, Coq code can be extracted to OCaml code. OCaml type system is less powerful than Coq's, so Coq needs to cheat, and the emitted code is full of "unsafe" features. But the program was typechecked with Coq's type system, and is thus perfectly safe.

Of course, the goal of the language designer is to minimize its usage. That's something the Rust people understood very well, and the unsafe blocks are an extremely good solution to this problem.