diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index ad01f0077a..99dcc24fe2 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -26,7 +26,6 @@ pair<expr, constraint_seq> converter::infer_type(type_checker & tc, expr const &
 
 extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
 
-
 /** \brief Do nothing converter */
 struct dummy_converter : public converter {
     virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker &) {
@@ -37,7 +36,7 @@ struct dummy_converter : public converter {
     }
     virtual bool is_opaque(declaration const &) const { return false; }
     virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
-    virtual bool is_stuck(expr const &, type_checker &) { return false; }
+    virtual optional<expr> is_stuck(expr const &, type_checker &) { return none_expr(); }
 };
 
 std::unique_ptr<converter> mk_dummy_converter() {
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index 7c9338b113..b2be4d4d5b 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -21,7 +21,7 @@ public:
     virtual bool is_opaque(declaration const & d) const = 0;
     virtual optional<declaration> is_delta(expr const & e) const = 0;
 
-    virtual bool is_stuck(expr const & e, type_checker & c) = 0;
+    virtual optional<expr> is_stuck(expr const & e, type_checker & c) = 0;
     virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker & c) = 0;
     virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
 
diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
index bd565055c1..dc96057350 100644
--- a/src/kernel/default_converter.cpp
+++ b/src/kernel/default_converter.cpp
@@ -50,8 +50,12 @@ bool default_converter::is_stuck(expr const & e) {
     return static_cast<bool>(m_env.norm_ext().is_stuck(e, get_extension(*m_tc)));
 }
 
-bool default_converter::is_stuck(expr const & e, type_checker & c) {
-    return static_cast<bool>(m_env.norm_ext().is_stuck(e, get_extension(c)));
+optional<expr> default_converter::is_stuck(expr const & e, type_checker & c) {
+    if (is_meta(e)) {
+        return some_expr(e);
+    } else {
+        return m_env.norm_ext().is_stuck(e, get_extension(c));
+    }
 }
 
 /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h
index ea2304f689..3b6508b392 100644
--- a/src/kernel/default_converter.h
+++ b/src/kernel/default_converter.h
@@ -90,7 +90,7 @@ public:
     virtual optional<declaration> is_delta(expr const & e) const;
     virtual bool is_opaque(declaration const & d) const;
 
-    virtual bool is_stuck(expr const & e, type_checker & c);
+    virtual optional<expr> is_stuck(expr const & e, type_checker & c);
     virtual pair<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c);
     virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst);
 };
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index af916a8ff6..8d6c2d98d4 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -436,11 +436,7 @@ type_checker::type_checker(environment const & env):
 type_checker::~type_checker() {}
 
 optional<expr> type_checker::is_stuck(expr const & e) {
-    if (is_meta(e)) {
-        return some_expr(e);
-    } else {
-        return m_env.norm_ext().is_stuck(e, m_tc_ctx);
-    }
+    return m_conv->is_stuck(e, *this);
 }
 
 void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index a8c09bb788..fd3dd416cd 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -224,7 +224,7 @@ public:
 
     optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
 
-    bool may_reduce_later(expr const & e) { return m_conv->is_stuck(e, *this); }
+    bool may_reduce_later(expr const & e) { return !is_meta(e) && static_cast<bool>(m_conv->is_stuck(e, *this)); }
 
     template<typename F>
     typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {