diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp
index 46a5f5101f..2d2d3cc0b5 100644
--- a/src/library/metavar_context.cpp
+++ b/src/library/metavar_context.cpp
@@ -98,12 +98,12 @@ struct metavar_context::interface_impl {
     metavar_context & m_ctx;
     interface_impl(metavar_context const & ctx):m_ctx(const_cast<metavar_context&>(ctx)) {}
 
-    static bool is_mvar(level const & l) { return is_metavar_decl_ref(l); }
+    static bool is_mvar_core(level const & l) { return is_metavar_decl_ref(l); }
     bool is_assigned(level const & l) const { return m_ctx.is_assigned(l); }
     optional<level> get_assignment(level const & l) const { return m_ctx.get_assignment(l); }
     void assign(level const & u, level const & v) { m_ctx.assign(u, v); }
 
-    static bool is_mvar(expr const & e) { return is_metavar_decl_ref(e); }
+    static bool is_mvar_core(expr const & e) { return is_metavar_decl_ref(e); }
     bool is_assigned(expr const & e) const { return m_ctx.is_assigned(e); }
     optional<expr> get_assignment(expr const & e) const { return m_ctx.get_assignment(e); }
     void assign(expr const & m, expr const & v) { m_ctx.assign(m, v); }
diff --git a/src/library/metavar_util.h b/src/library/metavar_util.h
index e73d963c2e..af6aea5134 100644
--- a/src/library/metavar_util.h
+++ b/src/library/metavar_util.h
@@ -14,12 +14,12 @@ Helper functions for metavariable assignments.
 The template parameter CTX must be an object that
 provides the following API:
 
-bool is_mvar(level const & l) const;
+bool is_mvar_core(level const & l) const;
 bool is_assigned(level const & l) const;
 optional<level> get_assignment(level const & l) const;
 void assign(level const & u, level const & v);
 
-bool is_mvar(expr const & e) const;
+bool is_mvar_core(expr const & e) const;
 bool is_assigned(expr const & e) const;
 optional<expr> get_assignment(expr const & e) const;
 void assign(expr const & m, expr const & v);
@@ -35,7 +35,7 @@ bool has_assigned(CTX const & ctx, level const & l) {
                 return false; // stop search
             if (found)
                 return false;  // stop search
-            if (ctx.is_mvar(l) && ctx.is_assigned(l)) {
+            if (ctx.is_mvar_core(l) && ctx.is_assigned(l)) {
                 found = true;
                 return false; // stop search
             }
@@ -63,7 +63,7 @@ bool has_assigned(CTX const & ctx, expr const & e) {
                 return false; // stop search
             if (found)
                 return false; // stop search
-            if ((ctx.is_mvar(e) && ctx.is_assigned(e)) ||
+            if ((ctx.is_mvar_core(e) && ctx.is_assigned(e)) ||
                 (is_constant(e) && has_assigned(ctx, const_levels(e))) ||
                 (is_sort(e) && has_assigned(ctx, sort_level(e)))) {
                 found = true;
@@ -83,7 +83,7 @@ level instantiate_mvars(CTX & ctx, level const & l) {
     return replace(l, [&](level const & l) {
             if (!has_meta(l)) {
                 return some_level(l);
-            } else if (ctx.is_mvar(l)) {
+            } else if (ctx.is_mvar_core(l)) {
                 if (auto v1 = ctx.get_assignment(l)) {
                     level v2 = instantiate_mvars(ctx, *v1);
                     if (*v1 != v2) {
@@ -125,7 +125,7 @@ class instantiate_mvars_fn : public replace_visitor {
     }
 
     virtual expr visit_meta(expr const & m) override {
-        if (m_ctx.is_mvar(m)) {
+        if (m_ctx.is_mvar_core(m)) {
             if (auto v1 = m_ctx.get_assignment(m)) {
                 if (!has_metavar(*v1)) {
                     return *v1;
@@ -146,7 +146,7 @@ class instantiate_mvars_fn : public replace_visitor {
     virtual expr visit_app(expr const & e) override {
         buffer<expr> args;
         expr const & f = get_app_rev_args(e, args);
-        if (m_ctx.is_mvar(f)) {
+        if (m_ctx.is_mvar_core(f)) {
             if (auto v = m_ctx.get_assignment(f)) {
                 expr new_app = apply_beta(*v, args.size(), args.data());
                 if (has_metavar(new_app))
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index a5f75c2b07..fa9ea66c2c 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1114,6 +1114,13 @@ void type_context::clear_tmp_eassignment() {
 /* -----------------------------------
    Uniform interface to temporary & regular metavariables
    ----------------------------------- */
+bool type_context::is_mvar_core(level const & l) const {
+    return (in_tmp_mode() && is_idx_metauniv(l)) || is_metavar_decl_ref(l);
+}
+
+bool type_context::is_mvar_core(expr const & e) const {
+    return (in_tmp_mode() && is_idx_metavar(e)) || is_metavar_decl_ref(e);
+}
 
 bool type_context::is_mvar(level const & l) const {
     if (in_tmp_mode())
@@ -1131,7 +1138,7 @@ bool type_context::is_mvar(expr const & e) const {
 
 bool type_context::is_assigned(level const & l) const {
     const_cast<type_context*>(this)->m_used_assignment = true;
-    if (in_tmp_mode())
+    if (in_tmp_mode() && is_idx_metauniv(l))
         return static_cast<bool>(get_tmp_assignment(l));
     else
         return m_mctx.is_assigned(l);
@@ -1139,7 +1146,7 @@ bool type_context::is_assigned(level const & l) const {
 
 bool type_context::is_assigned(expr const & e) const {
     const_cast<type_context*>(this)->m_used_assignment = true;
-    if (in_tmp_mode())
+    if (in_tmp_mode() && is_idx_metavar(e))
         return static_cast<bool>(get_tmp_assignment(e));
     else
         return m_mctx.is_assigned(e);
@@ -1147,7 +1154,7 @@ bool type_context::is_assigned(expr const & e) const {
 
 optional<level> type_context::get_assignment(level const & l) const {
     const_cast<type_context*>(this)->m_used_assignment = true;
-    if (in_tmp_mode())
+    if (in_tmp_mode() && is_idx_metauniv(l))
         return get_tmp_assignment(l);
     else
         return m_mctx.get_assignment(l);
@@ -1155,7 +1162,7 @@ optional<level> type_context::get_assignment(level const & l) const {
 
 optional<expr> type_context::get_assignment(expr const & e) const {
     const_cast<type_context*>(this)->m_used_assignment = true;
-    if (in_tmp_mode())
+    if (in_tmp_mode() && is_idx_metavar(e))
         return get_tmp_assignment(e);
     else
         return m_mctx.get_assignment(e);
@@ -1163,7 +1170,7 @@ optional<expr> type_context::get_assignment(expr const & e) const {
 
 void type_context::assign(level const & u, level const & l) {
     m_used_assignment = true;
-    if (in_tmp_mode())
+    if (in_tmp_mode() && is_idx_metauniv(u))
         assign_tmp(u, l);
     else
         m_mctx.assign(u, l);
@@ -1171,7 +1178,7 @@ void type_context::assign(level const & u, level const & l) {
 
 void type_context::assign(expr const & m, expr const & v) {
     m_used_assignment = true;
-    if (in_tmp_mode())
+    if (in_tmp_mode() && is_idx_metavar(m))
         assign_tmp(m, v);
     else
         m_mctx.assign(m, v);
@@ -1243,22 +1250,6 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part
 
     flet<unsigned> inc_depth(m_is_def_eq_depth, m_is_def_eq_depth+1);
 
-    if (in_tmp_mode()) {
-        /* TODO(Leo): we should instantiate any assigned regular metavariable
-           when we are in tmp_mode. */
-        if (is_metavar_decl_ref(l1)) {
-            /* Check if l1 is regular metavar that is already assigned */
-            if (auto v1 = m_mctx.get_assignment(l1))
-                return is_def_eq_core(*v1, l2, partial);
-        }
-
-        if (is_metavar_decl_ref(l2)) {
-            /* Check if l2 is regular metavar that is already assigned */
-            if (auto v2 = m_mctx.get_assignment(l2))
-                return is_def_eq_core(l1, *v2, partial);
-        }
-    }
-
     level new_l1 = instantiate_mvars(l1);
     level new_l2 = instantiate_mvars(l2);
 
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 1b30de9101..7a249c6e99 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -476,6 +476,8 @@ private:
        and in regular mode they access m_mctx.
        ------------ */
 public:
+    bool is_mvar_core(level const & l) const;
+    bool is_mvar_core(expr const & e) const;
     bool is_mvar(level const & l) const;
     bool is_mvar(expr const & e) const;
     bool is_assigned(level const & l) const;
diff --git a/tests/lean/run/mixed_tmp_non_tmp_universe_bug.lean b/tests/lean/run/mixed_tmp_non_tmp_universe_bug.lean
new file mode 100644
index 0000000000..d21f0ea986
--- /dev/null
+++ b/tests/lean/run/mixed_tmp_non_tmp_universe_bug.lean
@@ -0,0 +1,2 @@
+eval default (bool × unit × nat)
+eval default (bool × bool × bool × bool)