[Draft][spec] Improve typing of br_if
#532
Conversation
`br_if` previously had type `[t* i32] -> [t*]` where `[t*]` was the type of its target label. This typing unnecessarily lost type information in cases where the actual input result type is a strict subtype of the label result type, requiring casts to recover the types that the validation algorithm already knew about before the `br_if`. Update the type of `br_if` to be `[t1* i32] -> [t1*]` where `[t*]` is a subtype of the label type `[t*]`. This type preserves types that were present before the `br_if`, even when they are strict subsets of the label result types. Update the description of principle types in the appendix to allow type variables to be constrained by upper bounds and update the validation algorithm to reflect the new typing. This current PR illustrates the intended changes only for `br_if`, but the full intended change would similarly improve the types of `br_on_null`, `br_on_non_null`, `br_on_cast`, `br_on_cast_fail`, and `local.tee`.
Without more justification, I'd be against this. It seems like an unfortunate last-minute complication to our conceptual model of how typing works to allow these kinds of bounds. Is the aim here to bless what some implementations are doing, due to the divergences in #516? |
No, not directly, but it is related. The aim is to improve the precision of the types for these instructions so we admit programs with fewer casts than before. The reason implementations were wrong in the first place is that the implementers incorrectly assumed the spec would already be giving these instructions the most precise possible types for the same reasons. From the implementer point of view, this is fixing a bug in the spec, not just changing the spec to match implementations. |
I don't really agree with these points. We spent a lot of time debating the exact principal types property we wanted, and how we were going to type We did note in #201 that we could potentially revisit the discussion later, but we should acknowledge that this patch is effectively reopening the #201 discussion, rather than making an uncontroversial improvement. |
|
Yes, my intent is to reopen the discussion from #201 (and WebAssembly/reference-types#55). Sorry if that wasn't clear. |
br_ifpreviously had type[t* i32] -> [t*]where[t*]was the type of its target label. This typing unnecessarily lost type information in cases where the actual input result type is a strict subtype of the label result type, requiring casts to recover the types that the validation algorithm already knew about before thebr_if.Update the type of
br_ifto be[t1* i32] -> [t1*]where[t1*]is a subtype of the label type[t*]. This type preserves types that were present before thebr_if, even when they are strict subsets of the label result types.Update the description of principle types in the appendix to allow type variables to be constrained by upper bounds and update the validation algorithm to reflect the new typing.
This current PR illustrates the intended changes only for
br_if, but the full intended change would similarly improve the types ofbr_on_null,br_on_non_null,br_on_cast,br_on_cast_fail, andlocal.tee.Procedurally, we would want to run this by the full CG before making this change since the proposal is already phase 4. This is a non-breaking change, though, and until very recently was actually how most implementations behaved.