Explaination of subtyping

[q82419]

Hi, there's a question of matching the subtype, and need the explaination for it.

As the module in the test of subtyping :

(module
  (type $s (sub (struct)))
  (type $s' (sub $s (struct)))

  (type $f1 (sub (func (param (ref $s')) (result anyref))))
  (type $f2 (sub $f1 (func (param (ref $s)) (result (ref any)))))
  (type $f3 (sub $f2 (func (param (ref null $s)) (result (ref $s)))))
  (type $f4 (sub $f3 (func (param (ref null struct)) (result (ref $s')))))
)

This module should pass the validation.
When validating the type $f2, follow the rule of validating a sub type:

• (Checked) The comptype func (param (ref $s)) (result (ref any)) must be valid.
• (Checked) The super type sequence must no longer than 1.
• For every type index in super type sequence (currently $f1):
  • (Checked) The type index must smaller than x.
  • (Checked) The type index must exist in the context.
  • (Checked) Unrolling the type index as subtype: sub (func (param (ref $s')) (result anyref))
  • (Checked) The unrolled sub (func (param (ref $s')) (result anyref)) must not contain final.
  • (Checked) Let the comptype' of this subtype be func (param (ref $s')) (result anyref)).
  • The comptype func (param (ref $s)) (result (ref any)) must match comptype' func (param (ref $s')) (result anyref)).

For the final step matching, follow the rule of matching function type, the ref $s should match ref $s', and the ref any should match anyref.

That is, the defined type $s should match defined type $s'.

According to the rule of matching defined types, the type $s matches $s' iff the $s is equal to $s' or there exists any super type in unrolled $s matches $s'.
But $s has no super type index.
Can you help to explain why the defined type $s matches defined type $s'? Thanks!

[rossberg]

You probably missed that function subtyping is contravariant in the parameters, i.e., the subtyping rule switches direction for the parameter types (in Wasm's rule, the premise t21* ≤ t11*). Thus, $s' needs to match $s, not the other way round. (Edit: fixed typo)

[q82419]

Ohhhhh.....
Thanks. That make senses.
Sorry that it's hard to be discovered...