Function elaborate_app_against 

pub fn elaborate_app_against(
    ctx: &Context,
    mctx: &mut MetaCtx,
    head: &Term,
    head_ty: &Term,
    kinds: &[ParamKind],
    explicit_args: &[Term],
    expected: Option<&Term>,
) -> KernelResult<(Term, Term)>

Like elaborate_app but with an EXPECTED result type. After the explicit arguments are processed, the result type is unified with expected — so an implicit that the arguments alone do not pin (e.g. the A of nil : {A} → List A, which has no value argument) is solved from the surrounding context. The expected-type pass runs BEFORE instance resolution, so a class’s type variable can be fixed by the context too.