Any (single) thing


When typechecking a language with polymorphism (generics), it is usually up to the compiler to fill in the type parameters when a polymorphic function / generic method is called. For instance, given polymorphic function id of type α.αα∀α. α → α, it can equally be called as id(5) and id("hello"), and the compiler will work out the correct value of αα in both cases.

However, for any single call to id there is only one αα to choose, and the compiler must choose consistently. The expression id("hello") + 5 is a type error, even though instantiating αα to string and int are both fine.

In practice, this means that whenever the compiler chooses a type parameter it must record that choice and check compatibility with any other use of the parameter. Early versions of Generic Java1 and certain versions of Scala2 and Kotlin3 failed to do this in all cases, leading to unsoundness. The problem in each case was incorrectly allowing conversions from a type with one arbitrary parameter to a type with two arbitrary parameters, losing the constraint that the two parameters must be chosen the same way.

// Counterexample by Alan Jeffrey
public class Problem {
    // This code compiles, but produces a ClassCastException when executed
    // even though there are no explicit casts in the program.
    public static void main (String [] args) {
        Integer x = new Integer (5);
        String y = castit (x);
        System.out.println (y);

    static <A,B> A castit (B x) {
        // This method casts any type to any other type.
        // Oh dear.  This shouldn't type check, but does
        // because build () returns a type Ref<*>
        // which is a subtype of RWRef<A,B>.
        final RWRef<A,B> r = build ();
        r.set (x);
        return r.get ();

    static <A> Ref<A> build () {
        return new Ref<A> ();

interface RWRef<A,B> {
    public A get ();
    public void set (B x);

class Ref<A> implements RWRef <A,A> {
    A contents;
    public void set (A x) { contents = x; }
    public A get () { return contents; }
// Counterexample by Stephen Compall
trait Magic {
  type S
  def init: S
  def step(s: S): String

case class Pair[A](left: A, right: A)

object Main extends App {
  type Aux[A] = Magic {type S = A}

  // I can't call this one from outerd,
  def outertp[A](p: Pair[Aux[A]]) =

  // but I can call this one.
  def outere(p: Pair[Aux[E]] forSome {type E}) =

  // This one means the left and the right may have *different* S.  I
  // shouldn't be able to call outere with p.
  def outerd(p: Pair[Magic]) =

  def boom =
    outerd(Pair(new Magic {
                  type S = String
                  def init = "hi"
                  def step(s: S) = s.reverse
                new Magic {
                  type S = Int
                  def init = 42
                  def step(s: S) = (s - 3).toString
// Counterexample by Victor Petukhov
class A<R1, K1>(val r1: R1, var k1: K1)
class B<R2, K2>(val r2: R2, val k2: K2)
interface I
class Q1 : I
class Q2 : I {
    fun x() = ""
fun <L, M> foo(x: A<L, M>, y: B<L, M>) {
    x.k1 = y.k2
inline fun <reified T : I> bar(): B<T, T> {
    val w = T::class.constructors.first().call()
    return B(w, w)
fun main() {
    val a1 = A(Q1(), Q2())
    val a = a1 as A<Q1, out Any?>
    foo(a, bar()) // type mismatch in NI

Generic Java type inference is unsound (TYPES mailing list), Alan Jeffrey (2001)