[spec] Update the definition of tagtype and its subtyping (WebAssembly#1862)

Author: f52985

document/core/syntax/types.rst

@@ -483,11 +483,11 @@ Global Types
 Tag Types
 ~~~~~~~~~
 
-*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a function type.
+*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a defined type |deftype|, which expands to a function type |functype|.
 
 .. math::
    \begin{array}{llll}
-   \production{tag type} &\tagtype &::=& \functype \\
+   \production{tag type} &\tagtype &::=& \deftype \\
    \end{array}
 
 Currently tags are only used for categorizing exceptions.

document/core/valid/instructions.rst

@@ -2601,15 +2601,15 @@ Control Instructions
 
 * The tag :math:`C.\CTAGS[x]` must be defined in the context.
 
-* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
+* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`expansion <aux-expand-deftype>` of the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
 
 * The :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]` must be empty.
 
-* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of  :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
+* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
 .. math::
    \frac{
-     C.\CTAGS[x] = [t^\ast] \to []
+     \expanddt(C.\CTAGS[x]) = [t^\ast] \to []
    }{
      C \vdashinstr \THROW~x : [t_1^\ast~t^\ast] \to [t_2^\ast]
    }

document/core/valid/matching.rst

@@ -580,14 +580,22 @@ A :ref:`global type <syntax-globaltype>` :math:`(\mut_1~t_1)` matches :math:`(\m
 Tag Types
 ~~~~~~~~~
 
-A :ref:`tag type <syntax-tagtype>` :math:`\tagtype_1` matches :math:`\tagtype_2` if and only if they are the same.
+A :ref:`tag type <syntax-tagtype>` :math:`\deftype_1` matches :math:`\deftype_2` if and only if the :ref:`defined type <syntax-deftype>` :math:`\deftype_1` :ref:`matches <match-deftype>` :math:`\deftype_2`, and vice versa.
 
 .. math::
    \frac{
+     C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2
+     \qquad
+     C \vdashdeftypematch \deftype_2 \matchesdeftype \deftype_1
    }{
-     C \vdashtagtypematch \tagtype \matchestagtype \tagtype
+     C \vdashtagtypematch \deftype_1 \matchestagtype \deftype_2
    }
 
+.. note::
+   Although the conclusion of this rule looks identical to its premise,
+   they in fact describe different relations:
+   the premise invokes subtyping on defined types,
+   while the conclusion defines it on tag types that happen to be expressed as defined types.
 
 .. index:: external type, function type, table type, memory type, global type
 .. _match-externtype:

document/core/valid/types.rst

@@ -551,19 +551,25 @@ Memory Types
 Tag Types
 ~~~~~~~~~
 
-:math:`[t_1^n] \to [t_2^m]`
-...........................
+:math:`\deftype`
+................
 
-* The :ref:`function type <syntax-functype>` :math:`[t_1^n] \to [t_2^m]` must be :ref:`valid <valid-functype>`.
+
+* The :ref:`defined type <syntax-deftype>` :math:`\deftype` must be :ref:`valid <valid-deftype>`.
+
+* The :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` must be a :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^n] \toF [t_2^m]`.
 
 * The type sequence :math:`t_2^m` must be empty.
 
 * Then the tag type is valid.
 
 .. math::
    \frac{
+     C \vdashdeftype \deftype \ok
+     \qquad
+     \expanddt(\deftype) = \TFUNC~[t^\ast] \to []
    }{
-     \vdashtagtype [t^\ast] \to [] \ok
+     C \vdashtagtype \deftype \ok
    }