This is a correct observation, and also something to always remember. There are dark corners where unsound type systems fail, they inevitably exist in most practical languages, so you can wander into one in daily practice.