One example that comes to mind is type state [0]. I'm not aware of any other language (including those with support for dependent types, like Agda) where these properties can be checked without external static analysis tools and the problems they bring.
[0] https://yoric.github.io/post/rust-typestate/