Function voile::check::unify::unify

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

Try to unify two well-typed terms. This may lead to meta variable resolution.