Type annotations on switch

[tlively]

The explainer currently has switch taking two type annotations, but the second can be computed from the first, so it seems we should only need one. Is there any reason to prefer having both?

[dhil]

All the instructions are annotated with their continuation types (notably cont.bind has two annotations too as its typing rule involves two continuations). I don't think any of these annotations are strictly necessary as I believe they are computable (maybe I am missing an edge case). However, in my experience the type annotations make the implementation simpler as you simply have to verify/check a producer provided type against what's on the stack rather than first constructing the type and then checking. To me there is a philosophical discussion to be had here: do we want the engine to compute evidence as much as possible or simply have it verify/check provided evidence? (personally I am lean towards the latter.)

That said, I think it may be the case that in practice switch will end up with the same type annotation twice, e.g. switch $ct $ct $tag, because my current belief is that practical use-cases will fix some universal type for switching in order to allow any stack to switch to any other stack. Though, it is possible to imagine use-cases where the heterogeneity provided by the current typing rule could be useful (e.g. static encoding of transaction protocols).

[rossberg]

In the case of cont.bind, the second annotation cannot be derived easily — validation would have to construct a new deftype, and there generally is no principal way of doing so, e.g., because of type recursion. In the case of switch, however, the second type can simply be read off the definition of the first. So the annotation should indeed be unnecessary and we should remove it. That actually simplifies validation, since it avoids an extra comparison with the annotation.

[dhil]

OK, I will revert the reference interpreter to the single type annotation.