[explainer] Fix constraints and refactor handlers

[tlively]

• Refactor the rules for handlers out so they do not need to be repeated for both resume and resume_throw.
• Fix the constraint on the tag type in (on $e switch) handlers to ensure the tag result type is equal to the continuation return type. The tag result type must be a subtype of the resume result type to ensure the switched-to continuation has a compatible type, and it must also be a supertype to ensure the return continuation has a correct type. If we wanted to provide more flexibility here, we could upper bound the switched-to continuation result type with the tag results and lower bound the return continuation result type with the tag parameters, but I can't think of any benefit to doing that.
• Fix the constraint on the return continuation result type in switch. We know the switched-from continuation returns t*, so we must type it as returning a supertype of t*, not a subtype.
• Fix some mismatched iteration bugs.

[conrad-watt]

Although it is necessary for the target continuation's return type to match the return type expected at the handler and communicated via the tag, it is not necessary for the return continuation's return type to match the expected return type as well. If the same handler (and therefore tag) is to be used to return to the previous continuation, then that returning switch will only validate if the return result type matches, but in general the return switch could be done with a different handler with an arbitrary type.

Wouldn't this be unsound? The return continuation (representing the computation suspended by the switch) must have as its return type some te2* <: t* because it was suspended up to a handler with return type t* (and if it had run to completion instead of suspending, it would have returned these results). I wouldn't expect it to be safe to use a different handler unless the return types also match.

In fact, I think this rule isn't correct even as it is - it's not safe for the return configuration to have type te2* <: t* - it must have type t*, because you don't know that the te2* picked by the "switch-to" continuation's annotation is the same as the "real" te2* used by the currently-executing "resume"-d stack. Imagine that the parent resume has return type any - this would allow you to resume a continuation with return type any, but the current switch instruction would allow you to later suspend this computation as a continuation with return type struct --- seems unsound! @rossberg?

[conrad-watt]

Also noting that @rossberg's original comment (https://github.com/WebAssembly/stack-switching/issues/61#issuecomment-2222629632) gets this right, and I've been overzealous in adding subtyping :)

I think the subtyping on the "switched-to" continuation is ok, but the subtyping on the "return" continuation is wrong - instead of te2* <: t*, it should just be t*. Could we repurpose this PR to fix this? (technically further constraining the return type...)

[conrad-watt]

Actually, even this might not be enough, because currently the typing rules for switch handlers that I wrote down allow the recorded return type to be a subtype of the actual one - so you can create the same unsoundness even with the t* change just be switching off the "wrong" handler. I have systematically messed up my contravariance vs covariance.

So I think the total needed changes are as follows: The bottom lines of switch need to be "reversed" to

`C.types[$ft2] = [t2*] -> [te2*]`
`t* <: te2*

(or just t* = te2*)

Similarly, the constraint on the switch handler's type needs to be reversed - i.e.

te1* = []
t2* <:  te2*

(or just t2* = te2*, or whatever we decide in https://github.com/WebAssembly/stack-switching/pull/64)

@rossberg please check my work here, and very sorry for the churn.

[rossberg]

The tag type essentially works as a cross-site type annotation, so all local types ought to be subtypes of that to agree. So yes, it should be t2* <: te1* (or better t2* <: te2*) in the handler rule. On the switch instruction the subtype direction looks right to me, but is obscured by an inverted naming choice that might be worth changing.

But on closer inspection, I'm afraid a few more bugs sneaked in:

• Several double uses of * iteration in the handler rules (e.g. ([te1*] <: [te1'*])* should be [te1*] <: [te1'*]).
• All the type expansions are missing (use ~~ instead of = when looking up a type).

My first comment probably comes closest to being correct, modulo some side conditions moving from handler to switch (and notational shortcuts). I would also strongly suggest maintaining the factorisation of handler typing to avoid all the duplication.

[tlively]

Thanks, @conrad-watt, you're totally right about the soundness.

I'm happy to repurpose this PR to fix the bugs, but I think it will be easier on top of #68 if we can land that.

[tlively]

Ok, I think what I have here should now be good to go. See the updated PR description, and in particular the note about the necessity of using type equality in the switch handler, which I think we had not made explicit before.