Okay, then I can pick another example: A dictionary where the type of the values depends on the key they're inserted under. (For example, a representation of the closure of a function in a typed language.) Of course, then I can go to a dependently typed language, but are you really going to tell me that only dependently typed languages count as "good" static type systems?

I am not arguing completeness here; a type system is not a full-blown specification language and does not have to be. (I actually tend towards the point of view that trying to make them complete specification languages has limited practical value, but that's a different issue.)

The point here is that the type system does not restrict me from implementing a data structure that adheres to this constraint, even if it does not enforce it for me.

You can do this in GHC Haskell with existential quantification, or trade static checks for runtime with Data.Dynamic.

(Again, not arguing against your thesis here.)

After quickly scanning https://realworldocaml.org/v1/en/html/variants.html, isn't the same thing accomplished by GADTs?

The point of polymorphic variants is that the entire type doesn't have to be fully defined in one place; you can have partial definitions in a module and those definitions can even overlap. You can have (say) [ `Int of int | `String of string ] in one module and [ `String of string | `Char of char ] in another, and the typechecker will handle intersections and unions of these types.