JDK-4993221 : Produce infinite types from lub as required by JLS
  • Type: Bug
  • Component: tools
  • Sub-Component: javac
  • Affected Version: 5.0,6,7,8
  • Priority: P5
  • Status: Open
  • Resolution: Unresolved
  • OS: solaris_8
  • CPU: generic
  • Submitted: 2004-02-11
  • Updated: 2015-12-12
The Version table provides details related to the release that this issue/RFE will be addressed.

Unresolved : Release in which this issue/RFE will be addressed.
Resolved: Release in which this issue/RFE has been resolved.
Fixed : Release in which this issue/RFE has been fixed. The release containing this fix may be available for download as an Early Access Release or a General Availability Release.

To download the current JDK release, click here.
Other
tbd_majorUnresolved
Related Reports
Blocks :  
Relates :  
Relates :  
Description
The main question I have is how type inference works in javac for
cases where GJ-like type inference is actually undecidable. Unfortunately,
with the introduction of variance annotations, the least upper bound
of two types does not always exist. Naturally, this would lead to a
looping compiler. javac doesn't loop but returns arbitrary results; so
I wonder if this is intentional, and if it's intentional, I wonder
what the correct behavior of a Java compiler is in such a case.
Here is an example:

class A<T> {}
class B extends A<B> {}
class C extends A<C> {}
class D {
    <t> t choose(t x, t y) {
        return x;
    }
    void foo() {
        B b = new B();
        C c = new C();
        A<? extends A<? extends A<?>>> x = choose(b, c);
    }
}

The polymorphic method 'choose' of class D expects two parameters of the
same type. When this function is called, the compiler has to infer the
"best" instantiation of the type parameter such that both actual
parameters conform to this type. In my example, the compiler has to
compute the least upper bound of B and C. A first approximation is
A<? extends A<?>>, a better type would be A<? extends A<? extends A<?>>>,
and so on. The problem now is that javac simply infers the type
A<? extends A<?>>; this decision is arbitrary and if a programmer
wants a better type (like in the program above), he has to enforce
the instantiation manually by giving the desired type. I personally
think that simply returning *a* solution is not a good idea; the compiler
should try to construct a really big type and fail if the type required
by the user is bigger (which never happens if the limit of the compiler
is high enough). Then you could sell this as an implementation restriction,
which is completely unrelevant for basically all hand-written Java
programs.

Comments
Inference is a harder problem than checking. If checking is undecidable, so is inference.
23-08-2013

The lifetime on this bug is likely to be quite long, if it can ever be fixed at all. The phrase "infer infinite types" should set off bells. We cannot expect this to be fixed in 8. Thoughts: Type-checking itself is presently undecidable (see https://bugs.openjdk.java.net/browse/JDK-6558545). We cannot expect inference to behave well under these circumstances, especially where infinite types are concerned (as subtyping questions on infinite types are exactly the kind of cases that cause type checking procedures to run infinitely when the type system is generally undecidable). Even if we do fix the problem of the undecidable type system, type inference may well still be undecidable. Type inference is undecidable for type systems with impredicative polymorphism (ie the kind that allows general infinite types), even though checking may be decidable. Possible solutions: i) Find a decidable subset, infer that, require programmers to write down the types otherwise (ie what Haskell does) ii) Try to pare down the allowable infinite types to a decidable set (hard) iii) Write an inference implementation (ie. iterated depth first search) that's complete for all typable programs, but may diverge for untypable ones.
23-08-2013

EVALUATION Not for Mustang
07-08-2005

CONVERTED DATA BugTraq+ Release Management Values COMMIT TO FIX: dragon mustang
07-09-2004

EVALUATION I expect the JLS is likely to require that we act as if we infer the infinitely long type. The current compiler simply cuts it off as soon as it notices the recursion. None of this is undecidable, just difficult. ###@###.### 2004-02-11 Yes, though the product may not be fixed to do this before it ships. For example, the desired type in this bug report is rec T. exists S <: T. A<S> which cannot be written as a Java type, but is a valid type nonetheless. JLS 3ed will have to pin this down soon. ###@###.### 2004-02-11 As I understand it, we will infer "infinite" types but not recursive types. ###@###.### 2004-05-18
11-02-2004