It's unsound to refine the operand of an instanceof.

[smillst]

However, the operand of an instance of is non-null if the instanceof is true.

This changes cause a new (legitimate) Daikon type-checking error at this line. It's a method.invocation.invaild error on pslice.num_samples();.

[smillst]

Add testcase

[mernst]

I resolved the Daikon type-checking issue by adding annotations to Daikon indicating that num_samples can be called even when its receiver is under initialization.

[smillst]

@wmdietl I would like to rebase this pull request into one commit before merging

[wmdietl]

Is it unsound for type systems other than Nullness because the property is not checked at runtime?

If that's the reasoning, shouldn't the same be done for casts? A cast without runtime check is equally unsound.

[smillst]

@wmdietl is this pull request ok to merge?

[smillst]

Is it unsound for type systems other than Nullness because the property is not checked at runtime?

Yes

If that's the reasoning, shouldn't the same be done for casts? A cast without runtime check is equally unsound.

Correct, which is why a warning is issued if the cast is unsafe.

[wmdietl]

If that's the reasoning, shouldn't the same be done for casts? A cast without runtime check is equally unsound.

Correct, which is why a warning is issued if the cast is unsafe.

So why not do the same thing for instanceof? Refine the type and issue a warning. The two seem equally unsound, so why treat them differently?

[smillst]

So why not do the same thing for instanceof? Refine the type and issue a warning. The two seem equally unsound, so why treat them differently?

We can do this, and I've opened an issue for this request, #762. However, we can't issue the warning without defaulting the reference type of the instanceof to top and it is not straight forward to do so. I would like to merge this pull request so that this fix appears in the release.

[wmdietl]

That sounds like a good plan. I would add a reference from #762 back to this change, to have the basic implementation of the refinement feature.