Collected comments / questions re type inference in 0.6.3

[Stephan Herrmann]

I finally found a contiguous time slot for updating my inference
implementation according to spec version 0.6.3.
These are my comments and questions:


I couldn't find a statement on how type inference supports
"pass-through" varargs semantics, where a provided array
is directly bound to the varargs array variable.
This way Java 8 would change the semantics in cases like this:
        String[][] x = {{"X"}, {"Y"}};
        List l = Arrays.asList(x);
In Java 7 'l' has two elements of type String[] but the new
inference seems to produce one element of type String[][].
Is this intended?


Incorporation of captures bounds (18.3) is unclear in the use
of indices of α and B. In the former case I believe this is
just a matter of lax notation (replacing all α by αi seems to
trivially mend the issue). However, for the case of B I'm not
sure about the intention: B1,...,Bn are introduced as the
bounds of type parameters P1,...,Pn, i.e., each Bi is a list of
bounds. The first bullet splits these into Bij, which is fine.
But what am I to make of a constraint ⟨θ Bi <: R⟩?
A list of types cannot be a subtype of a type, can it?
Is s.t. like "foreach j : Bij" implied here?

BTW, the notation for substitution is not consistent, e.g.:
- 18.3: θ Bi
- 18.4: L1θ
Is θ prefix or postfix? :)


Sect. 18.4. requires some type variables to "have well-formed bounds".
I could find no reference to well-formedness rules for type variables
in the given sense.

I tend to say that this is a consequence of loose terminology in
the classification of types: On the one hand great care is taken
to distinguish "proper types" from inference variables (good!),
but detailed classification of proper types is still blurred.
First it might help to link usage of the term "type argument"
(notably in 18.2.3 second half, 18.2.4. second half) to 4.5.1
in order to remind the reader, that
   "Type arguments may be either reference types or wildcards."
Otherwise the condition "If T is a type" (should be "reference type")
looks confusing.
Secondly, usage of the term "type variable" conflicts with 4.4.
I found this conflict to be in the tradition of 5.1.10, but it
seems that 0.6.3 aggravates the situation, because in places like
18.4 ("Let Z1, ..., Zn be fresh type variables") we now speak of
type variables with a lower bound and *arbitrary* upper bounds.
Can a type variable have both upper and lower bounds?
Can a type variable have multiple bounds that are classes?
Can a type variable have multiple bounds that are arrays?
To me it is not clear what rules would apply to these type
variables in terms of well-formedness and in terms of compatibilty/
equivalence/subtyping/erasure, but it seems that these type
variables may survive inference (in contrast to inference variables)
and thus must be handled by all downstream phases of compilation,
right?
I don't see how a type variable in this sense falls into the
existing classification, it seems to be neither of type,
inference variable, type argument, type variable à la 4.5.1.
That would mean none of the existing rules are applicable to
type variables?
OTOH, from some uses of "type variable" I could _infer_ that these
are indeed considered as types. But why a type variable should be
a type and a wildcard should not is obscure to me.
Given a suitable interpretation this may all be very clean,
but currently it seems in order to understand type inference
you first have to apply type meta inference :)


18.2.1 calls for applying 18.5.2 to method invocations *and*
class instance creations. Inside 18.5.2, however, I don't see
proper handling of constructors. Specifically:
   "let R be the return type of m"
Given that constructors have no return type
(8.8: "... the constructor declaration looks just like a method
        declaration that has no result (§8.4.5)."),
I believe that inference only works as desired, if we extend
this to include the type of the class instance creation.
Else the rule "If R is void, then a compile-time error occurs"
would cause trouble for constructors.


Repeating from a previous mail: integration of unchecked
conversions into 18.5.1 and 18.5.2 is unclear.
 From Dan's last statement it seems that Java 8 will be significantly
more restrictive, rejecting some programs legal in Java 7.
Before implementing such semantics I need confirmation by the EG,
given that javac (b109) does *not* enforce the stricter semantics.
I might add that I'm actually in favor of gradually fading out some uses
of unchecked conversions, but this must happen in a coordinated way.

thanks,
Stephan