Kotlin's Type System is (Also) Unsound

TL;DR

This paper demonstrates that Kotlin's type system is unsound due to a specific combination of language features, providing a counterexample and discussing potential fixes to ensure soundness.

Contribution

It presents the first unsoundness proof for Kotlin's type system, identifying a previously unknown problematic feature combination.

Findings

Kotlin's type system is unsound due to declaration-site variance.

A counterexample exploits Kotlin's features without relying on null values.

The paper suggests how to patch the Kotlin compiler to restore soundness.

Abstract

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.