diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 6361b04201..e33e88c435 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3846,26 +3846,9 @@ struct sanitize_param_names_fn : public replace_visitor {
 
 /** When the output of the elaborator may contain meta-variables, we convert the type_context_old level meta-variables
     into regular kernel meta-variables. */
-static expr replace_with_simple_metavars(metavar_context mctx, name_map<expr> & cache, expr const & e) {
-    if (!has_expr_metavar(e)) return e;
-    return replace(e, [&](expr const & e, unsigned) {
-            if (is_metavar(e)) {
-                if (auto r = cache.find(mvar_name(e))) {
-                    return some_expr(*r);
-                } else if (auto decl = mctx.find_metavar_decl(e)) {
-                    expr new_type = replace_with_simple_metavars(mctx, cache, mctx.instantiate_mvars(decl->get_type()));
-                    expr new_mvar = mk_metavar(mvar_name(e), new_type);
-                    cache.insert(mvar_name(e), new_mvar);
-                    return some_expr(new_mvar);
-                } else if (is_metavar_decl_ref(e)) {
-                    throw exception("unexpected occurrence of internal elaboration metavariable");
-                } else {
-                    return none_expr();
-                }
-            } else {
-                return none_expr();
-            }
-        });
+static expr replace_with_simple_metavars(metavar_context /* mctx */, name_map<expr> & /* cache */, expr const & e) {
+    // Disabled this code
+    return e;
 }
 
 expr elaborator::elaborate(expr const & e) {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 3df425a786..a1ef4721bb 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -395,7 +395,6 @@ static void check_no_metavars(name const & n, expr const & e) {
                 format r("failed to add declaration '");
                 r += format(n);
                 r += format("' to local context, type has metavariables");
-                r += pp_until_meta_visible(fmt, mvar_type(e));
                 return r;
             });
     }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index a47bbc2113..271cfc817b 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -268,9 +268,9 @@ expr pretty_fn::purify(expr const & e) {
             if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e))) {
                 return some_expr(e);
             } else if (m_purify_metavars && is_metavar_decl_ref(e)) {
-                return some_expr(mk_metavar(mk_metavar_name(mvar_name(e), "m"), infer_type(e)));
+                return some_expr(mk_metavar(mk_metavar_name(mvar_name(e), "m")));
             } else if (m_purify_metavars && is_metavar(e) && !is_idx_metavar(e)) {
-                return some_expr(mk_metavar(mk_metavar_name(mvar_name(e)), infer_type(e)));
+                return some_expr(mk_metavar(mk_metavar_name(mvar_name(e))));
             } else if (is_local(e)) {
                 return some_expr(mk_local(local_name(e), mk_local_name(local_name(e), local_pp_name(e)),
                                           infer_type(e), local_info(e)));
diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp
index 95843f3c7e..6ebaaa04ad 100644
--- a/src/kernel/equiv_manager.cpp
+++ b/src/kernel/equiv_manager.cpp
@@ -75,9 +75,7 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
             compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
         break;
     case expr_kind::MVar:
-        result =
-            mvar_name(a) == mvar_name(b) &&
-            is_equiv_core(mvar_type(a), mvar_type(b));
+        result = mvar_name(a) == mvar_name(b);
         break;
     case expr_kind::FVar:
         result =
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 95d9bcd913..1ec12946c6 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -105,7 +105,7 @@ inline constexpr unsigned num_obj_fields(expr_kind k) {
         k == expr_kind::Pi      ?  3 :
         k == expr_kind::BVar    ?  1 :
         k == expr_kind::Let     ?  4 :
-        k == expr_kind::MVar    ?  2 :
+        k == expr_kind::MVar    ?  1 :
         k == expr_kind::Sort    ?  1 :
         k == expr_kind::Lit     ?  1 :
         k == expr_kind::MData   ?  2 :
@@ -451,22 +451,21 @@ expr mk_let(name const & n, expr const & t, expr const & v, expr const & b) {
     return expr(lean_expr_mk_let(n.raw(), t.raw(), v.raw(), b.raw()));
 }
 
-extern "C" object * lean_expr_mk_mvar_core(object * n, object * t) {
-    object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::MVar), 2, rec_expr_scalar_size(expr_kind::MVar));
+extern "C" object * lean_expr_mk_mvar_core(object * n) {
+    object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::MVar), 1, rec_expr_scalar_size(expr_kind::MVar));
     cnstr_set(r, 0, n);
