Why does the following code crash javac? What can be done about it?

Question

I was reading this article about "odd things in Java" and I came across an interesting concept: Undecidable types.

Consider the following three classes / interfaces:

public interface Type<T> { }

public class D<P> implements Type<Type<? super D<D<P>>>> { }

public class WildcardTest {
  Type<? super D<Byte>> d = new D<Byte>();
}

Apparently the problem is that it is undecidable whether D is a Type<? super D<Byte>>; can anyone explain this further?

javac 1.8.0_60 throws a very long StackOverflowError when trying to compile WildcardTest:

The system is out of resources.
Consult the following stack trace for details.
java.lang.StackOverflowError
        at com.sun.tools.javac.code.Types$UnaryVisitor.visit(Types.java:4640)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3834)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3826)
        at com.sun.tools.javac.code.Type$ClassType.accept(Type.java:778)
        at com.sun.tools.javac.code.Types$UnaryVisitor.visit(Types.java:4640)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3839)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3826)
        at com.sun.tools.javac.code.Type$ClassType.accept(Type.java:778)
        at com.sun.tools.javac.code.Types$UnaryVisitor.visit(Types.java:4640)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3839)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3826)
        at com.sun.tools.javac.code.Type$ClassType.accept(Type.java:778)
        at com.sun.tools.javac.code.Types$UnaryVisitor.visit(Types.java:4640)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3839)
        at com.sun.tools.javac.code.Types$26.visitClassType(Types.java:3826)
        at com.sun.tools.javac.code.Type$ClassType.accept(Type.java:778)

This code also crashes the entire Eclipse IDE.

The author has filed a bug with the Eclipse team but it hasn't gotten any votes (besides mine). Can anything even be done? Is this simply the Halting Problem in compiler form?

There is also a link to this paper about it in the article, but I am hoping there is a more straightforward explanation.

Answer 1

As Tunaki pointed out in the comments, this goes back to a Microsoft research paper co-authored by Pierce (the TAPL author). In fact, the problem Tate et al. give is Example 2 from Appendix A (with Byte = T, Type = N and D = C).

The Stack Overflow

First, let's figure out why it blows the stack. To do that it's good to remind ourselves that the compiler checks types pretty much the same way we do. Problems we encounter it will encounter.

// To be determined:
D<Byte> <: Type<? super D<Byte>>

// using D<P> implements Type<Type<? super D<D<P>>>>

Type<Type<? super D<D<Byte>>>> <: Type<? super D<Byte>>

// The outermost type constructor (Type) matches. For the
// suptyping relationship to hold, we have to test the type
// arguments. (Sides are flipped due to contravariance.)

D<Byte> <: Type<? super D<D<Byte>>>

// Mhh… That looks an awful lot like above.
// Feel free to rinse and repeat until your "stack" blows too… ;)

Pierce et al. describe a similar regress as Example 2 in Section 3 of their paper. It is slightly different because Java does not allow lower bounds on type variables, only on wildcards.

What can be done?

Similar to Example 1 given by Pierce et al., this regression follows a pattern. This pattern can be detected by the compiler and the subtyping relationship can be assumed to hold under the co-inductive interpretation. (This is the same reasoning as with F-bounded polymorphism, i.e. Enum<E extends Enum<E>>. You enter a similar infinite regress without contradiction.)

Undecidable?

The given problem can be addressed by a smarter algorithm. Whether Java's type system is decidable or not remains an open question.

If Java allowed lower bounds on type parameters it would be undecidable (semi-decidable). However, in their paper Pierce et al. define restrictions with which such a type system could be made decidable again. Incidentally, these restrictions were adopted by Scala which ironically has a turing complete type system.