[spec/interpreter/test] Reintroduce bottom type

[rossberg]

This addresses #111, which was a collateral damage of removing subtyping in #87. The fix here is to reintroduce the bottom operand type as before, though without the general subtype relation. This change

• is maximally conservative,
• implies the minimal change for implementations,
• merely reenacts what was already implemented in engines before Remove subtyping #87.

More far-reaching revisits of the Wasm typing machinery, as e.g. discussed in WebAssembly/design#1379, ought to be considered as separate proposals. The fix here is conservative over such broader relaxations.

Background:

• In [spec/interpreter/test] Avoid lubs and glbs #43, we added the type-annotated version of select and introduced a simple bottom type. This was in order to avoid the need for computing lubs and glbs during type-checking with subtypes. The bottom type elevated the "unknown" type present in algorithmic validation to a proper citizen of the semantics, and as such required almost no changes to implementations. See also the presentation from the 2019/05 F2F meeting, where this was discussed.

• In Remove subtyping #87, we removed subtyping (based on discussions in the 2020/03 F2F meeting). This also removed the bottom type, because short of subtyping, it no longer worked and seemed no longer necessary. However, one consequence we overlooked is a corner case that occurs in the interference with the new restriction on the select instruction, as noted by @RossTate in Typeability Bug in Reference Implementation #111. That restriction has to remain, in order for typing of select to be future-proof.

• This PR hence reintroduces the bottom type in the simplest possible fashion, without reliance on a general subtype relation. For implementations, this boils down to reverting the change in the typing of the br_table instruction that came with Remove subtyping #87, and possibly tweaks to typing select (depending on whether they currently accept the example in Typeability Bug in Reference Implementation #111 or not). Both can be seen in the changes to algorithm.rst and the reference interpreter in this PR.

• The PR is forward-compatible with the typing rules in the function references proposal.

[RossTate]

This (re)introduces a value type that has no fixed(-per-engine) size. It also violates the property that two value types are (effective) subtypes only if they have the same size, or that distinctly-sized value types have no common (effective) subtypes. It also has the same property that nullptr had in that it means joins of existential (result/state) types do not exist.

The purpose of this change seems to be solely the same purpose as WebAssembly/design#1379. So WebAssembly/design#1379 would make this change completely redundant. And having both introduces warts, like [i32, bot] would be a subtype of [bot, i32] because both are equivalent to unreachable, illustrating that subtyping of lists of value types would no longer be componentwise.

If we don't want the reference types proposal to wait on resolving the discussion in WebAssembly/design#1379, I already outlined how to fix the type-checker in #111 without requiring any changes to the proposal.

[rossberg]

The fix you proposed would require introducing a new form of auxiliary type into the typing algorithm that has not been needed before. Consequently, it is a larger and more intrusive change to implementations than this PR, with potentially more loose ends.

The solution here has already been in engines until recently, so we know it's implementable and we know that it is a minimal change to what engines have been doing all along.

We also know that the value size argument is not an actual problem, otherwise engines would be having it in the MVP already. The property you're alluding to never held in algorithmic checking, so there is no regression in that regard.

We certainly do not want to block on something like WebAssembly/design#1379, which will likely take months to resolve, since the implementation impact across engines is not clear at all.

[titzer]

+1 on not blocking on a long, drawn-out discussion about unreachable code.

[RossTate]

The fix you proposed would require introducing a new form of auxiliary type into the typing algorithm that has not been needed before. Consequently, it is a larger and more intrusive change to implementations than this PR, with potentially more loose ends.

Both introduce an auxiliary type. #111's fix requires no changes to the spec. The main difference between the two is whether ref.is_null accepts the output of a (numeric) select, i.e. does ref.is_null accept the auxiliary type or not. For #111, the answer is no, whereas for here the answer is yes (which seems less conservative). Another difference is whether assignments of the auxiliary type to reference types is accepted or not. This seem like small differences in implementation, whereas #111 requires no changes to the spec.

[rossberg]

@RossTate:

Both introduce an auxiliary type.

No, please read what I said and see the diff. This PR requires no new type in the algorithmic formulation that's used in every engine I'm aware of. It requires zero changes to their type representation, and merely a change to how they check br_table, which reverts back to what it was before #87.

[gahaas]

I think the text here would be more understandable with a clarification what opd stands for.

[rossberg]

Reordered and changed wording to clarify.

[RossTate]

Oh shoot, I forgot to say that I'm fine with this change if it's just a holdover until WebAssembly/design#1379. My concerns are about long-term issues, and WebAssembly/design#1379 would resolve those concerns before the long-term issues have a chance to manifest.