Require type exports to always ascribe a type

[lukewagner]

This is a tweak recommended by @pl-semiotics earlier as part of formalizing the semantics of resource types. It's technically a breaking change, but not in the grammar, just the validation rules for resource-type-exports, which, iirc, was only implemented recently and so this might not break anyone in practice (but let me know if otherwise).

So, the basic motivation for the change is that, from first principles, for the following component implementation:

(component
  (import "T" (type $T (sub resource)))
  (type $U (resource (rep i32)))
  (export "T1" (type $T))
  (export "T2" (type $T))
  (export "U1" (type $U))
  (export "U2" (type $U))
)

It's tricky to know what the implied component type is. I believe the explainer currently says it's:

(component
  (import "T" (type $T (sub resource)))
  (export "T1" (type (eq $T)))
  (export "T2" (type (eq $T)))
  (export $U1 "U1" (type (sub resource)))
  (export "U2" (type (eq $U1)))
)

but you might instead expect:

(component
  (import "T" (type $T (sub resource)))
  (export "T1" (type (eq $T)))
  (export "T2" (type (eq $T)))
  (export "U1" (type (sub resource)))
  (export "U2" (type (sub resource)))
)

or, for uniformity:

(component
  (import "T" (type (sub resource)))
  (export "T1" (type (sub resource)))
  (export "T2" (type (sub resource)))
  (export "U1" (type (sub resource)))
  (export "U2" (type (sub resource)))
)

All three of these component types can be assigned to the component using the optional type ascription immediate of exports, so this is only a question of what the default/inferred type is. After some discussion of what, in principle, the right default inferred type should be, it started to become clear that it's rather ambiguous and maybe we should sidestep the issue altogether and just say that type exports must always ascribe a type. A small practical benefit is that this removes a bit of inference logic (that needs to ask "is this already exported?" etc).

@alexcrichton WDYT?

[alexcrichton]

Hm so first it may be worth clarifying a few things perhaps?

First is that from a breaking change perspective this will definitely affect components today. For example given this WIT

package foo:bar

world foo {
  export a: interface {
    resource x
    type y = x
    type z = y
  }
}

you get this wasm

$ wasm-tools component embed foo.wit --dummy | wasm-tools component new -t
...
  (component (;0;)
    (import "import-type-x" (type (;0;) (sub resource)))
    (export (;1;) "x" (type 0))
    (export (;2;) "y" (type 1))
    (export (;3;) "z" (type 2))
  )
...

Second is that, somewhat ironically, type ascription on resource type exports is one of the only features not implemented resource-related in wasmparser right now. That would need to be figured out first and we largely punted on it as it brought up various questions about free variables sets and how to perform subtyping and such. For example you need to perform a subtyping check but with some sort of substitution map for ascription and exporting a resource type with an ascribed type would be modifying the substitution map while everything else would use the substitution map, or something like that. Basically it was tricky enough we punted on it, so a type-ascribed resource is always an error today because a fresh resource isn't a subtype of any other resource.

Third is that I can confirm the meaning of the above component. Given this test case:

(component
  (component $take-two
    (import "a" (type $a (sub resource)))
    (import "b" (type $b (eq $a)))
  )

  (component $define-T
    (type $T (resource (rep i32)))
    (export "T" (type $T))
  )
  (component $c
    (import "T" (type $T (sub resource)))
    (type $U (resource (rep i32)))
    (export "T1" (type $T))
    (export "T2" (type $T))
    (export "U1" (type $U))
    (export "U2" (type $U))
  )
  (instance $define-T (instantiate $define-T))

  (instance $c (instantiate $c (with "T" (type $define-T "T"))))

  (instance (instantiate $take-two
    (with "a" (type $c "T1")) (with "b" (type $c "T1"))))
  (instance (instantiate $take-two
    (with "a" (type $c "T2")) (with "b" (type $c "T2"))))
  (instance (instantiate $take-two
    (with "a" (type $c "U1")) (with "b" (type $c "U1"))))
  (instance (instantiate $take-two
    (with "a" (type $c "U2")) (with "b" (type $c "U2"))))

  (instance (instantiate $take-two
    (with "a" (type $c "T1")) (with "b" (type $c "T2"))))
  (instance (instantiate $take-two
    (with "a" (type $c "T2")) (with "b" (type $c "T1"))))

  (instance (instantiate $take-two
    (with "a" (type $c "U1")) (with "b" (type $c "U2"))))
  (instance (instantiate $take-two
    (with "a" (type $c "U2")) (with "b" (type $c "U1"))))
)

this validates with:

wasm-tools validate foo.wat --features component-model

which matches the component type that you mention first.

---

With all that, I wanted to dig more into:

it started to become clear that it's rather ambiguous

Could y'all expand a bit on this? My understanding is that if you export a resource it's always equivalent to the definition at this time, which doesn't feel ambiguous. I do agree that what one might expect could cause ambiguity, and this is probably something we could document better, but given that there is a single rule of thumb that covers all these I wouldn't personally reach the same conclusion that we should require type ascription.

I suspect y'all have more cases you discussed though, which I'd like to learn more about!

[lukewagner]

First is that from a breaking change perspective this will definitely affect components today.

I know it's expressible, I was just guessing that, at this point in time, the only examples of this would be test cases and not things people are actually creating (I assume resources are imported a lot, just not exported).

I suspect y'all have more cases you discussed though, which I'd like to learn more about!

Nah, it mostly just seemed unclear how "share-y" resource type exports should be when exported (you could make arguments for any of the 3 types I showed). That being said, I don't feel strongly about this at all; I just thought that, if it was an easy change (if resource type export ascription were implemented, then it'd mostly be just deleting code), it might be a good conservative change to make in the short-term, as it's easy to relax in the future. But if it's non-trivial work, it doesn't seem like a priority, given all the other work to be done in the short term.

[lukewagner]

Yeah, thinking about this some more, it does really seem like we have the right default atm (it's the most precise type which is a subtype of all the others), so closing the PR.

[alexcrichton]

I do think though that it might be worth considering changing things before a "final stabilization" of the component model however. The fact that Wasmtime doesn't implement type ascription on on exported resources correctly is simply a bug and needs fixing no matter what. With that fixed switching defaults and/or requiring ascription would be largely just a flip of a switch I think.

Basically I'd conclude that it'd be nontrivial work to do this now, but this theoretically won't be nontrivial work to do it later, so I wouldn't want to draw a final conclusion based on work required just yet.

[lukewagner]

Makes sense. My estimation is that, if we wanted to make the change later, it would need to be in the final "make breaking changes that require a binary rewrite" phase before 1.0 (or at least, after Preview 3). But, in that context, it would be a pretty simple rewrite rule.