Subtracting IndexOrHigh from array length is non-negative

[panacekcz]

Subtracting @IndexOrHigh("a") from a.length yields @NonNegative, and subtracting @IndexFor("a") from a.length yields @Positive.
However, since the Upper Bound Checker is dependent on the Lower Bound Checker, the Lower Bound Checker probably cannot make these inferences.

These inferences would help in situations when we specify a range at the end of an array (referring to a suffix of the array).

Possibly related: #96

Code:

import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.NonNegative;

public class SubtractFromLength {
	public void m(Object[] a, @IndexOrHigh("#1") int i) {
		@NonNegative int j = a.length - i; // line 7
	}
	
	// Example adapted from Guava UnsignedLongs.toString
	public String arraySuffixToString(char[] a, @IndexFor("#1") int i) {
		return new String(a, i, a.length-i); // line 12
	}
}

Output:

SubtractFromLength.java:7: error: [assignment.type.incompatible] incompatible types in assignment.
		@NonNegative int j = a.length - i;
		                              ^
  found   : @LowerBoundUnknown int
  required: @NonNegative int
SubtractFromLength.java:12: error: [argument.type.incompatible] incompatible types in argument.
		return new String(a, i, a.length-i);
		                                ^
  found   : @LowerBoundUnknown int
  required: @NonNegative int
2 errors

Expected: no warnings.