Function surface_elaborate_against 

pub fn surface_elaborate_against(
    ctx: &Context,
    term: &Term,
    expected: Option<&Term>,
) -> KernelResult<Term>

Like surface_elaborate but with an EXPECTED type (e.g. a definition’s declared type). The expected type is propagated to the top-level application/global so an implicit with no value argument — nil : {A} → List A used where a List Int is wanted — is inferred from context.