Type checking challenge

[ghost]

Working on the type system and in particular how the empty-type (result of br and unreachable) are handled suggested this challenge which fails the current ml-proto and sexp-wasm checks.

(module
 (func (param $i1 i32) (result i32)
   (block $l1
     (br $l1 (i32.const 1))
     (i64.const 2))))

This could be handled top-down by not checking the dead code. It can be handled bottom up by the unreachable fall-through result having the empty-type and the union with the break types still being consistent with the expected type.

[ghost]

Think I understand how this can work now, sorry for the noise. In case it's of interest to other people, the answer seems to be to consider all code live for the purpose of the type verification, then the test is more specific than otherwise but still seems sound. Can't think of any substantive example that breaks by failing to correctly derive that an expression has the empty-type, except for the leaf expressions and parametric operators.

Here's a simpler example. The empty-type would be considered when checking the argument to 'i64.extend_u/i32' but not propagated (bottom-up), so not taken into account when checking the function result.

(module (func (result i32) (i64.extend_u/i32 (unreachable))))

For the block operator, dead code would not yield the empty-type.

The 'parametric' operators would pass through an empty-type. For example the following are valid:

(module (func (result i32) (block (unreachable))))

(module (func (param $i1 i32) (result i32) (if_else (get_local $i1) (block (unreachable)) (block (unreachable)))))