`[T, T...]` is not a proper subtype of `[T...]`

[ushirask]

Description: [T, T...] is expected to be a proper subtype of [T...] but they are given as both subtypes of each other with isSubtype

ex:

// @type T2 < T1
type T1 [int...];
type T2 [int, int...];

test case fails with T2 is not a proper subtype of T1

[jclark]

@ushirask Please give a failing test case (check it in if we support -ft.bal cases).

[jclark]

I checked that it fails with JSON syntax too. The test case for --testJsonTypes is

[
    ["proper_subtype", ["list", "int", "int"], ["list", "int"]]
]

[jclark]

@ushirask Please see if it happens before the changes to add fixed length array types.

[ushirask]

@ushirask Please see if it happens before the changes to add fixed length array types.

It gives the same results before the fixed length array type implementation

[rdhananjaya]

In listInhabited function, we are changing the fixed length of an array, fixing that solved the issue.

list.bal:239

        int len = members.fixedLength;
        ListAtomicType nt = cx.listAtomType(neg.atom);
        int negLen = nt.members.fixedLength;
        if len < negLen { // we transform semtype here [int...] - [int, int...] => [int, int...] - [int, int...]
            if isNever(rest) {
                return listInhabited(cx, members, rest, neg.next);
            }
            fixedArrayFill(members, negLen, rest);
            len = negLen;
        }
        else if negLen < len && isNever(nt.rest) {
            return listInhabited(cx, members, rest, neg.next);
        }
//........

[jclark]

I explain the logic for rest type for tuples here:

https://github.com/ballerina-platform/nballerina/blob/main/compiler/modules/types/NOTES.md#rest-type-for-tuples

[jclark]

This is the relevant commit:

https://github.com/jclark/semtype/commit/3e15e635b735cabdec422f3e00a984fb29456f61

[jclark]

@rdhananjaya I think the fix is not as simple as what you suggest, because we have to explore all possible ways the list can be inhabited and see whether any of them can survive all the negs.

As the comment at the top says:

// This function returns true if there is a list shape v such that
// v is in the type described by `members` and `rest`, and
// for each tuple t in `neg`, v is not in t.
// `neg` represents a set of negated list types.

We have to find one v that is in the pos and not in any of the negs.

I see two bugs

1. is that we are doing fixedArrayFill without first copying
2. we are not considering all possible ways that it can be inhabited: the one we do explore (by filling out) is a valid possibility, but there are also all the possibilities for when the length is >= len and < negLen

[jclark]

So I think the code for the len < negLen case needs to be something like this:

            if isNever(rest) {
                return listInhabited(cx, members, rest, neg.next);
            }
            if listInhabited(cx, members, NEVER, neg.next) {
                return true;
            }
            foreach int i in len + 1 ..< negLen {
                FixedLengthArray s = fixedArrayShallowCopy(members);
                fixedArrayFill(s, i, rest);
                if listInhabited(cx, s, NEVER, neg.next) {
                    return true;
                }
            }
            members = fixedArrayShallowCopy(members);
            fixedArrayFill(members, negLen, rest);
            len = negLen;

I renamed the param to origMembers and assigned it to members, so I could mutate members.

But it's late and I'm tired.

[jclark]

Actually not sure 1st point about modifying members is correct.

[jclark]

@rdhananjaya I committed what I think is the correct fix. Please have a look and try to break it.

There was a bug in the JSON types parsing code also, which had me very confused for a while.

[jclark]

I think my patch has a problem with fixed length arrays: when negLen is large, we will test every possibility between len and negLen, which will be linear in the size of negLen. Note that in deciding how many lengths we need to test, we need to consider what is in the remaining negatives not just the current negative.

So I also think there's a bug in the fix to #827 in that it does not do that. A neg type further down the list may have different types for i and i + 1 even though they are the same in the positive and the current negative.

We need to consider the maximum initial length of all the negatives.