diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 8835008aa4..3c5edc1aed 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3196,6 +3196,7 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
         } else {
             new_s = visit(s, none_expr());
         }
+        synthesize(); // try to instantiate all metavars in `new_s`, otherwise reflection will fail
         expr cls = mk_app(m_ctx, get_reflected_name(), new_s);
         return mk_instance(cls, e);
     }