Types

A type $\tau$ is either:

• A type parameter of the form $\text{param}i$
• An alias type of the form $\tau ::T⟨\overline{\tau }⟩$
• A type constructor application of the form $T⟨\overline{\tau }⟩$
• A box type of the form $\text{Box}⟨\tau ⟩$

Corresponding Regions

If $r$ is a region in $\tau$, the corresponding region $r_c$ in a type ${\tau }_c$ is:

If $\tau =\text{\&}rm{\tau }^{\prime }$ and ${\tau }_c=\text{\&}{r}_c^{\prime }m{\tau }_c^{\prime }$ then $r_c=r_c^{\prime }$

If $\tau =T⟨{\tau }_1,\dots ,t_n⟩$ and ${\tau }_c=T⟨{\tau }_{c_1},\dots ,t_{c_n}⟩$, iterate $i$ over $1,\dots ,n$, and if there exists an $r_c^{\prime }$ where $r_c^{\prime }$ in ${\tau }_{c_i}$ is the corresponding region of $r$ in $t_i$, then $r_c=r_c^{\prime }$.