Function elaborate_app 

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

Elaborate an application of head (of type head_ty) where leading parameters may be implicit or instance-implicit (kinds[i]). A fresh metavariable is inserted for each implicit position; instance positions get a placeholder metavariable whose resolution is DEFERRED until all explicit arguments (which may pin the class’s type variables) have been unified. Returns the fully explicit, metavariable-instantiated term and type.