Function resolve_coercion 

pub fn resolve_coercion(
    ctx: &Context,
    mctx: &mut MetaCtx,
    from: &Term,
    to: &Term,
) -> Option<Term>

Find a registered coercion carrying from to to (up to unification), returning the coercion FUNCTION to wrap the argument in — Lean’s ↑. The elaborator calls this when an argument’s type does not match the expected parameter type; a match commits the unification (a polymorphic coercion’s type variables get solved).