search

WebAssembly / gc

Branch of the spec repo scoped to discussion of GC integration in WebAssembly
https://webassembly.github.io/gc/
Other
1k stars 73 forks source link

[Draft][spec] Improve typing of `br_if` #532

Open tlively opened 8 months ago

tlively commented 8 months ago

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 [t1*] 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.

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.

conrad-watt commented 8 months ago

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.

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 https://github.com/WebAssembly/gc/issues/516?

tlively commented 8 months ago

Is the aim here to bless what some implementations are doing, due to the divergences in https://github.com/WebAssembly/gc/issues/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.

conrad-watt commented 8 months ago

The aim is to improve the precision of the types for these instructions so we admit programs with fewer casts than before.

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 local.tee specifically. I think the presumption should be that we stick with these decisions rather than reopen them due to an implementation discrepancy. I appreciate that the issue with br_* seems to specifically create more work for Binaryen because of the inference vs checking distinction, but it seems like there's a feasible patch? (https://github.com/WebAssembly/binaryen/pull/6390).

We did note in https://github.com/WebAssembly/gc/issues/201 that we could potentially revisit the discussion later, but we should acknowledge that this patch is effectively reopening the https://github.com/WebAssembly/gc/issues/201 discussion, rather than making an uncontroversial improvement.

tlively commented 8 months ago

Yes, my intent is to reopen the discussion from #201 (and https://github.com/WebAssembly/reference-types/issues/55). Sorry if that wasn't clear.