typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
1.02k stars 354 forks source link

Restrict the instantiation type on a constructor #1330

Open mernst opened 7 years ago

mernst commented 7 years ago

It is desirable to specify the result type (the "return type") of a constructor.

For example, new TreeSet<Integer>() has type TreeSet<@NonNull Integer>, but other treesets can permit nullable elements.

More generally, we wish to permit the first two constructor calls but forbid the last two.

   new TreeSet<@Nullable Integer>(new IntegerOrNullComparator()); 
   new TreeSet<Integer>(); 

   //:: error: (type.argument.type.incompatible) 
   new TreeSet<@Nullable Integer>(); 
   //:: error: (type.argument.type.incompatible) 
   new TreeSet<@Nullable Integer>(new IntegerComparator()); 

Java provides syntax for restricting the receiver type on an instance method, but no syntax for type parameter annotations on the constructor result. Only a type annotation, not a full type which would include type parameters, can precede a constructor declaration. So, we would need to make up a new annotation to express the constraint.

There are likely to be classes other than TreeSet that need to utilize this new mechanism.

graememorgan commented 5 years ago

Another example of that is AtomicReference. It's desirable for the type arg to express the nullability of the reference, but the argumentless constructor initialises the reference to null.

AtomicReference<Integer> ref = new AtomicReference<>();
ref.get().hashCode(); // surprise NPE.