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

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.