diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index ee3a739e27..9180c628f4 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -662,7 +662,7 @@ bool elaborator::is_monad_fail(expr const & e) {
           tactic ?a    ===> smt_tactic unit
 
    TODO(leo): can/should we generalize this approach? */
-optional<expr> elaborator::try_monad_coercion(expr const & e, expr const & e_type, expr type, expr const & ref) {
+optional<expr> elaborator::try_monad_coercion(expr const & e, expr e_type, expr type, expr const & ref) {
     if ((has_expr_metavar(e_type) && has_expr_metavar(type))
         || (!has_expr_metavar(e_type) && !has_expr_metavar(type))
         || !is_app(e_type)
@@ -677,6 +677,7 @@ optional<expr> elaborator::try_monad_coercion(expr const & e, expr const & e_typ
     }
     if (!m_ctx.is_def_eq(app_arg(e_type), app_arg(type)))
         return none_expr();
+    e_type = instantiate_mvars(e_type);
     type   = instantiate_mvars(type);
     return mk_coercion_core(e, e_type, type, ref);
 }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index cf0f4ede4c..eb86c79082 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -138,7 +138,7 @@ private:
     optional<expr> mk_coercion_core(expr const & e, expr const & e_type, expr const & type, expr const & ref);
     bool is_monad(expr const & e);
     bool is_monad_fail(expr const & e);
-    optional<expr> try_monad_coercion(expr const & e, expr const & e_type, expr type, expr const & ref);
+    optional<expr> try_monad_coercion(expr const & e, expr e_type, expr type, expr const & ref);
     optional<expr> mk_coercion(expr const & e, expr e_type, expr type, expr const & ref);
 
     void trace_coercion_fn_sort_failure(bool is_fn, expr const & e_type, expr const & ref, char const * error_msg);