Types
During validation, the abstract syntax types described above are
elaborated into types of a different structure, which are easier to
work with. Elaborated types are different from the original abstract
syntax types in three major aspects:
They do not contain any indirections through type index spaces:
since recursive types are explicitly not permitted by the component
model, it is possible to simply inline all such indirections.
Due to the above, instance and component types do not contain any
embedded declarations; the type sharing that necesstated the use of
type alias declarations is replaced with explicit binders and type
variables.
Value types have been despecialised: the value type constructors
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{tuple}}\), \(\href{../syntax/types.html#syntax-valtype}{\mathsf{flags}}\), \(\href{../syntax/types.html#syntax-valtype}{\mathsf{enum}}\),
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{option}}\), \(\href{../syntax/types.html#syntax-valtype}{\mathsf{union}}\), \(\href{../syntax/types.html#syntax-valtype}{\mathsf{result}}\), and
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{string}}\) have been replaced by equivalent types.
This elaboration also ensures that the type definitions themselves
have valid structures, and so may be considered as validation on
types.
Primitive value types
Any \(\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\), \(\href{../syntax/types.html#syntax-defvaltype}{\mathit{defvaltype}}\), or \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)
elaborates to a a \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\). The syntax of \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\)
is specified by parts over the next several sections, as it becomes
relevant.
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(evaltype)} & \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} &::=&
\href{../valid/types.html#syntax-evaltype}{\mathsf{bool}}\\&&|&
\href{../valid/types.html#syntax-evaltype}{\mathsf{s8}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{u8}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{s16}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{u16}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{s32}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{u32}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{s64}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{u64}}\\&&|&
\href{../valid/types.html#syntax-evaltype}{\mathsf{float32}} | \href{../valid/types.html#syntax-evaltype}{\mathsf{float64}}\\&&|&
\href{../valid/types.html#syntax-evaltype}{\mathsf{char}}\\&&|&
\href{../valid/types.html#syntax-evaltype}{\mathsf{list}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\&&|&
\dots\\
\end{array}\end{split}\]
Because values are used linearly, values in the context must be
associated with information about whether they are alive or dead. This
is accomplished by assigning them types from \(\href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}\):
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(evaltypead)} & \href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}} &::=&
\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\&&|&
\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}^\dagger
\end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{string}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{string}} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathsf{list}}~\href{../valid/types.html#syntax-evaltype}{\mathsf{char}}
}\]
\(\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\) other than \(\href{../syntax/types.html#syntax-valtype}{\mathsf{string}}\)
\[\frac{
\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}} \neq \href{../syntax/types.html#syntax-valtype}{\mathsf{string}}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\vdash}} \href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\leadsto}} \href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}
}\]
Record fields
Any \(\href{../syntax/types.html#syntax-recordcase}{\mathit{record\_field}}\) elaborates to a \(\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}\) with
the following abstract syntax:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(erecordfield)} & \href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e} &::=&
\{ \href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \}\\
\end{array}\end{split}\]
The type of the record field must elaborate to some \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\)
Then the record field elaborates to an \(\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}\) of the
same name with the type \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-rftoerf}{\vdash}} \{ \href{../syntax/types.html#syntax-recordcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-recordcase}{\mathsf{type}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \}
\mathrel{\href{../valid/types.html#elaborate-rftoerf}{\leadsto}} \{ \href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \}
}\]
Variant cases
Because validation must ensure that a variant case which refines
another case has a compatible type, a variant case elaborates to an
\(\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}\) in a special context \(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}\):
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(vcctx)} & \href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}} &::=&
\{ \href{../valid/types.html#syntax-vcctx}{\mathsf{ctx}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}, \href{../valid/types.html#syntax-vcctx}{\mathsf{cases}}~\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}^{*} \}\\
\def\mathdef454#1{{}}\mathdef454{(evariantcase)} & \href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e} &::=&
\{ \href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}^?, \href{../valid/types.html#syntax-evariantcase}{\mathsf{refines}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}^? \}\\
\end{array}\end{split}\]
If the variant case contains a type, it must elaborate to some \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
If an index \(i\) is present in the \(\href{../syntax/types.html#syntax-variantcase}{\mathsf{refines}}\) record of
the variant case type, then \(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}.\href{../valid/types.html#syntax-vcctx}{\mathsf{cases}}[i]\) must be
present, and:
If the variant case does not contain a type,
\(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}.\href{../valid/types.html#syntax-vcctx}{\mathsf{cases}}[i]\) must not contain a type.
If the variant case contains a type, then
\(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}.\href{../valid/types.html#syntax-vcctx}{\mathsf{cases}}[i]\) must also contain an elaborated type,
and the elaborated form of the cases’ type must be a subtype of
that type.
Then the variant case elaborates to an \(\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}\) of the
same name, with:
If the variant case does not contain a type, then no type.
If the variant case does contain a type, then the
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) to which it elaborates.
If the variant case does not contain a refines index, then no
refines name.
If the variant case does contain a refines index \(i\), then a
refines name of \(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}.\href{../valid/types.html#syntax-vcctx}{\mathsf{cases}}[i].\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i, \href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}.\href{../valid/types.html#syntax-vcctx}{\mathsf{ctx}} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\\
\forall j, \href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}.\href{../valid/types.html#syntax-vcctx}{\mathsf{cases}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_j] = \{ \href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_j, \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\overline{{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}'}_k}, \dots \} \land \forall i, {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i \preccurlyeq {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}'}_i
\end{array}
}{
\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}} \mathrel{\href{../valid/types.html#elaborate-vctoevc}{\vdash}} \{ \href{../syntax/types.html#syntax-variantcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-variantcase}{\mathsf{type}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}, \href{../syntax/types.html#syntax-variantcase}{\mathsf{refines}}~\overline{\href{../syntax/values.html#syntax-int}{\mathit{u32}}_j} \}
\mathrel{\href{../valid/types.html#elaborate-vctoevc}{\leadsto}} \{ \href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\overline{{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i}, \href{../syntax/types.html#syntax-variantcase}{\mathsf{refines}}~\overline{\href{../syntax/values.html#syntax-name}{\mathit{name}}_j} \}
}\end{split}\]
Definition value types
A definition value type elaborates to a \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\). The syntax
of \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) is broader than shown earlier:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(evaltype2)} & \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} &::=&
\dots\\&&|&
\href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}^{+}\\&&|&
\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}^{+}\\&&|&
\href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-refscope}{\mathit{scope}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{prim}}~\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\)
The primitive value type \(\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\) must elaborate to some
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
Then the definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{prim}}~\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\)
elaborates to the the the same \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\vdash}} \href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{prim}}~\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{record}}~\href{../syntax/types.html#syntax-recordcase}{\mathit{record\_field}}^{+}\)
Each record field declaration \(\href{../syntax/types.html#syntax-recordcase}{\mathit{record\_field}}_i\) must elaborate
to some \({\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}}_i\).
The \(\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}\)s of the \({\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}}_i\) must all be
distinct.
Then the definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{record}}~\overline{\href{../syntax/types.html#syntax-recordcase}{\mathit{record\_field}}_i}^n\)
elaborates to \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\overline{{\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}}_i}^n\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-rftoerf}{\vdash}} \href{../syntax/types.html#syntax-recordcase}{\mathit{record\_field}}_i \mathrel{\href{../valid/types.html#elaborate-rftoerf}{\leadsto}} {\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}}_i\\
\forall i j, {\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}}_i.\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}} = {\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}}_j.\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}} \Rightarrow i = j
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{record}}~\overline{{\href{../syntax/types.html#syntax-recordcase}{\mathit{record\_field}}}_i}^n
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\overline{{\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}}_i}^n
}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{variant}}~\href{../syntax/types.html#syntax-variantcase}{\mathit{variant\_case}}^{+}\)
Each variant case declaration \(\href{../syntax/types.html#syntax-variantcase}{\mathit{variant\_case}}_i\) must elaborate
to some \({\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_i\), in a variant-case context
\(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}_i\) where:
\(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}_i.\href{../valid/types.html#syntax-vcctx}{\mathsf{ctx}} = \Gamma\)
\(\href{../valid/types.html#syntax-vcctx}{\mathit{vcctx}}_i.\href{../valid/types.html#syntax-vcctx}{\mathsf{cases}} = {\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_1, \dots,
{\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_{i-1}\)
The \(\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}\)s of the \({\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_i\) must all be
distinct.
Then the definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{variant}}~\overline{\href{../syntax/types.html#syntax-variantcase}{\mathit{variant\_case}}_i}^n\)
elaborates to \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\overline{{\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_i}^n\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i, \{ \href{../valid/types.html#syntax-vcctx}{\mathsf{ctx}}~\Gamma, \href{../valid/types.html#syntax-vcctx}{\mathsf{cases}}~{\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_1,\dots,{\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_{i-1} \} \mathrel{\href{../valid/types.html#elaborate-vctoevc}{\vdash}} \href{../syntax/types.html#syntax-variantcase}{\mathit{variant\_case}}_i \mathrel{\href{../valid/types.html#elaborate-vctoevc}{\leadsto}} {\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_i\\
\forall i, j {\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_i.\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}} = {\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_j.\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}} \Rightarrow i = j
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{variant}}~\overline{\href{../syntax/types.html#syntax-variantcase}{\mathit{variant\_case}}_i}^n
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\overline{{\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}}_i}^n
}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{list}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)
The list element type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must elaborate to some
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
Then the definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{list}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) elaborates
to \(\href{../valid/types.html#syntax-evaltype}{\mathsf{list}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{list}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathsf{list}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{tuple}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}\)
Each tuple element type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i\) must elaborate to some
\({\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\).
Then the definition value type
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{tuple}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}\) elaborates to
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\overline{\{\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~''i'',\href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\}}\).
\[\frac{
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{tuple}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\overline{\{\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~''i'',\href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\}}
}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{flags}}~\overline{\href{../syntax/values.html#syntax-name}{\mathit{name}}_i}\)
The definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{flags}}~\overline{\href{../syntax/values.html#syntax-name}{\mathit{name}}_i}\)
elaborates to \(\href{../syntax/types.html#syntax-valtype}{\mathsf{record}}~\overline{\{\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathsf{bool}}\}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{flags}}~\overline{\href{../syntax/values.html#syntax-name}{\mathit{name}}_i}
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\overline{\{\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathsf{bool}}\}}
}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{enum}}~\overline{\href{../syntax/values.html#syntax-name}{\mathit{name}}_i}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{enum}}~\overline{\href{../syntax/values.html#syntax-name}{\mathit{name}}_i}
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../syntax/types.html#syntax-valtype}{\mathsf{variant}}~\overline{\{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i\}}
}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{option}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)
The type contained in the option \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must elaborate to
some \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
Then the definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{option}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) elaborates
to \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\{ \href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''none'' \}~\{ \href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''some'',
\href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{option}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\{ \href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''none'' \}~\{ \href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''some'', \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \}
}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{union}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}\)
Each value type valtype_i must elaborate to some \({\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\).
Then the definition value type
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{union}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}\) elaborates to
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\overline{\{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''i'', \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\}}\).
\[\frac{
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{union}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\overline{\{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''i'', \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\}}
}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{result}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'_j}\)
Each value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i\) must elaborate to some \({\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\).
Each value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'_j\) must elaborate to some
\({\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}'_j\).
Then the definition value type
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{result}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'_j}\)
elaborates to \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''ok'', \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\overline{{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i}\}~\{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''error'', \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\overline{{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}'}_j}\}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\\
\forall j, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'_j \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}'}_j\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}}{}&\href{../syntax/types.html#syntax-valtype}{\mathsf{result}}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i}~\overline{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'_j}\\
\mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}}{}&\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''ok'', \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\overline{{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i}\}~\{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~''error'', \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~\overline{{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}'}_j}\}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{own}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the
context, and must be a subtype of \(\mathsf{resource}\).
Then the definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{own}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\) elaborates
to \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \preccurlyeq \mathsf{resource}\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{own}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{borrow}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the
context, and must be a subtype of \(\mathsf{resource}\).
Then the definition value type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{borrow}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\) elaborates
to \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-refscope}{\mathsf{call}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \preccurlyeq \mathsf{resource}\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathsf{borrow}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-refscope}{\mathsf{call}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\end{split}\]
Value types
\(\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\)
A value type of the form \(\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\) must be a
\(\href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}}\) which elaborates to some \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
Then the value type elaborates to the same \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\vdash}} \href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}} \mathrel{\href{../valid/types.html#elaborate-pvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-primvaltype}{\mathit{primvaltype}} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\]
\(\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the
context.
Then the value type \(\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\) elaborates to
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\).
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]
}\]
Value type well-formedness
Since certain value types cannot appear in certain places (most
notably, \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-refscope}{\mathsf{call}}\) may not appear anywhere save a
function parameter type), we define a family of well-formedness
judgments. Each context which may require a \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) uses one
of these well-formedness judgments to ensure that it is of correct
form.
Note that the variable scoping constraints should already be enforced
by earlier elaboration stages, which never generate free type
variables, but they are included here for completeness.
We define a formal syntax of the position parameters which may be used:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(evaltypepos)} & {\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} &::=&
{\href{../valid/types.html#syntax-evaltypepos}{\epsilon}}\\&&|&
{\href{../valid/types.html#syntax-evaltypepos}{\mathsf{p}}}\\
\end{array}\end{split}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{bool}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{bool}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{s8}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{s8}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{u8}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{u8}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{s16}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{s16}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{u16}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{u16}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{s32}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{s32}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{u32}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{u32}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{s64}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{s64}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{u64}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{u64}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{float32}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{float32}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{float64}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{float64}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{char}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{char}}
}\]
\(\href{../valid/types.html#syntax-evaltype}{\mathsf{list}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\)
In any context and any position, if \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) is
well-formed, then \(\href{../valid/types.html#syntax-evaltype}{\mathsf{list}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) is well-formed.
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathsf{list}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\]
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\href{../valid/types.html#syntax-erecordfield}{\mathit{record\_field}_e}^{\ast}\)
In any context and any position, if each \(\href{../syntax/values.html#syntax-name}{\mathit{name}}_i\) is
distinct, and each \({\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\) is well-formed, then
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\overline{\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i}\) is well-formed.
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i j, i \neq j \Rightarrow \href{../syntax/values.html#syntax-name}{\mathit{name}}_i \neq name_j\\
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}}
\href{../valid/types.html#syntax-evaltype2}{\mathsf{record}}~\overline{\href{../valid/types.html#syntax-erecordfield}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../valid/types.html#syntax-erecordfield}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i}
}\end{split}\]
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\href{../valid/types.html#syntax-evariantcase}{\mathit{variant\_case}_e}^{+}\)
In any context and any position, if each \(\href{../syntax/values.html#syntax-name}{\mathit{name}}_i\) is
distinct, and each \({\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\) is well-formed, and each
\(\href{../syntax/values.html#syntax-int}{\mathit{u32}}^?_i\) does not refer to a non-existent or
self-referential case, then
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\overline{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}^?}_i, \href{../valid/types.html#syntax-evariantcase}{\mathsf{refines}}}\) is well-formed.
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i j, i \neq j \Rightarrow \href{../syntax/values.html#syntax-name}{\mathit{name}}_i \neq \href{../syntax/values.html#syntax-name}{\mathit{name}}_j\\
\forall i, \forall \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}, {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}^?}_i = \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \Rightarrow \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}}
\href{../valid/types.html#syntax-evaltype2}{\mathsf{variant}}~\overline{\href{../valid/types.html#syntax-evariantcase}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../valid/types.html#syntax-evariantcase}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}^?}_i, \href{../valid/types.html#syntax-evariantcase}{\mathsf{refines}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}^?_i}^n
}\end{split}\]
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~\mathit{rtidx}\)
The resource type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{rtypes}}[\mathit{rtidx}]\) must be defined
in the context.
Then in any position, \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~\mathit{rtidx}\) is
well-formed.
\[\frac{
\exists \href{../valid/types.html#syntax-eresourcetype}{\mathit{resourcetype}_e}, \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{rtypes}}[\mathit{rtidx}] = \href{../valid/types.html#syntax-eresourcetype}{\mathit{resourcetype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~\mathit{rtidx}
}\]
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\alpha\)
The type variable \(\alpha\) must be defined in the context with
a bound of \(\href{../valid/types.html#syntax-etypebound}{\mathsf{sub~resource}}\).
Then in any position, \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\alpha\) is well-formed.
\[\frac{
(\alpha : \href{../valid/types.html#syntax-etypebound}{\mathsf{sub~resource}}) \in \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}} \lor \exists \href{../valid/types.html#syntax-eresourcetype}{\mathit{resourcetype}_e}, (\alpha : \href{../valid/types.html#syntax-etypebound}{\mathsf{sub~resource}}, \href{../valid/types.html#syntax-eresourcetype}{\mathit{resourcetype}_e}) \in \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{evars}}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\alpha
}\]
\(\href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\)
The value type \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\) must be well-formed in the
context in parameter position.
Then \(\href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-refscope}{\mathsf{call}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\) is well-formed in parameter
position.
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathsf{p}}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{own}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathsf{p}}} \href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-refscope}{\mathsf{call}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}
}\]
Result types
Because a \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}\) may appear in a parameter position or in
a return position, its elaboration is parametrized by which position
it appears in.
Any \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}\) elaborates to a \(\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}\) with the
following abstract syntax:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(eresulttype)} & \href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e} &::=&
\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\&&|&
\{ \href{../valid/types.html#syntax-eresulttype}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eresulttype}{\mathsf{type}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e} \}^\ast
\end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)
\(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must elaborate to some \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\)
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) must be valid in the appropriate position.
Then the result type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) elaborates to \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-rttoert}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\href{../valid/types.html#elaborate-rttoert}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\end{split}\]
\(\overline{\{\href{../syntax/types.html#syntax-resulttype}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../syntax/types.html#syntax-resulttype}{\mathsf{type}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i\}}\)
Each \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i\) must elaborate to some \({\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\).
Then the result type \(\overline{\{\href{../syntax/types.html#syntax-resulttype}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../syntax/types.html#syntax-resulttype}{\mathsf{type}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i\}}\) elaborates to
\(\overline{\{\href{../valid/types.html#syntax-eresulttype}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../valid/types.html#syntax-eresulttype}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\}}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\vdash}} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i \mathrel{\href{../valid/types.html#elaborate-vttoevt}{\leadsto}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\\
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} {\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-rttoert}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathit{\rho}}} \overline{\{\href{../syntax/types.html#syntax-resulttype}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../syntax/types.html#syntax-resulttype}{\mathsf{type}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_i\}} \mathrel{\href{../valid/types.html#elaborate-rttoert}{\leadsto}} \overline{\{\href{../valid/types.html#syntax-eresulttype}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../valid/types.html#syntax-eresulttype}{\mathsf{type}}~{\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}}_i\}}
}\end{split}\]
Function types
Any \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) elaborates to a \(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\) with the
following abstract syntax:
\[\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(efunctype)} & \href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e} &::=&
\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}\to\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}
\end{array}\]
\(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_1 \to \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_2\)
\(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_1\) must elaborate in parameter position to some
\({\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_1\).
\(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_2\) must elaborate to some \({\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_2\).
Then the function type \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_1\to\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_2\)
elaborates to \({\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_1\to{\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_2\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-rttoert}{\vdash}}_{\href{../valid/types.html#syntax-evaltypepos}{\mathsf{p}}} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_1 \mathrel{\href{../valid/types.html#elaborate-rttoert}{\leadsto}} {\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_1\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-rttoert}{\vdash}} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_2 \mathrel{\href{../valid/types.html#elaborate-rttoert}{\leadsto}} {\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_2\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-fttoeft}{\vdash}} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_1\to\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_2
\mathrel{\href{../valid/types.html#elaborate-fttoeft}{\leadsto}} {\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_1\to{\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_2
}\end{split}\]
Type bound
A type bound elaborates to a \(\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}\) with the following
abstract syntax:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(etypebound)} & \href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e} &::=& \href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\&&|&
\href{../valid/types.html#syntax-etypebound}{\mathsf{sub~resource}}\\
\end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-typebound}{\mathsf{EQ}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the context.
Then the type bound \(\href{../syntax/types.html#syntax-typebound}{\mathsf{EQ}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\) elaborates to
\(\href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\).
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-tbtoetb}{\vdash}} \href{../syntax/types.html#syntax-typebound}{\mathsf{EQ}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-tbtoetb}{\leadsto}} \href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]
}\]
\(\href{../syntax/types.html#syntax-typebound}{\mathsf{SUB~resource}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-tbtoetb}{\vdash}} \href{../syntax/types.html#syntax-typebound}{\mathsf{SUB~resource}} \mathrel{\href{../valid/types.html#elaborate-tbtoetb}{\leadsto}} \href{../valid/types.html#syntax-etypebound}{\mathsf{sub~resource}}
}\]
Instance types
An elaborated instance type is nothing more than a list of its exports
behind existential quantifiers for exported types:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(einstancetype)} & \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e} &::=& \exists \href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^{*}\\
\def\mathdef454#1{{}}\mathdef454{(boundedtyvar)} & \href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}} &::=& (\alpha : \href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e})\\
\def\mathdef454#1{{}}\mathdef454{(eexterndecl)} & \href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e} &::=& \{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\\
\def\mathdef454#1{{}}\mathdef454{(eexterndesc)} & \href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} &::=&
\href{../valid/types.html#syntax-eexterndesc}{\mathsf{core\_module}}~\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\\&&|&
\href{../valid/types.html#syntax-eexterndesc}{\mathsf{func}}~\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\\&&|&
\href{../valid/types.html#syntax-eexterndesc}{\mathsf{value}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\&&|&
\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\&&|&
\href{../valid/types.html#syntax-eexterndesc}{\mathsf{instance}}~\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\\&&|&
\href{../valid/types.html#syntax-eexterndesc}{\mathsf{component}}~\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\\
\end{array}\end{split}\]
Because instance value exports must be used linearly in the context,
instances in the contexts are, by analogy with \(\href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}\),
assigned types from \(\href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}}\).
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(einstancetypead)} & \href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}} &::=&
\exists\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}^{*}\\
\def\mathdef454#1{{}}\mathdef454{(eexterndeclad)} & \href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}} &::=&
\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}\\&&|&
\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\dagger\\
\end{array}\end{split}\]
Notational conventions
We write \(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e} \oplus \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}'\) to mean the
instance type formed by the concationation of the export
declarations of \(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\) and \(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}'\).
We write \(\bigoplus_i {\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_i\) to mean the instance
type formed by \({\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_1 \oplus \dots \oplus
{\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_n\).
Finalize: \(\href{../valid/types.html#auxiliary-ifinalize}{\langle\mkern-5mu\langle} \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e} \href{../valid/types.html#auxiliary-ifinalize}{\rangle\mkern-5mu\rangle}\)
Finalizing an instance type eliminates unnecessary type variables with
equality constraints, ensures that all type variables are well-scoped,
and that all quantified types are exported.
Each type variable existentially quantified in
\(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\) must either be exported or have an equality
type bound.
Then the finalized version of \(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\) is that type,
with each type variable which is not exported replaced by the type
that it is equality-bounded to.
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\mathrm{defined}(\alpha) =
\begin{cases}
\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e} & \text{if } \exists i, \alpha_i = \alpha \land {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}_i = \href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\bot & \text{otherwise}\\
\end{cases}\\
\mathrm{externed}(\alpha) =
\begin{cases}
\top & \text{if } \exists i, \alpha_i = \alpha \land \exists\href{../syntax/values.html#syntax-name}{\mathit{name}}, \{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\alpha \} \in \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_j}\\
\bot & \text{otherwise}\\
\end{cases}\\
\forall i, \mathrm{defined}(\alpha_i) \lor \mathrm{externed}(\alpha_i)\\
\delta(\alpha) = \begin{cases}
\mathrm{defined}(\alpha) & \text{if }\neg\mathrm{externed}(\alpha)\\
\bot & \text{otherwise}\\
\end{cases}\\
\overline{i} = \{ i \mid \mathrm{externed}(\alpha_i) \}\\
\end{array}
}{
\begin{aligned}
&\href{../valid/types.html#auxiliary-ifinalize}{\langle\mkern-5mu\langle} \exists \overline{(\alpha_i : {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}_i)}. \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}'_j} \href{../valid/types.html#auxiliary-ifinalize}{\rangle\mkern-5mu\rangle}\\
={}&\delta(\exists \overline{(\alpha_i : {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}_i)}^{i \in \overline{i}}. \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}'_j})\\
\end{aligned}
}\end{split}\]
\(\overline{\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}_i}\)
\(\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}_1\) must elaborate to some
\({\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_1\) in the context
\(\{\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}\}\).
For each \(i > 1\), the instance declarator
\(\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}_i\) must elaborate in the context produced by
the elaboration of \(\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}_{i-1}\) to some
\({\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_i\).
Then the instance type \(\overline{\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}_i}\) elaborates
to \(\bigoplus_i {\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_i\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}_0 = \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \}\\
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_{i-1} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\vdash}} \href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}_i
\mathrel{\href{../valid/types.html#elaborate-idtoeit}{\leadsto}} {\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_i \dashv \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_i
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-ittoeit}{\vdash}} \overline{\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}_i}
\mathrel{\href{../valid/types.html#elaborate-ittoeit}{\leadsto}} \href{../valid/types.html#auxiliary-ifinalize}{\langle\mkern-5mu\langle} \bigoplus_i {\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}}_i \href{../valid/types.html#auxiliary-ifinalize}{\rangle\mkern-5mu\rangle}
}\end{split}\]
Instance declarators
Each instance declarator elaborates to a (partial)
\(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\).
\(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{alias}}~\href{../syntax/types.html#syntax-alias}{\mathit{alias}}\)
The \(\href{../syntax/types.html#syntax-alias}{\mathit{alias}}.\href{../syntax/types.html#syntax-alias}{\mathsf{sort}}\) must be \(\href{../syntax/components.html#syntax-sort}{\mathsf{type}}\).
The \(\href{../syntax/types.html#syntax-alias}{\mathit{alias}}.\href{../syntax/types.html#syntax-alias}{\mathsf{target}}\) must be of the form
\(\href{../syntax/components.html#syntax-aliastarget}{\mathsf{outer}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i\).
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\) must be
defined in the context.
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\) must not
be of the form \(\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~i\) for any i.
Then the instance declarator \(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{alias}}~\href{../syntax/types.html#syntax-alias}{\mathit{alias}}\) elaborates to the empty
list of exports, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) in the context to the
original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) followed by
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../syntax/types.html#syntax-alias}{\mathit{alias}}.\href{../syntax/types.html#syntax-alias}{\mathsf{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{type}}\\
\href{../syntax/types.html#syntax-alias}{\mathit{alias}}.\href{../syntax/types.html#syntax-alias}{\mathsf{target}} = \href{../syntax/components.html#syntax-aliastarget}{\mathsf{outer}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i\\
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i] \neq \href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~i\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\vdash}} \href{../syntax/types.html#syntax-instancedecl}{\mathsf{alias}}~\href{../syntax/types.html#syntax-alias}{\mathit{alias}} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\leadsto}}
\exists\varnothing. \varnothing \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i] \}
}\end{split}\]
\(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{core\_type}}~\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{type}}\)
The core type definition \(\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{type}}\) must elaborate to some
elaborated core type \(\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}\).
Then the instance declarator \(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{core\_type}}~\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{type}}\)
elaborates to the empty list of exports, and sets
\(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\) in the context to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\) followed by the
\(\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{type}} \leadsto \href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\vdash}} \href{../syntax/types.html#syntax-instancedecl}{\mathsf{core\_type}}~\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{type}} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\leadsto}}
\exists\varnothing. \varnothing \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}~\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}~\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e} \}
}\]
\(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{type}}~\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\)
The definition type \(\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\) must elaborate to some
elaborated definition type \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\).
Let \(\alpha\) be a fresh type variable.
Then the instance declarator \(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{type}}~\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\) elaborates to
the empty list of exports behind an existential quantifier
associating \(\alpha\) with \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\), and sets
\(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) in the context to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) followed by the \(\alpha\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\vdash}} \href{../syntax/types.html#syntax-deftype}{\mathit{deftype}} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\leadsto}} \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\vdash}} \href{../syntax/types.html#syntax-instancedecl}{\mathsf{type}}~\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\leadsto}}
\exists(\alpha : \href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}). \varnothing
\mathrel{\href{../valid/types.html#elaborate-idtoeit}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{evars}}~(\alpha : \href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}, \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}), \href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}~\alpha \}
}\]
Notice that because this type variable is equality-bounded and not
exported, it will always be inlined by \(\href{../valid/types.html#auxiliary-ifinalize}{\langle\mkern-5mu\langle}
\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e} \href{../valid/types.html#auxiliary-ifinalize}{\rangle\mkern-5mu\rangle}\).
\(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{export}}~\href{../syntax/types.html#syntax-exportdecl}{\mathit{exportdecl}}\)
The extern descriptor \(\href{../syntax/types.html#syntax-exportdecl}{\mathit{exportdecl}}.\href{../syntax/types.html#syntax-exportdecl}{\mathsf{desc}}\) must elaborate to
some \(\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\).
Then the instance declarator \(\href{../syntax/types.html#syntax-instancedecl}{\mathsf{export}}~\href{../syntax/types.html#syntax-exportdecl}{\mathit{exportdecl}}\)
elaborates to the singleton list of exports containing
\(\{\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/types.html#syntax-exportdecl}{\mathit{exportdecl}}.\href{../syntax/types.html#syntax-exportdecl}{\mathsf{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\) and
quantified by \(\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}\), and adds an appropriately typed
entry to the context.
\[\begin{split}\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-exportdecl}{\mathit{exportdecl}}.\href{../syntax/types.html#syntax-exportdecl}{\mathsf{desc}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\vdash}}{}& \href{../syntax/types.html#syntax-exportdecl}{\mathit{exportdecl}}\\
\mathrel{\href{../valid/types.html#elaborate-idtoeit}{\leadsto}}{}&\exists\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/types.html#syntax-exportdecl}{\mathit{exportdecl}}.\href{../syntax/types.html#syntax-exportdecl}{\mathsf{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\\
\mathrel{\href{../valid/types.html#elaborate-idtoeit}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}}~\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast, \href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}
\end{aligned}
}\end{split}\]
Extern descriptors
An extern descriptor elaborates to a quantified \(\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\)
with the following abstract syntax:
\(\href{../syntax/types.html#syntax-externdesc}{\mathsf{type}}~\href{../syntax/types.html#syntax-typebound}{\mathit{typebound}}\)
The \(\href{../syntax/types.html#syntax-typebound}{\mathit{typebound}}\) must elaborate to some \(\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}\).
Let \(\alpha\) be a fresh type variable.
Then the import descriptor \(\href{../syntax/types.html#syntax-externdesc}{\mathsf{type}}~\href{../syntax/types.html#syntax-typebound}{\mathit{typebound}}\) elaborates to
\(\forall(\alpha : \href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}).\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\alpha\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-tbtoetb}{\vdash}} \href{../syntax/types.html#syntax-typebound}{\mathit{typebound}} \mathrel{\href{../valid/types.html#elaborate-tbtoetb}{\leadsto}} \href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-externdesc}{\mathsf{type}}~\href{../syntax/types.html#syntax-typebound}{\mathit{typebound}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \forall(\alpha : \href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}).\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\alpha
}\]
\(\href{../syntax/types.html#syntax-externdesc}{\mathsf{core\_module}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-typeidx}{\mathit{core{:}}\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}[\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-typeidx}{\mathit{core{:}}\mathit{typeidx}}]\) must be
defined in the context, and must be of the form
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
Then the import descriptor \(\href{../syntax/types.html#syntax-externdesc}{\mathsf{core\_module}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-typeidx}{\mathit{core{:}}\mathit{typeidx}}\)
elaborates to \(\forall\varnothing.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{core\_module}}~\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}[\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-typeidx}{\mathit{core{:}}\mathit{typeidx}}] = \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \forall\varnothing.\href{../syntax/types.html#syntax-externdesc}{\mathsf{core\_module}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-typeidx}{\mathit{core{:}}\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{core\_module}}~\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
}\]
\(\href{../syntax/types.html#syntax-externdesc}{\mathsf{func}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the
context, and must be of the form \(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\).
Then the import descriptor \(\href{../syntax/types.html#syntax-externdesc}{\mathsf{func}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\) elaborates to
\(\forall\varnothing.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{func}}~\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\)
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-externdesc}{\mathsf{func}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \forall\varnothing.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{func}}~\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}
}\]
\(\href{../syntax/types.html#syntax-externdesc}{\mathsf{value}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the
context, and must be of the form to some \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) must be well-formed.
Then the import descriptor \(\href{../syntax/types.html#syntax-externdesc}{\mathsf{value}}~\href{../syntax/types.html#syntax-typebound}{\mathit{typebound}}\) elaborates to
\(\forall\varnothing.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{value}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\)
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-externdesc}{\mathsf{value}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{value}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\end{split}\]
\(\href{../syntax/types.html#syntax-externdesc}{\mathsf{instance}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the
context, and must be of the form \(\exists\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\ast\).
Then the import descriptor \(\href{../syntax/types.html#syntax-externdesc}{\mathsf{instance}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\) elaborates
to \(\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{instance}}~\exists\varnothing.\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\ast\)
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[typeidx] = \exists\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\ast
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-externdesc}{\mathsf{instance}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{instance}}~\exists\varnothing.\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\ast
}\]
\(\href{../syntax/types.html#syntax-externdesc}{\mathsf{component}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the
context, and must be of the form \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\).
Then the import descriptor \(\href{../syntax/types.html#syntax-externdesc}{\mathsf{component}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\) elaborates
to \(\forall\varnothing.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{component}}~\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\)
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-externdesc}{\mathsf{component}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \forall\varnothing.\href{../valid/types.html#syntax-eexterndesc}{\mathsf{component}}~\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
}\]
Component types
In a similar manner to instance types above, component types change
significantly upon elaboration: an elaborated component type is
described as a mapping from a quantified list of imports to the type
of the instance that it will produce upon instantiation:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(ecomponenttype)} & \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e} &::=&
\forall \href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\ast \to \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\\
\end{array}\end{split}\]
Notational conventions
Much like with instance types above, we write \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
\oplus \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}'\) to mean the combination of two component
types; in this case, the component type whose imports are the
concatenation of the import lists of \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\) and
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}'\) and whose instantiation result (instance)
type is the result of applying \(\oplus\) to the instantiation
result (instance) types of \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\) and
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}'\).
Finalize: \(\href{../valid/types.html#auxiliary-cfinalize}{\langle\mkern-5mu\langle} \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e} \href{../valid/types.html#auxiliary-cfinalize}{\rangle\mkern-5mu\rangle}\)
As with instance types above, finalizing a component type eliminates
unnecessary type variables with equality constraints, ensures that all
type variables are well-scoped, and that all quantified types are
imported or exported.
Each type variable universally quantified in \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\)
must either be imported (either directly or as a type export of an
imported instance) or have an equality type bound.
Each type variable existentially quantified in
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\) must either be exported or have an equality
type bound.
Each type variable existentially quantified in
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\) that is exported must not be present in the
type of any import.
Then the finalized version of \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\) is that type,
with each type variable which is not imported or exported replaced
by the type that it is equality-bounded to.
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\mathrm{defined}(\alpha) =
\begin{cases}
\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e} & \text{if } \exists i, \alpha_i = \alpha \land {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}^\alpha_i = \href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e} & \text{if } \exists k, \beta_k = \alpha \land {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}^\beta_k = \href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\bot & \text{otherwise}\\
\end{cases}\\
\mathrm{externed}(\alpha) =
\begin{cases}
\top & \text{if } \exists i, \alpha_i = \alpha \land \exists\href{../syntax/values.html#syntax-name}{\mathit{name}}, \{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\alpha \} \in \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_j}\\
\top & \text{if } \exists j, {\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_j = \exists \overline{\alpha''}. \overline{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}''} \land \{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\alpha \} \in \overline{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}''}\\
\top & \text{if } \exists i, \beta_k = \alpha \land \exists\href{../syntax/values.html#syntax-name}{\mathit{name}}, \{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\alpha \} \in \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}'}_k}\\
\bot & \text{otherwise}\\
\end{cases}\\
\forall i, \mathrm{defined}(\alpha_i) \lor \mathrm{externed}(\alpha_i)\\
\forall k, \mathrm{defined}(\beta_k) \lor \mathrm{externed}(\beta_k)\\
\forall k, \mathrm{externed}(\beta_k) \Rightarrow \beta_k \notin \mathrm{free\_tyvars}(\overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_j})\\
\delta(\alpha) = \begin{cases}
\mathrm{defined}(\alpha) & \text{if }\neg\mathrm{externed}(\alpha)\\
\bot & \text{otherwise}\\
\end{cases}\\
\overline{i} = \{ i \mid \mathrm{externed}(\alpha_i) \}\\
\overline{k} = \{ k \mid \mathrm{externed}(\beta_k) \}\\
\end{array}
}{
\begin{aligned}
&\href{../valid/types.html#auxiliary-cfinalize}{\langle\mkern-5mu\langle} \forall \overline{(\alpha_i : {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}^\alpha_i)}. \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_j} \to \exists \overline{(\beta_k : {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}^\beta_k)}. \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}'_l} \href{../valid/types.html#auxiliary-cfinalize}{\rangle\mkern-5mu\rangle}\\
={}&\delta(\forall \overline{(\alpha_i : {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}^\alpha_i)}^{i \in \overline{i}}. \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_j} \to \exists \overline{(\beta_k : {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}^\beta_k)}^{k \in \overline{k}}. \overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}'_l})\\
\end{aligned}
}\end{split}\]
\(\overline{\href{../syntax/types.html#syntax-componentdecl}{\mathit{componentdecl}}_i}\)
\(\href{../syntax/types.html#syntax-componentdecl}{\mathit{componentdecl}}_1\) must elaborate to some
\({\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}}_1\) in the context
\(\{\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}~\Gamma\}\).
For each \(i > 1\), the component declarator
\(\href{../syntax/types.html#syntax-componentdecl}{\mathit{componentdecl}}_i\) must elaborate in the context produced by
the elaboration of \(\href{../syntax/types.html#syntax-componentdecl}{\mathit{componentdecl}}_{i-1}\) to some
\({\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}}_i\).
Then the component type \(\overline{\href{../syntax/types.html#syntax-componentdecl}{\mathit{componentdecl}}_i}\)
elaborates to the type produced by finalizing \(\bigoplus_i
{\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}}_i\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}_0 = \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \}\\
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_{i-1} \mathrel{\href{../valid/types.html#elaborate-cdtoect}{\vdash}} \href{../syntax/types.html#syntax-componentdecl}{\mathit{componentdecl}}_i
\mathrel{\href{../valid/types.html#elaborate-cdtoect}{\leadsto}} {\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}}_i \mathrel{\href{../valid/types.html#elaborate-cdtoect}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_i
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-cttoect}{\vdash}} \overline{\href{../syntax/types.html#syntax-componentdecl}{\mathit{componentdecl}}_i}
\mathrel{\href{../valid/types.html#elaborate-cttoect}{\leadsto}} \href{../valid/types.html#auxiliary-cfinalize}{\langle\mkern-5mu\langle} \bigoplus_i {\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}}_i \href{../valid/types.html#auxiliary-cfinalize}{\rangle\mkern-5mu\rangle}
}\end{split}\]
Component declarators
Each component declarator elaborates to a (partial)
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\).
\(\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}\)
The instance declarator \(\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}\) must elaborate to some
instance type \(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\) (and may affect the context).
Then the component declarator \(\href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}}\) elaborates to
the component type \(\forall\varnothing. \varnothing \to \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\) and alters
the context in the same way.
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-idtoeit}{\vdash}} \href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}} \mathrel{\href{../valid/types.html#elaborate-idtoeid}{\leadsto}} \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e} \mathrel{\href{../valid/types.html#elaborate-idtoeid}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma}'
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-cdtoect}{\vdash}} \href{../syntax/types.html#syntax-instancedecl}{\mathit{instancedecl}} \mathrel{\href{../valid/types.html#elaborate-cdtoect}{\leadsto}} \forall\varnothing. \varnothing \to \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e} \mathrel{\href{../valid/types.html#elaborate-cdtoect}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma}'
}\]
\(\href{../syntax/types.html#syntax-importdecl}{\mathit{importdecl}}\)
The extern descriptor \(\href{../syntax/types.html#syntax-importdecl}{\mathit{importdecl}}.\href{../syntax/types.html#syntax-importdecl}{\mathsf{desc}}\) must elaborate to
some \(\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\).
Then the component declarator \(\href{../syntax/types.html#syntax-importdecl}{\mathit{importdecl}}\) elaborates to the
component type with no results, the same quantifiers, and a
singleton list of imports containing
\(\{\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/types.html#syntax-importdecl}{\mathit{importdecl}}.\href{../syntax/types.html#syntax-importdecl}{\mathsf{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\}\), and
updates the context with \(\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\).
\[\begin{split}\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-importdecl}{\mathit{importdecl}}.\href{../syntax/types.html#syntax-importdecl}{\mathsf{desc}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-cdtoect}{\vdash}}{}&\href{../syntax/types.html#syntax-importdecl}{\mathit{importdecl}}\\
\mathrel{\href{../valid/types.html#elaborate-cdtoect}{\leadsto}}{}&\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \{\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/types.html#syntax-importdecl}{\mathit{importdecl}}.\href{../syntax/types.html#syntax-importdecl}{\mathsf{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\} \to \varnothing\\
\mathrel{\href{../valid/types.html#elaborate-cdtoect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}}~\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast, \href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}
\end{aligned}
}\end{split}\]
Definition types
A \(\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\) elaborates to a \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\) with the
following abstract syntax:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(edeftype)} & \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e} &::=&
\alpha\\&&|&
\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~\mathit{rtidx}\\&&|&
\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\&&|&
\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\\&&|&
\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\\&&|&
\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\\
\end{array}\end{split}\]
In general, a \(\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\) of the form \(\href{../syntax/types.html#syntax-resourcetype}{\mathit{resourcetype}}\) does
not elaborate to any \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\); however, the component
\(\href{../syntax/components.html#syntax-definition}{\mathsf{type}}\) declarator
\(\href{../valid/components.html#cdecl-rtype}{\text{generates}}\) a new
context entry for the resource in question and produces an appropriate
\(\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}\) type.
\(\href{../syntax/types.html#syntax-defvaltype}{\mathit{defvaltype}}\)
The definition value type \(\href{../syntax/types.html#syntax-defvaltype}{\mathit{defvaltype}}\) must elaborate to some
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
Then the definition type \(\href{../syntax/types.html#syntax-defvaltype}{\mathit{defvaltype}}\) elaborates to
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\vdash}} \href{../syntax/types.html#syntax-defvaltype}{\mathit{defvaltype}} \mathrel{\href{../valid/types.html#elaborate-dvttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dttoevt}{\vdash}} \href{../syntax/types.html#syntax-defvaltype}{\mathit{defvaltype}} \mathrel{\href{../valid/types.html#elaborate-dttoevt}{\leadsto}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\]
\(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)
The function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) must elaborate to some
\(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\).
Then the definition type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) elaborates to
\(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-fttoeft}{\vdash}} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\href{../valid/types.html#elaborate-fttoeft}{\leadsto}} \href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\vdash}} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\leadsto}} \href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}
}\]
\(\href{../syntax/types.html#syntax-componenttype}{\mathit{componenttype}}\)
The component type \(\href{../syntax/types.html#syntax-componenttype}{\mathit{componenttype}}\) must elaborate to some
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\).
Then the definition type \(\href{../syntax/types.html#syntax-componenttype}{\mathit{componenttype}}\) elaborates to
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-cttoect}{\vdash}} \href{../syntax/types.html#syntax-componenttype}{\mathit{componenttype}} \mathrel{\href{../valid/types.html#elaborate-cttoect}{\leadsto}} \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\vdash}} \href{../syntax/types.html#syntax-componenttype}{\mathit{componenttype}} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\leadsto}} \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
}\]
\(\href{../syntax/types.html#syntax-instancetype}{\mathit{instancetype}}\)
The instance type \(\href{../syntax/types.html#syntax-instancetype}{\mathit{instancetype}}\) must elaborate to some
\(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\).
Then the definition type \(\href{../syntax/types.html#syntax-instancetype}{\mathit{instancetype}}\) elaborates to
\(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-ittoeit}{\vdash}} \href{../syntax/types.html#syntax-instancetype}{\mathit{instancetype}} \mathrel{\href{../valid/types.html#elaborate-ittoeit}{\leadsto}} \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\vdash}} \href{../syntax/types.html#syntax-instancetype}{\mathit{instancetype}} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\leadsto}} \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}
}\]
Core instance types
Although there are no core instance types present at the surface
level, it is useful to define the abstract syntax of (elaborated) core
instance types, as they will be needed to characterise the results of
instantiationg core modules. As with a component instance type, an
(elaborated) core instance type is nothing more than a list of its
exports:
\[\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(ecoreinstancetype)} & \href{../valid/types.html#syntax-ecoreinstancetype}{\mathit{core{:}instancetype}_e} &::=&
\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}^\ast
\end{array}\]
Core module types
Core module types are defined much like component types above: as a
mapping from import descriptions to the type of the instance that will
be produced upon instantiating the module:
\[\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(ecoremoduletype)} & \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e} &::=&
\href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}^\ast \to \href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}^\ast
\end{array}\]
Notational conventions
Much like with core instance types above, we write
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e} \oplus \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}'\) to mean the
combination of two module types; in this case, the module type whose
imports are the concatenation of the import lists of
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\) and \(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}'\) and whose
instantiation result (instance) type is the result of applying
\(\oplus\) to the instantiation result (instance) types of
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\) and \(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}'\).
\(\overline{\href{../syntax/types.html#syntax-coremoduledecl}{\mathit{coremoduledecl}}_i}\)
\(\href{../syntax/types.html#syntax-coremoduledecl}{\mathit{coremoduledecl}}_1\) must elaborate to some
\({\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}}_1\) in the context
\(\{\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}~\Gamma\}\).
For each \(i > 1\), the core module declarator
\(\href{../syntax/types.html#syntax-coremoduledecl}{\mathit{coremoduledecl}}_i\) must elaborate in the context produced by
the elaboration of \(\href{../syntax/types.html#syntax-coremoduledecl}{\mathit{coremoduledecl}}_{i-1}\) to some
\({\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}}_i\).
Then the core module type \(\overline{\href{../syntax/types.html#syntax-coremoduledecl}{\mathit{coremoduledecl}}_i}\) to
\(\bigoplus_i {\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}}_i\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}_0 = \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \}\\
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_{i-1} \vdash \href{../syntax/types.html#syntax-coremoduledecl}{\mathit{coremoduledecl}}_i
\leadsto {\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}}_i \dashv \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_i
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \overline{\href{../syntax/types.html#syntax-coremoduledecl}{\mathit{coremoduledecl}}_i}
\leadsto \bigoplus_i {\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}}_i
}\end{split}\]
Core module declarators
Each core module declarator elaborates to a (partial)
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
\(\href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}\)
The core module declarator \(\href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}\) elaborates to the
core module type with no results and a singleton list of imports
containing \(\href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}\), and does not modify the context.
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}} \leadsto \href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}} \to \varnothing \dashv \href{../valid/conventions.html#syntax-tyctx}{\Gamma}
}\]
\(\href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}}\)
The core definition tyep \(\href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}}\) must elaborate to some
elaborated core definition type \(\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}\).
Then the core module declarator \(\href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}}\) elaborates to
the empty core module type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\) in
the context to the original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\)
followed by the \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}} \leadsto \href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}} \leadsto
\varnothing \to \varnothing \dashv \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}~\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e} \}
}\]
\(\href{../syntax/types.html#syntax-corealias}{\mathit{core{:}alias}}\)
The \(\href{../syntax/types.html#syntax-corealias}{\mathit{core{:}alias}}.\href{../syntax/types.html#syntax-corealias}{\mathsf{sort}}\) must be \(\href{../syntax/components.html#syntax-coresort}{\mathsf{type}}\).
The \(\href{../syntax/types.html#syntax-corealias}{\mathit{core{:}alias}}.\href{../syntax/types.html#syntax-alias}{\mathsf{target}}\) must be of the form
\(\href{../syntax/types.html#syntax-corealiastarget}{\mathsf{outer}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i\).
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\)
must be defined in the context.
Then the core module declarator \(\href{../syntax/types.html#syntax-corealias}{\mathit{core{:}alias}}\) elaborates to the
empty core module type and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\) in the
context to the original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\) followed by
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../syntax/types.html#syntax-corealias}{\mathit{core{:}alias}}.\href{../syntax/types.html#syntax-corealias}{\mathsf{sort}} = \href{../syntax/components.html#syntax-coresort}{\mathsf{type}}\\
\href{../syntax/types.html#syntax-corealias}{\mathit{core{:}alias}}.\href{../syntax/types.html#syntax-corealias}{\mathsf{target}} = \href{../syntax/types.html#syntax-corealiastarget}{\mathsf{outer}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-alias}{\mathit{alias}} \leadsto
\varnothing \to \varnothing \dashv \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i] \}
}\end{split}\]
\(\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}\)
The core module declarator \(\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}\) elaborates to the
core module type with no imports and a singleton list of exports
containing \(\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}\), and does not modify the context.
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}} \leadsto \varnothing \to \href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}} \dashv \href{../valid/conventions.html#syntax-tyctx}{\Gamma}
}\]
Core definition types
A core definition type elaborates to a \(\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}\) with the
following abstract syntax:
\[\begin{split}\begin{array}{llcl}
\def\mathdef454#1{{}}\mathdef454{(ecoredeftype)} & \href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e} &::=&
\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{functype}}\\&&|&
\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
\end{array}\end{split}\]
\(\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{functype}}\)
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{functype}} \leadsto \href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{functype}}
}\]
\(\href{../syntax/types.html#syntax-coremoduletype}{\mathit{core{:}moduletype}}\)
The core module type \(\href{../syntax/types.html#syntax-coremoduletype}{\mathit{core{:}moduletype}}\) must elaborate to some
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
Then the core definition type \(\href{../syntax/types.html#syntax-coremoduletype}{\mathit{core{:}moduletype}}\) elaborates to
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-coremoduletype}{\mathit{core{:}moduletype}} \leadsto \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-coremoduletype}{\mathit{core{:}moduletype}} \leadsto \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
}\]