-    cnstr_set(r, 1, t);
-    set_scalar<expr_kind::MVar>(r, name::hash(n), true, has_univ_mvar(t), has_fvar(t), has_univ_param(t));
-    set_rec_scalar<expr_kind::MVar>(r, expr_get_loose_bvar_range(t));
+    set_scalar<expr_kind::MVar>(r, name::hash(n), true, false, false, false);
+    set_rec_scalar<expr_kind::MVar>(r, 0);
     return r;
 }
 
 extern "C" object * lean_expr_mk_mvar(object * n) {
-    return lean_expr_mk_mvar_core(n, get_dummy().to_obj_arg());
+    return lean_expr_mk_mvar_core(n);
 }
 
-expr mk_mvar(name const & n, expr const & t) {
-    inc(n.raw()); inc(t.raw());
-    return expr(lean_expr_mk_mvar_core(n.raw(), t.raw()));
+expr mk_mvar(name const & n) {
+    inc(n.raw());
+    return expr(lean_expr_mk_mvar_core(n.raw()));
 }
 
 static expr * g_Prop  = nullptr;
@@ -649,13 +648,6 @@ expr update_const(expr const & e, levels const & new_levels) {
         return e;
 }
 
-expr update_mvar(expr const & e, expr const & new_type) {
-    if (is_eqp(mvar_type(e), new_type))
-        return e;
-    else
-        return mk_mvar(mvar_name(e), new_type);
-}
-
 expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body) {
     if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_value) || !is_eqp(let_body(e), new_body))
         return mk_let(let_name(e), new_type, new_value, new_body);
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 786c75a4a4..d2c08bdc35 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -77,7 +77,7 @@ inline deserializer & operator>>(deserializer & d, literal & l) { l = read_liter
 inductive expr
 | bvar  : nat → expr          -- bound variables
 | fvar  : name → expr         -- free variables
-| mvar  : name → expr → expr  -- meta variables
+| mvar  : name → expr         -- meta variables
 | sort  : level → expr
 | const : name → list level → expr
 | app   : expr → expr → expr
@@ -96,7 +96,7 @@ class expr : public object_ref {
     friend expr mk_mdata(kvmap const & d, expr const & e);
     friend expr mk_proj(name const & s, nat const & idx, expr const & e);
     friend expr mk_bvar(nat const & idx);
-    friend expr mk_mvar(name const & n, expr const & t);
+    friend expr mk_mvar(name const & n);
     friend expr mk_const(name const & n, levels const & ls);
     friend expr mk_app(expr const & f, expr const & a);
     friend expr mk_sort(level const & l);
@@ -190,7 +190,7 @@ inline expr mk_bvar(unsigned idx) { return mk_bvar(nat(idx)); }
 expr mk_fvar(name const & n);
 expr mk_const(name const & n, levels const & ls);
 inline expr mk_const(name const & n) { return mk_const(n, levels()); }
-expr mk_mvar(name const & n, expr const & t);
+expr mk_mvar(name const & n);
 expr mk_app(expr const & f, expr const & a);
 expr mk_app(expr const & f, unsigned num_args, expr const * args);
 expr mk_app(unsigned num_args, expr const * args);
@@ -234,7 +234,6 @@ inline name const &    fvar_name_core(object * o)            { lean_assert(is_fv
 inline name const &    fvar_name(expr const & e)             { lean_assert(is_fvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
 inline level const &   sort_level(expr const & e)            { lean_assert(is_sort(e)); return static_cast<level const &>(cnstr_get_ref(e, 0)); }
 inline name const &    mvar_name(expr const & e)             { lean_assert(is_mvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
-inline expr const &    mvar_type(expr const & e)             { lean_assert(is_mvar(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
 inline name const &    const_name(expr const & e)            { lean_assert(is_const(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
 inline levels const &  const_levels(expr const & e)          { lean_assert(is_const(e)); return static_cast<levels const &>(cnstr_get_ref(e, 1)); }
 inline bool is_const(expr const & e, name const & n)         { return is_const(e) && const_name(e) == n; }
@@ -261,7 +260,6 @@ expr update_const(expr const & e, levels const & new_levels);
 expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body);
 expr update_mdata(expr const & e, expr const & new_e);
 expr update_proj(expr const & e, expr const & new_e);
-expr update_mvar(expr const & e, expr const & new_type);
 // =======================================
 
 
@@ -342,7 +340,7 @@ inline bool is_var(expr const & e) { return is_bvar(e); }
 inline bool is_var(expr const & e, unsigned idx) { return is_bvar(e, idx); }
 inline bool is_metavar(expr const & e) { return is_mvar(e); }
 inline bool is_metavar_app(expr const & e) { return is_mvar_app(e); }
-inline expr mk_metavar(name const & n, expr const & t) { return mk_mvar(n, t); }
+inline expr mk_metavar(name const & n) { return mk_mvar(n); }
 expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi);
 inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, mk_binder_info()); }
 inline expr mk_local(name const & n, expr const & t, binder_info bi) { return mk_local(n, n, t, bi); }
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index a2b253bd66..ec9a62ed38 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -88,9 +88,7 @@ class expr_eq_fn {
                 const_name(a) == const_name(b) &&
                 compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
         case expr_kind::MVar:
-            return
-                mvar_name(a) == mvar_name(b) &&
-                apply(mvar_type(a), mvar_type(b));
+            return mvar_name(a) == mvar_name(b);
         case expr_kind::FVar:
             return
                 local_name(a) == local_name(b) &&
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index d5adddf575..08487d6403 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -87,6 +87,7 @@ class for_each_fn {
             switch (e.kind()) {
             case expr_kind::Const: case expr_kind::BVar:
             case expr_kind::Sort:  case expr_kind::Lit:
+            case expr_kind::MVar:
                 goto begin_loop;
             case expr_kind::MData:
                 todo.emplace_back(mdata_expr(e), offset);
@@ -98,9 +99,6 @@ class for_each_fn {
                 // TODO(Leo): delete after refactoring
                 todo.emplace_back(local_type(e), offset);
                 goto begin_loop;
-            case expr_kind::MVar:
-                todo.emplace_back(mvar_type(e), offset);
-                goto begin_loop;
             case expr_kind::App:
                 todo.emplace_back(app_arg(e), offset);
                 todo.emplace_back(app_fn(e), offset);
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index 4432d0d0d9..6b6834ca0b 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -81,6 +81,7 @@ class replace_rec_fn {
             switch (e.kind()) {
             case expr_kind::Const: case expr_kind::Sort:
             case expr_kind::BVar:  case expr_kind::Lit:
+            case expr_kind::MVar:
                 return save_result(e, offset, e, shared);
             case expr_kind::MData: {
                 expr new_e = apply(mdata_expr(e), offset);
@@ -90,10 +91,6 @@ class replace_rec_fn {
                 expr new_e = apply(proj_expr(e), offset);
                 return save_result(e, offset, update_proj(e, new_e), shared);
             }
-            case expr_kind::MVar: {
-                expr new_t = apply(mvar_type(e), offset);
-                return save_result(e, offset, update_mvar(e, new_t), shared);
-            }
             case expr_kind::FVar: {
                 expr new_t = apply(local_type(e), offset); // TODO(Leo): delete after refactoring
                 return save_result(e, offset, update_local(e, new_t), shared);
diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index d2ee05c04d..bfb4da4e48 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -175,27 +175,21 @@ class app_builder {
     optional<entry> get_entry(name const & c, unsigned nargs) {
         key k(c, nargs);
         lean_assert(k.check_invariant());
-        auto it = m_cache.m_map.find(k);
-        if (it == m_cache.m_map.end()) {
-            if (optional<constant_info> info = env().find(c)) {
-                buffer<expr> mvars;
-                buffer<optional<expr>> inst_args;
-                levels lvls = mk_metavars(*info, mvars, inst_args);
-                if (nargs > mvars.size())
-                    return optional<entry>(); // insufficient number of arguments
-                entry e;
-                e.m_num_umeta = info->get_num_lparams();
-                e.m_num_emeta = mvars.size();
-                e.m_app       = ::lean::mk_app(mk_constant(c, lvls), mvars);
-                e.m_inst_args = reverse_to_list(inst_args.begin(), inst_args.end());
-                e.m_expl_args = reverse_to_list(mvars.begin() + mvars.size() - nargs, mvars.end());
-                m_cache.m_map.insert(mk_pair(k, e));
-                return optional<entry>(e);
-            } else {
-                return optional<entry>(); // unknown decl
-            }
+        if (optional<constant_info> info = env().find(c)) {
+            buffer<expr> mvars;
+            buffer<optional<expr>> inst_args;
+            levels lvls = mk_metavars(*info, mvars, inst_args);
+            if (nargs > mvars.size())
+                return optional<entry>(); // insufficient number of arguments
+            entry e;
+            e.m_num_umeta = info->get_num_lparams();
+            e.m_num_emeta = mvars.size();
+            e.m_app       = ::lean::mk_app(mk_constant(c, lvls), mvars);
+            e.m_inst_args = reverse_to_list(inst_args.begin(), inst_args.end());
+            e.m_expl_args = reverse_to_list(mvars.begin() + mvars.size() - nargs, mvars.end());
+            return optional<entry>(e);
         } else {
-            return optional<entry>(it->second);
+            return optional<entry>(); // unknown decl
         }
     }
 
@@ -227,30 +221,24 @@ class app_builder {
     optional<entry> get_entry(name const & c, unsigned mask_sz, bool const * mask) {
         key k(c, to_list(mask, mask+mask_sz));
         lean_assert(k.check_invariant());
-        auto it = m_cache.m_map.find(k);
-        if (it == m_cache.m_map.end()) {
-            if (auto d = env().find(c)) {
-                buffer<expr> mvars;
-                buffer<optional<expr>> inst_args;
-                levels lvls = mk_metavars(*d, mask_sz, mvars, inst_args);
-                entry e;
-                e.m_num_umeta = d->get_num_lparams();
-                e.m_num_emeta = mvars.size();
-                e.m_app       = ::lean::mk_app(mk_constant(c, lvls), mvars);
-                e.m_inst_args = reverse_to_list(inst_args.begin(), inst_args.end());
-                list<expr> expl_args;
-                for (unsigned i = 0; i < mask_sz; i++) {
-                    if (mask[i])
-                        expl_args = cons(mvars[i], expl_args);
-                }
-                e.m_expl_args = expl_args;
-                m_cache.m_map.insert(mk_pair(k, e));
-                return optional<entry>(e);
-            } else {
-                return optional<entry>(); // unknown decl
+        if (auto d = env().find(c)) {
+            buffer<expr> mvars;
+            buffer<optional<expr>> inst_args;
+            levels lvls = mk_metavars(*d, mask_sz, mvars, inst_args);
+            entry e;
+            e.m_num_umeta = d->get_num_lparams();
+            e.m_num_emeta = mvars.size();
+            e.m_app       = ::lean::mk_app(mk_constant(c, lvls), mvars);
+            e.m_inst_args = reverse_to_list(inst_args.begin(), inst_args.end());
+            list<expr> expl_args;
+            for (unsigned i = 0; i < mask_sz; i++) {
+                if (mask[i])
+                    expl_args = cons(mvars[i], expl_args);
             }
+            e.m_expl_args = expl_args;
+            return optional<entry>(e);
         } else {
-            return optional<entry>(it->second);
+            return optional<entry>(); // unknown decl
         }
     }
 
@@ -265,7 +253,7 @@ class app_builder {
             --i;
             if (!m_ctx.get_tmp_mvar_assignment(i)) {
                 if (inst_arg) {
-                    expr type = m_ctx.instantiate_mvars(mvar_type(*inst_arg));
+                    expr type = m_ctx.instantiate_mvars(m_ctx.get_tmp_mvar_type(*inst_arg));
                     if (auto v = m_ctx.mk_class_instance(type)) {
                         if (!m_ctx.is_def_eq(*inst_arg, *v)) {
                             // failed to assign instance
@@ -288,10 +276,6 @@ class app_builder {
         return true;
     }
 
-    void init_ctx_for(entry const & e) {
-        m_ctx.ensure_num_tmp_mvars(e.m_num_umeta, e.m_num_emeta);
-    }
-
     void trace_unify_failure(name const & n, unsigned i, expr const & m, expr const & v) {
         lean_app_builder_trace(
             trace_fun(n);
@@ -319,7 +303,6 @@ public:
             trace_failure(c, "failed to retrieve declaration");
             throw app_builder_exception();
         }
-        init_ctx_for(*e);
         unsigned i = nargs;
         for (auto m : e->m_expl_args) {
             if (i == 0) {
@@ -363,7 +346,6 @@ public:
             trace_failure(c, "failed to retrieve declaration");
             throw app_builder_exception();
         }
-        init_ctx_for(*e);
         unsigned i    = mask_sz;
         unsigned j    = nargs;
         list<expr> it = e->m_expl_args;
diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp
index bc12bbd6f9..0c22cc01ef 100644
--- a/src/library/deep_copy.cpp
+++ b/src/library/deep_copy.cpp
@@ -21,7 +21,7 @@ expr copy(expr const & a) {
     case expr_kind::App:    return mk_app(app_fn(a), app_arg(a));
     case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
     case expr_kind::Pi:     return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
-    case expr_kind::MVar:   return mk_mvar(mvar_name(a), mvar_type(a));
+    case expr_kind::MVar:   return mk_mvar(mvar_name(a));
     case expr_kind::Let:    return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index 2332b714a6..b1716a20ce 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -65,10 +65,7 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
         }
         /* fall-thru */
     case expr_kind::MVar:
-        if (mvar_name(a) != mvar_name(b))
-            return mvar_name(a) < mvar_name(b);
-        else
-            return is_lt(mvar_type(a), mvar_type(b), use_hash, lctx);
+        return mvar_name(a) < mvar_name(b);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -178,10 +175,7 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
         else
             return is_lt_no_level_params(local_type(a), local_type(b));
     case expr_kind::MVar:
-        if (mvar_name(a) != mvar_name(b))
-            return mvar_name(a) < mvar_name(b);
-        else
-            return is_lt_no_level_params(mvar_type(a), mvar_type(b));
+        return mvar_name(a) < mvar_name(b);
     }
     lean_unreachable();
 }
diff --git a/src/library/idx_metavar.cpp b/src/library/idx_metavar.cpp
index b23afcf852..f2f971bdff 100644
--- a/src/library/idx_metavar.cpp
+++ b/src/library/idx_metavar.cpp
@@ -29,8 +29,8 @@ level mk_idx_metauniv(unsigned i) {
     return mk_univ_mvar(name(*g_tmp_prefix, i));
 }
 
-expr mk_idx_metavar(unsigned i, expr const & type) {
-    return mk_metavar(name(*g_tmp_prefix, i), type);
+expr mk_idx_metavar(unsigned i) {
+    return mk_metavar(name(*g_tmp_prefix, i));
 }
 
 bool is_idx_metauniv(level const & l) {
@@ -100,66 +100,4 @@ bool has_idx_expr_metavar(expr const & e) {
         });
     return found;
 }
-
-struct to_idx_metavars_fn : public replace_visitor {
-    metavar_context const & m_mctx;
-    buffer<level> &         m_new_us;
-    buffer<expr> &          m_new_ms;
-    name_map<level>         m_lvl_cache;
-
-    to_idx_metavars_fn(metavar_context const & mctx, buffer<level> & new_us, buffer<expr> & new_ms):
-        m_mctx(mctx), m_new_us(new_us), m_new_ms(new_ms) {}
-
-    level visit(level const & l) {
-        if (!has_mvar(l)) return l;
-        return replace(l, [&](level const & l) {
-                if (is_mvar(l) && !is_idx_metauniv(l)) {
-                    if (auto it = m_lvl_cache.find(mvar_id(l)))
-                        return some_level(*it);
-                    level new_l = mk_idx_metauniv(m_new_us.size());
-                    m_lvl_cache.insert(mvar_id(l), new_l);
-                    m_new_us.push_back(new_l);
-                    return some_level(new_l);
-                }
-                return none_level();
-            });
-    }
-
-    levels visit(levels const & ls) {
-        return map_reuse(ls, [&](level const & l) { return visit(l); });
-    }
-
-    virtual expr visit_meta(expr const & m) override {
-        if (is_idx_metavar(m)) {
-            return m;
-        } else if (auto decl = m_mctx.find_metavar_decl(m)) {
-            expr new_type = visit(decl->get_type());
-            unsigned i    = m_new_ms.size();
-            expr new_m    = mk_idx_metavar(i, new_type);
-            m_new_ms.push_back(new_m);
-            return new_m;
-        } else {
-            throw exception("unexpected occurrence of metavariable");
-        }
-    }
-
-    virtual expr visit_constant(expr const & e) override {
-        return update_constant(e, visit(const_levels(e)));
-    }
-
-    virtual expr visit_sort(expr const & e) override {
-        return update_sort(e, visit(sort_level(e)));
-    }
-
-    virtual expr visit(expr const & e) override {
-        if (!has_metavar(e)) return e;
-        return replace_visitor::visit(e);
-    }
-};
-
-expr to_idx_metavars(metavar_context const & mctx, expr const & e, buffer<level> & new_us, buffer<expr> & new_ms) {
-    if (!has_metavar(e))
-        return e;
-    return to_idx_metavars_fn(mctx, new_us, new_ms)(e);
-}
 }
diff --git a/src/library/idx_metavar.h b/src/library/idx_metavar.h
index bafbee040e..584d8dd27b 100644
--- a/src/library/idx_metavar.h
+++ b/src/library/idx_metavar.h
@@ -22,7 +22,7 @@ unsigned to_meta_idx(level const & l);
     \remark The index \c i is encoded in the hierarchical name, and can be quickly accessed.
     In the match procedure the substitution is also efficiently represented as an array (aka buffer).
 */
-expr mk_idx_metavar(unsigned i, expr const & type);
+expr mk_idx_metavar(unsigned i);
 /** \brief Return true iff \c l is a metavariable created using \c mk_idx_metavar */
 bool is_idx_metavar(expr const & l);
 unsigned to_meta_idx(expr const & e);
@@ -34,10 +34,6 @@ bool has_idx_metauniv(level const & l);
 
 class metavar_context;
 
-/** \brief Convert metavariables occurring in \c e into indexed/temporary metavariables.
-    New metavariables are added to new_us and new_ms. */
-expr to_idx_metavars(metavar_context const & mctx, expr const & e, buffer<level> & new_us, buffer<expr> & new_ms);
-
 void initialize_idx_metavar();
 void finalize_idx_metavar();
 }
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index 5e40034456..909fdd0de4 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -75,6 +75,7 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
         switch (e.kind()) {
         case expr_kind::BVar: case expr_kind::Const:
         case expr_kind::Sort: case expr_kind::Lit:
+        case expr_kind::MVar:
             break; // do nothing
         case expr_kind::MData:
             visit(mdata_expr(e));
@@ -87,10 +88,6 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
                 visit(local_type(e));
             ls.insert(e);
             break;
-        case expr_kind::MVar:
-            lean_assert(!restricted);
-            visit(mvar_type(e));
-            break;
         case expr_kind::App:
             visit(app_fn(e));
             visit(app_arg(e));
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 3d0ed74b93..f595c31070 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -53,7 +53,7 @@ struct max_sharing_fn::imp {
             return *r;
         expr res;
         switch (a.kind()) {
-        case expr_kind::BVar: case expr_kind::Lit:
+        case expr_kind::BVar: case expr_kind::Lit: case expr_kind::MVar:
             res = a;
             break;
         case expr_kind::Const:
@@ -91,9 +91,6 @@ struct max_sharing_fn::imp {
             res = update_let(a, new_t, new_v, new_b);
             break;
         }
-        case expr_kind::MVar:
-            res = update_mvar(a, apply(mvar_type(a)));
-            break;
         case expr_kind::FVar:
             res = update_local(a, apply(local_type(a)));
             break;
diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp
index 860ae0f225..92688c72da 100644
--- a/src/library/metavar_context.cpp
+++ b/src/library/metavar_context.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "library/metavar_util.h"
 #include "library/metavar_context.h"
+#include "library/idx_metavar.h"
 
 namespace lean {
 static name *       g_meta_prefix;
@@ -24,7 +25,7 @@ metavar_decl::metavar_decl():
     metavar_decl(name(), local_context(), expr()) {}
 
 static expr mk_meta_ref(name const & n) {
-    return mk_metavar(n, *g_dummy_type);
+    return mk_metavar(n);
 }
 
 bool is_metavar_decl_ref(level const & u) {
@@ -32,7 +33,7 @@ bool is_metavar_decl_ref(level const & u) {
 }
 
 bool is_metavar_decl_ref(expr const & e) {
-    return is_mvar(e) && mvar_type(e) == *g_dummy_type;
+    return is_mvar(e) && !is_idx_metavar(e);
 }
 
 name get_metavar_decl_ref_suffix(level const & u) {
diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp
index 72f7e96018..aac64223bc 100644
--- a/src/library/placeholder.cpp
+++ b/src/library/placeholder.cpp
@@ -23,7 +23,7 @@ void finalize_placeholder() {
 level mk_level_placeholder() { return mk_univ_mvar(name()); }
 
 expr mk_expr_placeholder() {
-    return mk_mvar(name(), mk_Prop());
+    return mk_mvar(name());
 }
 static bool is_placeholder(name const & n) {
     return n.is_anonymous();
diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp
index 00e9e3e372..997e317fd4 100644
--- a/src/library/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -17,10 +17,7 @@ expr replace_visitor::visit_sort(expr const & e) { lean_assert(is_sort(e)); retu
 expr replace_visitor::visit_var(expr const & e) { lean_assert(is_var(e)); return e; }
 expr replace_visitor::visit_lit(expr const & e) { lean_assert(is_lit(e)); return e; }
 expr replace_visitor::visit_constant(expr const & e) { lean_assert(is_constant(e)); return e; }
-expr replace_visitor::visit_meta(expr const & e) {
-    lean_assert(is_mvar(e));
-    return update_mvar(e, visit(mvar_type(e)));
-}
+expr replace_visitor::visit_meta(expr const & e) { lean_assert(is_mvar(e)); return e; }
 expr replace_visitor::visit_local(expr const & e) {
     lean_assert(is_local(e));
     return update_local(e, visit(local_type(e)));
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index e02600368e..2a41ac43fd 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1061,7 +1061,7 @@ expr type_context_old::infer_metavar(expr const & e) {
         /* tmp metavariables should only occur in tmp_mode.
            The following assertion was commented because the pretty printer may violate it. */
         // lean_assert(!is_idx_metavar(e) || in_tmp_mode());
-        return mvar_type(e);
+        return get_tmp_mvar_type(e);
     }
 }
 
@@ -1223,14 +1223,6 @@ bool type_context_old::is_proof(expr const & e) {
 /* -------------------------------
    Temporary assignment mode support
    ------------------------------- */
-void type_context_old::ensure_num_tmp_mvars(unsigned num_uvars, unsigned num_mvars) {
-    lean_assert(in_tmp_mode());
-    if (m_tmp_data->m_uassignment.size() < num_uvars)
-        m_tmp_data->m_uassignment.resize(num_uvars, none_level());
-    if (m_tmp_data->m_eassignment.size() < num_mvars)
-        m_tmp_data->m_eassignment.resize(num_mvars, none_expr());
-}
-
 optional<level> type_context_old::get_tmp_uvar_assignment(unsigned idx) const {
     lean_assert(in_tmp_mode());
     lean_assert(idx < m_tmp_data->m_uassignment.size());
@@ -1287,12 +1279,18 @@ level type_context_old::mk_tmp_univ_mvar() {
 expr type_context_old::mk_tmp_mvar(expr const & type) {
     lean_assert(in_tmp_mode());
     unsigned idx = m_tmp_data->m_eassignment.size();
+    m_tmp_data->m_etype.push_back(type);
     m_tmp_data->m_eassignment.push_back(none_expr());
-    return mk_idx_metavar(idx, type);
+    return mk_idx_metavar(idx);
+}
+
+expr type_context_old::get_tmp_mvar_type(expr const & mvar) const {
+    return m_tmp_data->m_etype[to_meta_idx(mvar)];
 }
 
 void type_context_old::resize_tmp_mvars(unsigned sz) {
     lean_assert(in_tmp_mode());
+    m_tmp_data->m_etype.resize(sz, expr());
     m_tmp_data->m_eassignment.resize(sz, optional<expr>());
 }
 
@@ -1415,6 +1413,7 @@ void type_context_old::pop_scope() {
         }
         lean_assert(old_sz == m_tmp_data->m_trail.size());
         m_tmp_data->m_uassignment.shrink(s.m_tmp_uassignment_sz);
+        m_tmp_data->m_etype.shrink(s.m_tmp_eassignment_sz);
         m_tmp_data->m_eassignment.shrink(s.m_tmp_eassignment_sz);
     }
     m_scopes.pop_back();
@@ -3504,7 +3503,7 @@ struct instance_synthesizer {
         // When it is used, it creates a subproblem for
         //    is_nsubg : @is_normal_subgroup A s ?N
         // where ?N is not known. Actually, we can only find the value for ?N by constructing the instance is_nsubg.
-        expr mvar_ty       = m_ctx.instantiate_mvars(mvar_type(mvar));
+        expr mvar_ty       = m_ctx.instantiate_mvars(m_ctx.get_tmp_mvar_type(mvar));
         m_choices.push_back(choice());
         push_scope();
         choice & r = m_choices.back();
diff --git a/src/library/type_context.h b/src/library/type_context.h
index da0f248280..824a82fdd8 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -46,6 +46,7 @@ struct unifier_config {
 
 class type_context_old : public abstract_type_context {
     typedef buffer<optional<level>> tmp_uassignment;
+    typedef buffer<expr>            tmp_etype;
     typedef buffer<optional<expr>>  tmp_eassignment;
     typedef buffer<metavar_context> mctx_stack;
     enum class tmp_trail_kind { Level, Expr };
@@ -369,14 +370,15 @@ public:
        They are nullptr if type_context_old is not in tmp_mode. */
     struct tmp_data {
         tmp_uassignment & m_uassignment;
+        tmp_etype       & m_etype;
         tmp_eassignment & m_eassignment;
         /* m_tmp_mvar_local_context contains m_lctx when tmp mode is activated.
            This is the context for all temporary meta-variables. */
         local_context     m_mvar_lctx;
         /* undo/trail stack for m_tmp_uassignment/m_tmp_eassignment */
         tmp_trail         m_trail;
-        tmp_data(tmp_uassignment & uassignment, tmp_eassignment & eassignment, local_context const & lctx):
-            m_uassignment(uassignment), m_eassignment(eassignment), m_mvar_lctx(lctx) {}
+        tmp_data(tmp_uassignment & uassignment, tmp_etype & etype, tmp_eassignment & eassignment, local_context const & lctx):
+            m_uassignment(uassignment), m_etype(etype), m_eassignment(eassignment), m_mvar_lctx(lctx) {}
     };
 private:
     typedef buffer<scope_data> scopes;
@@ -781,13 +783,12 @@ public:
     struct tmp_mode_scope {
         type_context_old &      m_ctx;
         buffer<optional<level>> m_tmp_uassignment;
+        buffer<expr>            m_tmp_etype;
         buffer<optional<expr>>  m_tmp_eassignment;
         tmp_data *              m_old_data;
         tmp_data                m_data;
-        tmp_mode_scope(type_context_old & ctx, unsigned next_uidx = 0, unsigned next_midx = 0):
-            m_ctx(ctx), m_old_data(ctx.m_tmp_data), m_data(m_tmp_uassignment, m_tmp_eassignment, ctx.lctx()) {
-            m_tmp_uassignment.resize(next_uidx, none_level());
-            m_tmp_eassignment.resize(next_midx, none_expr());
+        tmp_mode_scope(type_context_old & ctx):
+            m_ctx(ctx), m_old_data(ctx.m_tmp_data), m_data(m_tmp_uassignment, m_tmp_etype, m_tmp_eassignment, ctx.lctx()) {
             m_ctx.m_tmp_data = &m_data;
         }
         ~tmp_mode_scope() {
@@ -806,13 +807,13 @@ public:
         }
     };
     bool in_tmp_mode() const { return m_tmp_data != nullptr; }
-    void ensure_num_tmp_mvars(unsigned num_uvars, unsigned num_mvars);
     optional<level> get_tmp_uvar_assignment(unsigned idx) const;
     optional<expr> get_tmp_mvar_assignment(unsigned idx) const;
     optional<level> get_tmp_assignment(level const & l) const;
     optional<expr> get_tmp_assignment(expr const & e) const;
     level mk_tmp_univ_mvar();
     expr mk_tmp_mvar(expr const & type);
+    expr get_tmp_mvar_type(expr const & mvar) const;
 
     /* Helper class to reset m_used_assignment flag */
     class reset_used_assignment {
diff --git a/tests/lean/check.lean.expected.out b/tests/lean/check.lean.expected.out
deleted file mode 100644
index 61cd4d34a7..0000000000
--- a/tests/lean/check.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-And.intro : ?M_1 → ?M_2 → ?M_1 ∧ ?M_2
-Or.elim : ?M_1 ∨ ?M_2 → (?M_1 → ?M_3) → (?M_2 → ?M_3) → ?M_3
-Eq : ?M_1 → ?M_1 → Prop
-Eq.rec : ?M_3 ?M_2 _ → Π {a : ?M_1} (t : ?M_2 = a), ?M_3 a t
diff --git a/tests/lean/check.lean b/tests/lean/run/check.lean
similarity index 100%
rename from tests/lean/check.lean
rename to tests/lean/run/check.lean