IDL: Implement width subtyping for sequences directly

[nomeata]

without appealing to records, and clarifying that it can be done lazily.

This allows functions to add new result values and new (optional)
argument values just fine. It seems.

[rossberg]

Hm, I am not sure this is correct. It seems to me that it runs afoul the same contra-variance violation that we have run into before, i.e., the subtyping against null/any is the wrong way around in the higher-order case.

[nomeata]

It is still different from earlier attempts (e.g. indexing the judgment) because it is not “deep”. We do not mess with the subtyping/contravariance machinery in any deep or tricky way; we just have two different type constructors on the left and right of the arrow.

Because of this, I am fairly confident that it is sound, and reasonably confident that it does not forbid any useful upgrade behavior.

[crusso]

Intriguing, but my head hurts.
I'm trying to figure out what this might mean without any coercions. An argument sequence would always have a prefix of the sequence in the type, and projecting outside the argument sequence would return null. A function would always return all of the results in the type and thus be compatible with any prefix of that type.

[nomeata]

An argument sequence would always have a prefix of the sequence in the type, and projecting outside the argument sequence would return null.
A function would always return all of the results in the type and thus be compatible with any prefix of that type.

Correct

What you lose is:

• Sending extra arguments to a function that you have no reason to believe that function is accepting.
• Returning less results than you used to.

[nomeata]

Probably obsoleted by #832 (As the opt machinery there will also be available in argument/result sequences.)

[dfinity-ci]

In terms of size, no changes are observed in 2 tests.
In terms of gas, no changes are observed in 2 tests.