Functions

Generalized Types and Parameter Environments

A generalized type ${\tau }^{\ast }$ is either a type $\tau$ or a region $r$

A param env $E$ is a list of constraints; where a constraint takes the form:

• $r:r^{\prime }$ ($r$ outlives $r^{\prime }$)
• $\tau :r$ (All regions in $\tau$ outlive $r$)
• $\tau :\text{Tr}$ ($\tau$ implements $\text{Tr}$)

Outlives Judgments

The base outlives relation $E{⊢}_0{\tau }^{\ast }:r$ holds iff it can be derived from the following rules:

1. Direct: $({\tau }^{\ast }:r)\in E$
2. Reflexivity: $E{⊢}_{0}r:r$
3. Transitivity: $E{⊢}_0{\tau }^{\ast }:r$ and $E{⊢}_{0}r:r^{\prime }$ implies $E{⊢}_0{\tau }^{\ast }:r^{\prime }$

That is, the base outlives relation is the transitive closure of the region-outlives and type-outlives facts in $E$.

There also exists an outlives relation $E⊢{\tau }^{\ast }:r$ such that $E{⊢}_0{\tau }^{\ast }:r$ implies $E⊢{\tau }^{\ast }:r$. This relation is computed by Rust's type system and additionally accounts for outlives constraints implied by trait membership constraints in $E$.

Function Signatures

A function signature is a pair $⟨\overline{{\tau }^{\text{in}}},{\tau }^{\text{out}}⟩$.

A defined function signature $f$ is a tuple $⟨\text{defid},\overline{{\tau }^{\text{in}}},{\tau }^{\text{out}},E⟩$.

An instantiation $\hat{f}$ of $f$ is the tuple $⟨f,\overline{{\tau }^{\ast }}⟩$; where $\overline{{\tau }^{\ast }}$ is a list of early-bound parameters.

The identity instantiation $f_I$ of $f$ is obtained by applying the identity substitution $I_{{\tau }^{\ast }}$. Defined function calls are applied to instantiations of a function.

The generalized lifetime projections $GRP(\hat{f})$ of a function instantiation $\hat{f}$ is defined as the set:

$\{\text{arg}i\downarrow gr|i⩽|\overline{{\tau }^{\text{in}}}|,gr\in GR({\tau }_i^{\text{in}})|\}\cup$ $\{\text{result}\downarrow gr|gr\in GR({\tau }^{\text{out}})\}$

Function Calls

A function call target $\tilde{f}$ is either an instantiation $\hat{f}$ or a closure / function pointer $ct$.

A function call $FC$ takes the form $p=\tilde{f}(\overline{op})\text{at}l$, where $p$ is a MIR place, and $\overline{op}$ is a sequence of MIR operands.

$E(FC)$ is the parameter environment of the function with respect to the call site.

The lifetime projections $RP(FC)$ of a function call is the union of the lifetime projections in $p$ and the lifetime projections in $\overline{op}$.

A function call $FC$ is valid iff it satisfies the unique region property: each region in the lifetime projections of $FC$ is unique.