Meaning of private structure constructor/fields

Stream: lean4

[Parth Shastri]

I previously discovered (lean4#8665) that the auto generated casesOn implementation can be used to read private fields of any (public) structure, even when the both the constructor and field are marked private. I now found out that the constructor tactic can be used to construct such structures as well. (Similarly, you can use cases/rcases to access fields.) This behavior is present even with the new module system enabled. Is this intended? It doesn't seem right to me that private acts effectively as a lint when applied to structure constructors or fields.