Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Kotlin's Type System is (Also) Unsound

Elad Kinsbruner, Hila Peleg, Shachar Itzhaky

TL;DR

The paper investigates a novel unsoundness in Kotlin's type system arising from a subtle combination of features: declaration-site variance, type erasure on the JVM, and inheritance rules within Kotlin's collection hierarchy. It constructs a counterexample where a non-variant class can be coerced through a sequence of upcasts and downcasts to produce and manipulate an uninhabited type $A$, exposing a runtime-unsafe coercion that the compiler does not warn about. The analysis shows how declaration-site variance can hide illegal conversions, how @UnsafeVariance and the behavior of CHECKCAST influence safety visibility, and how type erasure contributes to the persistence of unsoundness. The authors discuss practical fixes, including compiler-level checks to track local data-flow of casts, and they situate the result relative to prior unsoundness work such as KT-7972, highlighting broader implications for language design and static analysis tooling.

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.

Kotlin's Type System is (Also) Unsound

TL;DR

The paper investigates a novel unsoundness in Kotlin's type system arising from a subtle combination of features: declaration-site variance, type erasure on the JVM, and inheritance rules within Kotlin's collection hierarchy. It constructs a counterexample where a non-variant class can be coerced through a sequence of upcasts and downcasts to produce and manipulate an uninhabited type , exposing a runtime-unsafe coercion that the compiler does not warn about. The analysis shows how declaration-site variance can hide illegal conversions, how @UnsafeVariance and the behavior of CHECKCAST influence safety visibility, and how type erasure contributes to the persistence of unsoundness. The authors discuss practical fixes, including compiler-level checks to track local data-flow of casts, and they situate the result relative to prior unsoundness work such as KT-7972, highlighting broader implications for language design and static analysis tooling.

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.
Paper Structure (12 sections, 5 figures, 1 table)

This paper contains 12 sections, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The JVM Stack Machine
  4. Variance
  5. Counterexample to Soundness
  6. Discussion
  7. Who's to blame?
  8. @UnsafeVariance
  9. Compiler warnings
  10. CHECKCAST instruction
  11. Previously Known Unsoundness
  12. Conclusion

Figures (5)

  • Figure 1: A code snippet that demonstrates Kotlin's type system unsoundness
  • Figure 2: A code snippet on which Kotlin's compiler issues an unchecked cast warning
  • Figure 3: A translation of \ref{['fig:mainexample']} to C#
  • Figure 4: A program that receives a compiler warning without the @UnsafeVariance annotation on line \ref{['line:unsafevariance']}
  • Figure 5: Code demonstrating issue number KT-7972 in the Kotlin bug tracker, demonstrating how variance, type erasure and smart casts violate soundness.