Yes, you are correct. The types defined using this method are unsafe. This post is about sharing an informal way to define contravariant types, which is why I prefix packages that add types in this way with unsafe.
While this approach is unsafe, it addresses a significant limitation in TR: the lack of contravariant type support, which results in mutable types having no subtyping relationships. For example:
> (ann (vector 0) (Mutable-Vectorof Natural))
- : (Mutable-Vectorof Nonnegative-Integer)
'#(0)
> (ann (ann (vector 0) (Mutable-Vectorof Natural)) (Mutable-Vectorof Integer))
string:1:10: Type Checker: type mismatch
expected: (Mutable-Vectorof Integer)
given: (Mutable-Vectorof Nonnegative-Integer)
in: (vector 0)
[,bt for context]
Additionally, predicates for mutable types cannot be defined:
> (define-predicate p (Mutable-Vectorof Natural))
string:1:20: Type Checker: Error in macro expansion -- Type (Mutable-Vectorof Nonnegative-Integer) could not be converted to a predicate: required a flat contract but generated a chaperone contract
in: (Mutable-Vectorof Natural)
[,bt for context]
These factors make mutable types in TR very difficult to use. As shown in other posts (e.g., this one), I'm not the only one facing this problem, which seems to have persisted for quite some time. Years ago, I struggled with this issue and resorted to using untyped Racket, then importing unsafe types via unsafe-require, and carefully working with them. In this discussion, @AlexKnauth introduced the concept of contravariant contracts and proposed contravariant types as a potential solution.
Currently, the only contravariant type officially supported in TR is Parameterof:
> (ann (make-parameter 0) (Parameter Natural Natural))
- : (Parameterof Nonnegative-Integer)
#<procedure:parameter-procedure>
> (ann (ann (make-parameter 0) (Parameterof Natural Natural)) (Parameterof One Integer))
- : (Parameterof One Integer)
#<procedure:parameter-procedure>
I've summarized cases where using contravariant types defined with struct and Parameterof is unsafe, and I think these cases are relatively uncommon. A careful programmer can avoid them, making this type of unsafety one of the more manageable kinds. This approach introduces subtype polymorphism and read-only types, significantly alleviating the challenges of working with mutable types in TR.
Moreover, with Racket's recent addition of mutable-treelist, a new mutable data structure that has yet to see widespread use, I see an opportunity for programmers to experiment with these types in TR. Exploring contravariant types might also provide valuable insights and serve as a testbed for future developments in TR. For instance, some of the unsafe scenarios I've identified, such as write-only types and write types being supertypes of read types, are issues that would need to be addressed if TR were to officially support contravariant types. After all, types and contracts are fundamentally different, as evidenced by the fact that many TR types cannot be directly translated into corresponding contracts.
Lastly, I'd like to explain why it took me over a year to notice these unsafe scenarios 
. When writing TR code for testing, the test code itself must be type-correct, which makes it difficult to write test cases that deliberately produce type errors. Since rackunit only captures runtime exceptions, I naturally ended up writing code that was type-correct (which is one of the reasons I love TR—it guides me to write correct code). This is likely why I missed what, in hindsight, seems like an obvious unsafe scenario for almost a year! 