I feel like a distinction needs to be made between soundness and precision. A sound type system never tells you something wrong while a precise type system tell

I feel like a distinction needs to be made between soundness and precision. A sound type system never tells you something wrong while a precise type system tells you everything that needs to be said about a value. Gradual type systems are imprecise, because they could type something at some * type. There's nothing wrong with that. Unsoundness is bad on the other hand, it keeps you from omitting dynamic type checks in places where you would want to in your compiler. A natural thing to want to do is include dynamic checks expressly where you are downcasting from a * type, omitting them where the type is known precisely enough. That is how you reap a performance gain from your type system, and unsoundness prevents you doing that. (Downcasting from * in a gradual type system is analogous to how C lets you cast from void* to any pointer type implicitly, except that RTTI checks that the cast is safe.)