Avoid the need for computing lubs/glbs

[rossberg]

With subtyping, and lacking sufficient type annotations, some operations may require the validation algorithm to compute the least upper bound (lub) or greatest lower bond (glb) of two types to accurately infer an output or input type, respectively. In current Wasm, this comes up with two instructions:

• select: the result type is the lub of the two operand types
• br_table: the operand type is the glb of the label types

(Similar issues would come up with ops like dup or pick, which might also require a glb of the use edges when the input type is not known a priori, i.e., in unreachable code.)

While lub and glb are easy to compute with the tiny subtyping lattice introduced by this proposal itself, it will not stay that way with future reference extensions (e.g., typed functions or GC types), which will make it both more complex and more costly. In accordance with the design goals for Wasm validation, we should make sure to avoid the need for computing lubs/glbs altogether.

Possible Solution:

• For select, the only option seems to be introducing a new type-annotated version, and restricting the pre-existing unannotated version to numeric types for backwards compatibility (fortunately, only trivial subtyping is available on numeric types).

• Without going into technical details, the glb cases (br_table, dup, pick) can most easily be avoided by adding a bottom type to the type system (a least type in the subtype lattice). Effectively, this is already present in the MVP validation algorithm, to type unreachable stack slots; promoting it to a proper type itself is a natural generalisation in the presence of subtyping. (Note that this type doesn't need not to be expressible in programs, it's sufficient if it exists in the typing rules.)

[titzer]

I am on board with the proposed solution here.

restricting the pre-existing unannotated version to numeric types for backwards compatibility (fortunately, only trivial subtyping is available on numeric types).

Just to make this clearer for the broader audience: trivial subtyping for numeric types in wasm means no subtyping between any of the numeric types: there are no implicit conversions or subsumption.

[rossberg]

@titzer, right, with the one exception that, technically, a bottom type would of course be a subtype of all numeric types. But that's what actually makes this work.