Function voile::check::expr::check

fn check(tcs: TCS, expr: &Abs, expected_type: &Val) -> ValTCM

$$ \newcommand{\xx}[0]{\texttt{x}} \newcommand{\istype}[0]{\vdash_\texttt{t}} \newcommand{\Gistype}[0]{\Gamma \istype} \newcommand{\tyck}[0]{\vdash_\texttt{c}} \newcommand{\Gtyck}[0]{\Gamma \tyck} \newcommand{\infer}[0]{\vdash_\texttt{i}} \newcommand{\Ginfer}[0]{\Gamma \infer} \newcommand{\subtype}[0]{\vdash_{<:}} \newcommand{\Gsubtype}[0]{\Gamma \subtype} \newcommand{\ty}[0]{\textsf{Type}} \newcommand{\Sum}[0]{\texttt{Sum}\ } \newcommand{\merge}[0]{\texttt{merge}} \newcommand{\eval}[0]{\texttt{eval}} \newcommand{\inst}[0]{\texttt{inst}} \newcommand{\first}[0]{\texttt{first}} \newcommand{\second}[0]{\texttt{second}} \newcommand{\ctor}[0]{\texttt{Cons}\ } \newcommand{\app}[0]{\texttt{app}} \cfrac{\Gtyck a:o \Rightarrow n \quad \Gamma,n:o \tyck b:\inst(C, n) \Rightarrow m} {\Gtyck a, b : \Sigma\ C \Rightarrow n, m} \\ \space \\ \space \cfrac{\Gamma,[\xx]:o \tyck a:\app(n, [\xx])} {\Gtyck \lambda \xx.a :\Pi o. \lang n \rang \Rightarrow \lambda \lang n \rang} \\ \space \\ \space \cfrac{\Gtyck a:o \Rightarrow n \quad \Gistype c \Rightarrow m} {\Gtyck a:o+m \Rightarrow n} \\ \space \\ \space \cfrac{}{\Gtyck `\ctor:\Pi o. \lang n \rang \Rightarrow \lambda \lang n \rang} \\ \space \\ \space \cfrac{\Gistype a \Rightarrow n \quad \Gamma, [\xx]:n \istype b \Rightarrow m} {\Gtyck (\Sigma \xx:a.b):\ty \Rightarrow \Sigma n. \lang m \rang} \\ \space \\ \space \cfrac{\Gistype a \Rightarrow n \quad \Gamma, [\xx]:n \istype b \Rightarrow m} {\Gtyck (\Pi \xx:a.b):\ty \Rightarrow \Pi n. \lang m \rang} \\ \space \\ \space \cfrac{\Ginfer a \Rightarrow n \quad \Gsubtype n <: m} {\Gtyck a:m \Rightarrow \eval(a)} $$ Abstract Term -> Core Term under an expected type.

Some additional operations:

$$ \newcommand{\merge}[0]{\texttt{merge}} \begin{alignedat}{1} \merge((), S) &= S \
\merge((`L\ a, S_1), S_2) &= \merge(S_1, (`L a, S_2)) \end{alignedat} $$