Types in TS are Turing Complete [1], so any static analysis you build ontop of that language is bound to be unsound or undecidable. You could argue this rarely occurs in practice, but I would prefer a type system that is incomplete but sound and decidable. Incidentally, this issue also affects Java, which is both unsound [2] and undecidable [3]. Kotlin does have a fairly complicated subtyping relation [4], which has caused similar issues in languages like Scala [5], however whether the same issue affects languages based on mixed use-site and declaration-site variance like Kotlin is still an open question and requires further investigation.
TypeScript works well because they don’t worry about soundness and completeness. The type system isn’t trying to be perfect, just useful. This scares PL theorists, but I think it has been a very profitable corner of the design space to explore.
Variance rarely comes up in Kotlin because they don’t push immutability as much as Scala did. It’s like, there as an option but I’ve used it a total of two times in the last two years of full time Kotlin programming. Compared to typescript, Kotlin is fairly boring, but it is tooled well and is a vast improvement over Java.
[1]: https://github.com/microsoft/TypeScript/issues/14833
[2]: https://io.livecode.ch/learn/namin/unsound
[3]: https://arxiv.org/abs/1605.05274
[4]: https://kotlinlang.org/spec/type-system.html#subtyping
[5]: https://arxiv.org/abs/1908.05294