[Checkers] Question about resolving type variables

[Michael Ernst]

Mahmood-

> Thank you for taking a note of this.  Errr... we should be writing  
> about difficulties about implementing the system and our experience  
> with the Javac API also I guess.

Yes, definitely!  Please take notes on all these things.  A few weeks after
you've written something, it just seems obvious, which is not helpful to
anyone.

> > 1. Supply the context (the expected type) to inference, and if that  
> > type is
> > possible to achieve, then use it instead of the most specific type.   
> > (This
> > would make the "List<Object>" Java example type-check, too!)
> This would render the system unsound.

Oops.  Thanks for pointing this out!  OK, let's scratch that -- except
maybe to point out to others why it *doesn't* work.

How about constructing an example that builds upon the code that you
provided?  I think that will be more compelling.  Also, there are places
where changing the Java type would be bad, but changing the annotation
isn't a big deal.  (Method overriding is an example, and we've seen it in
particular with the receiver type.)  If that is the case here as well, then
the proposed solution may work after all.  I would like to be certain
either way, so let's look at this a tiny bit closer.

> > * must supply the type context.  This probably isn't a big deal.
> Actually, we already use the type context to infer types not specified  
> via arguments (e.g. Collections.emptyMap()).  Rather than supplying an  
> context argument,  AnnotatedTypeMirror uses TreePath to get the  
> assignment context.

That's interesting.  Can you please add this to wherever you are keeping
the list of details that a reader would be interested in knowing?
Generally speaking, a technical paper should be written in such a way that
a competent programmer should be able to reproduce it without making any
theoretical/conceptual decisions.

> it is a bit  
> annoying to break backward-compatibility and may require us to explain  
> our choice if we do so.

I agree, but some checkers already break backward compatibility, if I
understand what you mean by the term.  I think that you mean:  "an
unannotated program should type-check".  That isn't true of the non-null
checker, since it issues warnings about possible null dereferences.

The IGJ checker is (so far) backward compatible in this sense, which is
really nice.  We may discover that in general, backward compatibility in
this sense is impossible.  That would be very interesting to report as
well!

> I wonder if it will be possible to change the assigned to variable  
> type to the appropriate type.  So for the following example:
> 	List<String> lst = Arrays.asList(array); // where array is of type  
> String[@Interned];
> 	lst.set(0, new String());
> lst will get the type List<@Interned String>, thus the checker would  
> issue an error for the set method invocation, but not of the assignment.

When you say, "change the assigned to variable type", do you mean change
the declaration, or just change some of the uses?  I prefer the former if
possible, since it seems simpler.

I think you are saying:  use the variable's context for choosing the
generic type, but have that context include all uses in scope, not just
the declaration.  Is that right?

All this is verging on type inference, of course.  We don't want to go down
a slippery slope.

> Personally, I think this proposal will complicate the implementation  
> very much, and makes debugging harder.

Let's first determine whether it will simplify life for users.  If so, then
we can think about implementation and debugging.  If it's not beneficial to
users, then implementation complexity is irrelevant.  (Did you mean
debugging for users or for implementers of the type checker?)

                    -Mike