if(! nonempty [] x = ...) is accepted by the compiler (and spec), but is actually not sound

[ePaul]

The following code is accepted by the compiler (e.g. in the WebIDE), and also allowed by the spec, but throws an exception at runtime:

String[]? nonArray = null;
if(! nonempty [] emptyArray = nonArray) {
    print(emptyArray.size);
}

So this checks whether nonArray (i.e. null) is an instance of []? (it is), and then pretends it is an instance of [] (which it isn't, but this is only noted later).

The 1.3 specification says:

For a negated nonemptiness condition:

• if the condition has a pattern, it must be a pattern variable, and the patterned type is T&[], where the specifier expression is of type T and T has the principal instantiation E[]?, and the declared type of the variable, if any, must be [], [...]

So this is explicitly allowed, and the safer []? (which is what the type checker would use when omitting the type) is explicitly not allowed.
Like I noted in #7203 (for some other occurrences around here), I think there are ?s missing in the spec, but in this case also the type checker needs to be fixed. (I guess when T is a subtype of E[], then [] should also be allowed ... though honestly, I don't know why we need a type here at all.)

[gavinking]

Thanks for reporting!

[gavinking]

I've fixed the typechecker, but still need to fix the spec.

[gavinking]

Fixed, I believe.

[gavinking]

Happy now, @ePaul?

[ePaul]

Sorry for replying so late, I didn't find the time until now.

If I read the current spec (in master), I'm not sure what the behavior would be.

if the condition has a pattern, it must be a pattern variable, and the
patterned type is T&<[]?> and the declared
type of the variable, if any, must be a subtype of []?,
or

This sounds like it still allows the code (! nonempty [] emptyArray = nonArray), and I'm not sure what the effect is (i.e. whether for null it would actually enter the block, or not, and what the type of emptyArray is inside the block). The 1.3.3 WebIDE also is still accepting the code from my issue (which is, I suppose, because this is only for 1.4), so I can't currently check what the typechecker says here.

[gavinking]

@ePaul The patterned type is <String[]?> & <[]?> which is []?. The spec then says, in §5.2.3:

If the variable has an explicit type, then the patterned type must be assignable to this type

In your case, the explicit type of the pattern variable is [], to which []? is not assignable.

[ePaul]

Okay, I missed this. Thanks!

[gavinking]

No problem, thanks for reporting.