Soundness of a type system is a fundemental property that guarantees that no operation that is not supported by a value will be performed on that value at run time. A type checker for a sound type system is expected to issue a warning on every type error. While soundness is a desirable property for many practical applications, in 2016, Amin and Tate presented the first unsoundness proof for two major industry languages: Java and Scala. This proof relied on use-site variance and implicit null values. We present an unsoundness proof for Kotlin, another emerging industry language, which relies on a previously unknown unsound combination of language features. Kotlin does not have implicit null values, meaning that the proof by Amin and Tate would not work for Kotlin. Our new proof, which is an infringing code snippet, utilizes Kotlin's \emph{declaration-site} variance specification and does not require implicit null values. We present this counterexample to soundness in full along with detailed explanations of every step. Finally, we present a thorough discussion on precisely which language features cause this issue, as well as how Kotlin's compiler can be patched to fix it.

翻译：类型系统的健全性是一项基本性质，它保证在运行时不会对某个值执行该值不支持的操作。对于一个健全的类型系统，其类型检查器应当对每个类型错误都发出警告。尽管健全性对许多实际应用而言是理想的性质，但 Amin 和 Tate 在 2016 年首次证明了两种主流工业语言（Java 和 Scala）存在不健全性。该证明依赖于使用点变型与隐式空值。本文针对另一门新兴工业语言 Kotlin 提出了一个不健全性证明，该证明基于一种先前未知的语言特性组合。Kotlin 没有隐式空值，这意味着 Amin 和 Tate 的证明无法适用于 Kotlin。我们提出的新证明（一段违规代码片段）利用了 Kotlin 的声明点变型规范，且不需要隐式空值。我们完整展示了这一违反健全性的反例，并对每一步进行了详细解释。最后，我们深入讨论了究竟是哪些语言特性导致了此问题，以及如何修补 Kotlin 编译器以修复该问题。