Type-preserving compilation of polymorphic records

A record kind $\{\{{\ell }_i:{\tau }_i\}{\}}_{i=1}^m$ requires the listed distinct fields but does not fix the complete layout. Rule K-Rec checks both complete-record formation and finite-map inclusion:

$\mathcal{K}⊢\{{\ell }_j^{\prime }:{\upsilon }_j{\}}_{j=1}^n::\mathsf{U}$$\{{\ell }_i:{\tau }_i{\}}_{i=1}^m\subseteq \{{\ell }_j^{\prime }:{\upsilon }_j{\}}_{j=1}^n$

$\mathcal{K}⊢\{{\ell }_j^{\prime }:{\upsilon }_j{\}}_{j=1}^n::\{\{{\ell }_i:{\tau }_i\}{\}}_{i=1}^m$

The source record and projection rules are

$\mathcal{K};\mathcal{T}{⊢}_{\mathsf{R}}{M}_i:{\tau }_i(1\le i\le n)$${\ell }_1,\dots ,{\ell }_n\text{ are distinct}$

$\mathcal{K};\mathcal{T}{⊢}_{\mathsf{R}}\{{\ell }_i=M_i{\}}_{i=1}^n:\{{\ell }_i:{\tau }_i{\}}_{i=1}^n$

$\mathcal{K};\mathcal{T}{⊢}_{\mathsf{R}}M:\tau$$\mathcal{K}⊢\tau ::\{\{\ell :\upsilon \}\}$

$\mathcal{K};\mathcal{T}{⊢}_{\mathsf{R}}M.\ell :\upsilon$

The variable $I_{t,\ell }$ belongs only to the pair $(t,\ell )$. For a ground kind-respecting substitution $S$, the distinct numeral substitution is $${\nu }_S(I_{t,\ell })={\mathrm{pos}}_{\ell }(S(t)).$$ The target rules distinguish vector selection $C⟨J⟩$ from type application $C[\tau ]$:

$\mathcal{K};\mathcal{L};\mathcal{T}{⊢}_{\mathsf{V}}C:\tau$$\mathcal{K}⊢\tau ::\{\{\ell :\upsilon \}\}$$\mathcal{K};\mathcal{L}⊢J:\mathsf{idx}(\ell ,\tau )$

$\mathcal{K};\mathcal{L};\mathcal{T}{⊢}_{\mathsf{V}}C⟨J⟩:\upsilon$

$\mathcal{K};\mathcal{L},I:\mathsf{idx}(\ell ,\tau );\mathcal{T}{⊢}_{\mathsf{V}}C:\upsilon$

$\mathcal{K};\mathcal{L};\mathcal{T}{⊢}_{\mathsf{V}}{\lambda }^{\mathsf{i}}I.C:\mathsf{idx}(\ell ,\tau ){\Rightarrow }_{\mathsf{i}}\upsilon$

$\mathcal{K};\mathcal{L};\mathcal{T}{⊢}_{\mathsf{V}}C:\mathsf{idx}(\ell ,\tau ){\Rightarrow }_{\mathsf{i}}\upsilon$$\mathcal{K};\mathcal{L}⊢J:\mathsf{idx}(\ell ,\tau )$

$\mathcal{K};\mathcal{L};\mathcal{T}{⊢}_{\mathsf{V}}C@J:\upsilon$

The contextual judgment $\mathcal{K};\mathcal{L};\mathcal{T}⊢M{⇝}_{\mathsf{rec}}C:\sigma$ uses C-Record to compile records to vectors in increasing label order and C-Dot to compile projection as $M.\ell {⇝}_{\mathsf{rec}}C⟨J⟩$. Rule C-TAbsRec inserts ${\lambda }^{\mathsf{i}}{I}_{t,{\ell }_1}\cdots {\lambda }^{\mathsf{i}}{I}_{t,{\ell }_m}$ in canonical label order; C-TAppRec supplies the certified positions. Source call-by-value has term beta, type beta, and record projection. Target call-by-value has term beta, type beta, and the two additional roots $$[A_1,\dots ,A_n]⟨i⟩{⇝}_0{A}_i,({\lambda }^{\mathsf{i}}I.C)@i{⇝}_{0}C[i/I].$$