Function voile::check::unify::unify

fn unify(tcs: TCS, a: &Val, b: &Val) -> TCM

Try to unify two well-typed terms, using a conversion check algorithm. This may lead to meta variable resolution. $$ \newcommand{\Gvdash}[0]{\Gamma \vdash} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \newcommand{\recordext}[2]{\record{#1 \mid #2}} \newcommand{\clabVal}[0]{\delta} \newcommand{\recExt}[1]{\mid #1} \newcommand{\variantext}[2]{\variant{#1 \mid #2}} \cfrac{ \Gvdash \cA_0 \simeq \cA_1 \quad \Gvdash \cA_1 \simeq \cA_2 }{ \Gvdash \cA_0 \simeq \cA_2 } \quad \cfrac{}{\Gvdash \cA \simeq \cA} \\ \space \\ \cfrac{}{ \Gvdash \{\} \simeq \{\} } \quad \cfrac{\Gvdash \alpha \simeq \beta}{ \Gvdash n\ \alpha \simeq n\ \beta \quad \cfrac{\Gvdash \{ \clabVal_0 \} \simeq \{ \clabVal_1 \}}{ \Gvdash \{ n\ = \alpha, \clabVal_0 \} \simeq \{ n\ = \beta, \clabVal_1 \} } } $$