Semi-implicit dropping of initialization should be explicited

[rajdakin]

(Based on WebAssembly/stack-switching#118)

The current specification prevents initialization information to be propagated through blocks by simply not having variable lists in the rules:

C |- blocktype : [t1*] -> [t2*]    C, labels[t2*] |- instr* : [t1*] -> [t2*]
----------------------------------------------------------------------------
              C |- block blocktype instr* end : [t1*] -> [t2*]

C |- blocktype : [t1*] -> [t2*]    C, labels[t1*] |- instr* : [t1*] -> [t2*]
---------------------------------------------------------------------------
              C |- loop blocktype instr* end : [t1*] -> [t2*]

I understand the rationale behind this decision, and I agree that this is the simplest way that is also future-compatible. However, someone reading through this specification may not notice this as this is too implicit, and I think this decision should be explicited in a note as this is an important caveat.

The note would not have to be long; it could for example be:

This instruction never initializes locals.

EDIT: Another possibility is to add a note similar to the select instruction, such as:

In future versions of WebAssembly, this instruction may specify locals that become initialized.

On a related note, why are block types valid as instruction types when they cannot describe locals indices? Shouldn't they be valid as function types instead?

[rossberg]

On a related note, why are block types valid as instruction types when they cannot describe locals indices? Shouldn't they be valid as function types instead?

Either is fine, but instruction type seems more adequate, if you view the ability to encode it with a function type as a local detail of the blocktype construct. And in the future we might generalise that to produce more general instruction types.