Index refinement cancels argument compatibility with SameLen sequence

[panacekcz]

Comparing an index by <= or subtracting a non-negative integer sometimes causes an index to be incompatible when used with a sequence that is @SameLen with the original sequence.

import java.util.Arrays;

import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.SameLen;

public class SameLenCancel {
	void strings(String a, @IndexFor("#1") int i, @SameLen("#1") String b, @NonNegative int z) {
		// OK
		Object oa = a.charAt(i);
		// OK
		Object ob = b.charAt(i);
		
		if(i <= a.length() - z) {
			// OK
			Object ioa = a.charAt(i);
			// argument.type.incompatible (line 19)
			Object iob = b.charAt(i);
		}
	}
	
	Object @SameLen("#1")[] same(Object[] a){
		return a;
	}
	
	void arrays(Object[] a, @IndexFor("#1") int i, int z) {
		Object [] b = same(a);
		if(i <= a.length-z) {
			// argument.type.incompatible (line 31)
			Arrays.sort(b, 0, i);
		}
	}
	void arraysOK1(Object[] a, @IndexFor("#1") int i, @NonNegative int z) {
		Object [] b = same(a);
		if(i <= a.length-z) {
			// OK with NonNegative z
			Arrays.sort(b, 0, i);
		}
	}
	void arraysOK2(Object[] a, @IndexFor("#1") int i, int z) {
		Object [] b = same(a);
		if(i <= a.length-z) {
			// OK with array access
			Object o = b[i];
		}
	}
	
	void subtraction(Object[] a, Object@SameLen("#1")[] b, @IndexFor("#1") int i, @NonNegative int z) {
		// 3 cases OK
		sink(a, i);
		sink(a, i-z);
		sink(b, i);
		// argument.type.incompatible (line 55)
		sink(b, i-z);
	}
	
	void sink(Object[] a, @LTLengthOf("#1") int i) {
	}
}

Output:

SameLenCancel.java:19: error: [argument.type.incompatible] incompatible types in argument.
			Object iob = b.charAt(i);
			                      ^
  found   : @LTLengthOf(value={"a", "a"}, offset={"0", "z - 1"}) int
  required: @LTLengthOf(value="b", offset={}) int
SameLenCancel.java:31: error: [argument.type.incompatible] incompatible types in argument.
			Arrays.sort(b, 0, i);
			                  ^
  found   : @LTLengthOf(value={"a", "a", "b"}, offset={"0", "z - 1", "z - 1"}) int
  required: @LTEqLengthOf("b") int
SameLenCancel.java:55: error: [argument.type.incompatible] incompatible types in argument.
		sink(b, i-z);
		         ^
  found   : @LTLengthOf(value={"a", "a"}, offset={"0", "z"}) int
  required: @LTLengthOf(value="b", offset={}) int
3 errors

Expected: no warnings.

[kelloggm]

This looks like a bug in the implementation of SameLen. If this is on your critical path, I can investigate and fix right away.

[panacekcz]

No, this has only a single occurence in guava that got exposed after other issues were fixed. I tried a few experiments to see whether I can fix it by adding annotations and failed. I don't think we need to give priority to this.

[kelloggm]

Okay. I'll fix it when I get a chance, but this is just a bug in the checker - no need to try to fix it with annotations.