diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index f1ab6e4d1b..727b9bcd65 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "expr_maps.h"
 #include "sstream.h"
 #include "kernel_exception.h"
+#include "metavar.h"
 #include "elaborator.h"
 #include "lean_frontend.h"
 #include "lean_parser.h"
@@ -873,7 +874,7 @@ class parser::imp {
 
     /** \brief Create a fresh metavariable. */
     expr mk_metavar() {
-        return m_elaborator.mk_metavar(m_num_local_decls);
+        return m_elaborator.mk_metavar();
     }
 
     /** \brief Parse \c _ a hole that must be filled by the elaborator. */
diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp
index 5902c593ce..85d952cba5 100644
--- a/src/frontends/lean/lean_pp.cpp
+++ b/src/frontends/lean/lean_pp.cpp
@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 #include "context_to_lambda.h"
 #include "options.h"
 #include "interruptable_ptr.h"
-#include "metavar_env.h"
+#include "metavar.h"
 #include "exception.h"
 #include "lean_notation.h"
 #include "lean_pp.h"
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 57ce4b0d66..5e9941c8c2 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,3 +1,4 @@
-add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp
-  formatter.cpp context_to_lambda.cpp state.cpp beta.cpp metavar.cpp metavar_env.cpp elaborator.cpp)
+add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
+  toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
+  state.cpp beta.cpp metavar.cpp elaborator.cpp)
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp
index 90ea46ff4e..41b6a7673e 100644
--- a/src/library/elaborator.cpp
+++ b/src/library/elaborator.cpp
@@ -4,12 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <deque>
 #include "elaborator.h"
-#include "free_vars.h"
-#include "beta.h"
-#include "instantiate.h"
+#include "metavar.h"
+#include "printer.h"
+#include "context.h"
 #include "builtin.h"
-#include "exception.h"
+#include "free_vars.h"
+#include "for_each.h"
+#include "replace.h"
+#include "flet.h"
+#include "elaborator_exception.h"
 
 namespace lean {
 static name g_overload_name(name(name(name(0u), "library"), "overload"));
@@ -23,143 +28,511 @@ expr mk_overload_marker() {
     return g_overload;
 }
 
-expr elaborator::lookup(context const & c, unsigned i) {
-    auto p = lookup_ext(c, i);
-    context_entry const & def = p.first;
-    context const & def_c     = p.second;
-    lean_assert(length(c) > length(def_c));
-    return lift_free_vars(def.get_domain(), length(c) - length(def_c));
-}
+class elaborator::imp {
+    // unification constraint lhs == second
+    struct constraint {
+        expr     m_lhs;
+        expr     m_rhs;
+        context  m_ctx;
+        expr     m_source;     // auxiliary field used for producing error msgs
+        context  m_source_ctx; // auxiliary field used for producing error msgs
+        unsigned m_arg_pos;    // auxiliary field used for producing error msgs
+        constraint(expr const & lhs, expr const & rhs, context const & ctx, expr const & src, context const & src_ctx, unsigned arg_pos):
+            m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(src), m_source_ctx(src_ctx), m_arg_pos(arg_pos) {}
+        constraint(expr const & lhs, expr const & rhs, constraint const & c):
+            m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
+        constraint(expr const & lhs, expr const & rhs, context const & ctx, constraint const & c):
+            m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
+    };
 
-elaborator::elaborator(environment const & env):
-    m_env(env), m_metaenv(env) {
-}
-
-void elaborator::unify(expr const & e1, expr const & e2, context const & ctx) {
-    if (has_metavar(e1) || has_metavar(e2)) {
-        m_metaenv.unify(e1, e2, ctx);
-    }
-}
-
-expr elaborator::check_pi(expr const & e, context const & ctx) {
-    if (!e) {
-        // e is the type of a metavariable.
-        // approx: assume it is Type()
-        return Type();
-    } else if (is_pi(e)) {
-        return e;
-    } else {
-        expr r = head_reduce(e, m_env);
-        if (!is_eqp(r, e)) {
-            return check_pi(r, ctx);
-        } else if (is_var(e)) {
-            auto p = lookup_ext(ctx, var_idx(e));
-            context_entry const & entry = p.first;
-            context const & entry_ctx   = p.second;
-            if (entry.get_body()) {
-                return lift_free_vars(check_pi(entry.get_body(), entry_ctx),
-                                      length(ctx) - length(entry_ctx));
-            }
+    // information associated with the metavariable
+    struct metavar_info {
+        expr    m_assignment;
+        expr    m_type;
+        expr    m_mvar;
+        context m_ctx;
+        bool    m_mark; // for implementing occurs check
+        metavar_info() {
+            m_mark = false;
         }
-        throw exception("function expected");
-    }
-}
+    };
 
-level elaborator::check_universe(expr const & e, context const & ctx) {
-    if (!e) {
-        // e is the type of a metavariable
-        // approx: assume it is level 0
-        return level();
-    } else if (is_type(e)) {
-        return ty_level(e);
-    } else {
-        expr r = head_reduce(e, m_env);
-        if (!is_eqp(r, e)) {
-            return check_universe(r, ctx);
-        } else if (is_var(e)) {
-            auto p = lookup_ext(ctx, var_idx(e));
-            context_entry const & entry = p.first;
-            context const & entry_ctx   = p.second;
-            if (entry.get_body()) {
-                return check_universe(entry.get_body(), entry_ctx);
-            }
-        }
-        throw exception("type expected");
-    }
-}
+    typedef std::deque<constraint>    constraint_queue;
+    typedef std::vector<metavar_info> metavars;
 
-/**
-   \brief Given e and a context, try to instantiate the
-   meta-variables in \c e. Return an inferred type for \c e.
-*/
-expr elaborator::process(expr const & e, context const & ctx) {
-    switch (e.kind()) {
-    case expr_kind::Constant:
-        if (is_metavar(e)) {
-            expr r = m_metaenv.root_at(e, ctx);
-            if (is_metavar(r)) {
-                return expr();
-            } else {
-                return process(r, ctx);
-            }
+    environment const & m_env;
+    name_set const *    m_available_defs;
+    elaborator const *  m_owner;
+
+    constraint_queue    m_constraints;
+    metavars            m_metavars;
+
+    bool                m_add_constraints;
+
+    volatile bool       m_interrupted;
+
+    expr metavar_type(expr const & m) {
+        lean_assert(is_metavar(m));
+        unsigned midx = metavar_idx(m);
+        if (m_metavars[midx].m_type) {
+            return m_metavars[midx].m_type;
         } else {
-            return m_env.get_object(const_name(e)).get_type();
+            expr t = mk_metavar();
+            m_metavars[midx].m_type = t;
+            return t;
         }
-    case expr_kind::Var:
-        return lookup(ctx, var_idx(e));
-    case expr_kind::Type:
-        return mk_type(ty_level(e) + 1);
-    case expr_kind::Value:
-        return to_value(e).get_type();
-    case expr_kind::App: {
-        buffer<expr> types;
-        unsigned num = num_args(e);
-        for (unsigned i = 0; i < num; i++) {
-            types.push_back(process(arg(e,i), ctx));
-        }
-        // TODO: handle overload in args[0]
-        expr f_t = types[0];
-        if (!f_t) {
-            throw exception("invalid use of placeholder, the function must be provided to an application");
-        }
-        for (unsigned i = 1; i < num; i++) {
-            f_t = check_pi(f_t, ctx);
-            if (types[i])
-                unify(abst_domain(f_t), types[i], ctx);
-            f_t = instantiate(abst_body(f_t), arg(e, i));
-        }
-        return f_t;
     }
-    case expr_kind::Eq: {
-        process(eq_lhs(e), ctx);
-        process(eq_rhs(e), ctx);
-        return mk_bool_type();
-    }
-    case expr_kind::Pi: {
-        expr dt = process(abst_domain(e), ctx);
-        expr bt = process(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
-        return mk_type(max(check_universe(dt, ctx), check_universe(bt, ctx)));
-    }
-    case expr_kind::Lambda: {
-        expr dt = process(abst_domain(e), ctx);
-        expr bt = process(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
-        return mk_pi(abst_name(e), abst_domain(e), bt);
-    }
-    case expr_kind::Let: {
-        expr lt = process(let_value(e), ctx);
-        return process(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
-    }}
-    lean_unreachable();
-    return expr();
-}
 
-expr elaborator::operator()(expr const & e) {
-    while (true) {
-        process(e, context());
-        if (!m_metaenv.modified())
-            break;
-        m_metaenv.reset_modified();
+    expr lookup(context const & c, unsigned i) {
+        auto p = lookup_ext(c, i);
+        context_entry const & def = p.first;
+        context const & def_c     = p.second;
+        lean_assert(length(c) > length(def_c));
+        return lift_free_vars_mmv(def.get_domain(), 0, length(c) - length(def_c));
     }
-    return m_metaenv.instantiate_metavars(e);
-}
+
+    expr check_pi(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
+        check_interrupted(m_interrupted);
+        if (is_pi(e)) {
+            return e;
+        } else {
+            expr r = head_reduce_mmv(e, m_env, m_available_defs);
+            if (!is_eqp(r, e)) {
+                return check_pi(r, ctx, s, s_ctx);
+            } else if (is_var(e)) {
+                try {
+                    auto p = lookup_ext(ctx, var_idx(e));
+                    context_entry const & entry = p.first;
+                    context const & entry_ctx   = p.second;
+                    if (entry.get_body()) {
+                        return lift_free_vars_mmv(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, length(ctx) - length(entry_ctx));
+                    }
+                } catch (exception&) {
+                    // this can happen if we access a variable out of scope
+                    throw function_expected_exception(m_env, s_ctx, s);
+                }
+            }
+            throw function_expected_exception(m_env, s_ctx, s);
+        }
+    }
+
+    level check_universe(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
+        check_interrupted(m_interrupted);
+        if (is_metavar(e)) {
+            // approx: assume it is level 0
+            return level();
+        } else if (is_type(e)) {
+            return ty_level(e);
+        } else {
+            expr r = head_reduce_mmv(e, m_env, m_available_defs);
+            if (!is_eqp(r, e)) {
+                return check_universe(r, ctx, s, s_ctx);
+            } else if (is_var(e)) {
+                try {
+                    auto p = lookup_ext(ctx, var_idx(e));
+                    context_entry const & entry = p.first;
+                    context const & entry_ctx   = p.second;
+                    if (entry.get_body()) {
+                        return check_universe(entry.get_body(), entry_ctx, s, s_ctx);
+                    }
+                } catch (exception&) {
+                    // this can happen if we access a variable out of scope
+                    throw type_expected_exception(m_env, s_ctx, s);
+                }
+            }
+            throw type_expected_exception(m_env, s_ctx, s);
+        }
+    }
+
+    void add_constraint(expr const & t1, expr const & t2, context const & ctx, expr const & s, unsigned arg_pos) {
+        if (has_metavar(t1) || has_metavar(t2)) {
+            m_constraints.push_back(constraint(t1, t2, ctx, s, ctx, arg_pos));
+        }
+    }
+
+    expr infer(expr const & e, context const & ctx) {
+        check_interrupted(m_interrupted);
+        switch (e.kind()) {
+        case expr_kind::Constant:
+            if (is_metavar(e)) {
+                unsigned midx = metavar_idx(e);
+                if (!(m_metavars[midx].m_ctx)) {
+                    lean_assert(!(m_metavars[midx].m_mvar));
+                    m_metavars[midx].m_mvar = e;
+                    m_metavars[midx].m_ctx  = ctx;
+                }
+                return metavar_type(e);
+            } else {
+                return m_env.get_object(const_name(e)).get_type();
+            }
+        case expr_kind::Var:
+            return lookup(ctx, var_idx(e));
+        case expr_kind::Type:
+            return mk_type(ty_level(e) + 1);
+        case expr_kind::Value:
+            return to_value(e).get_type();
+        case expr_kind::App: {
+            buffer<expr> types;
+            unsigned num = num_args(e);
+            for (unsigned i = 0; i < num; i++) {
+                types.push_back(infer(arg(e,i), ctx));
+            }
+            // TODO: handle overload in args[0]
+            expr f_t = types[0];
+            if (!f_t) {
+                throw invalid_placeholder_exception(*m_owner, ctx, e);
+            }
+            for (unsigned i = 1; i < num; i++) {
+                f_t = check_pi(f_t, ctx, e, ctx);
+                if (m_add_constraints)
+                    add_constraint(abst_domain(f_t), types[i], ctx, e, i);
+                f_t = instantiate_free_var_mmv(abst_body(f_t), 0, arg(e, i));
+            }
+            return f_t;
+        }
+        case expr_kind::Eq: {
+            infer(eq_lhs(e), ctx);
+            infer(eq_rhs(e), ctx);
+            return mk_bool_type();
+        }
+        case expr_kind::Pi: {
+            expr dt = infer(abst_domain(e), ctx);
+            expr bt = infer(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
+            return mk_type(max(check_universe(dt, ctx, e, ctx), check_universe(bt, ctx, e, ctx)));
+        }
+        case expr_kind::Lambda: {
+            expr dt = infer(abst_domain(e), ctx);
+            expr bt = infer(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
+            return mk_pi(abst_name(e), abst_domain(e), bt);
+        }
+        case expr_kind::Let: {
+            expr lt = infer(let_value(e), ctx);
+            return infer(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
+        }}
+        lean_unreachable();
+        return expr();
+    }
+
+    bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
+        if (is_app(e1) && is_meta(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && length(ctx) > 0) {
+            return true;
+        } else {
+            return false;
+        }
+    }
+
+    void unify_simple_ho_match(expr const & e1, expr const & e2, constraint const & c) {
+        context const & ctx = c.m_ctx;
+        m_constraints.push_back(constraint(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), c));
+    }
+
+    struct cycle_detected {};
+    void occ_core(expr const & t) {
+        check_interrupted(m_interrupted);
+        auto proc = [&](expr const & e, unsigned offset) {
+            if (is_metavar(e)) {
+                unsigned midx = metavar_idx(e);
+                if (m_metavars[midx].m_mark)
+                    throw cycle_detected();
+                if (m_metavars[midx].m_assignment) {
+                    flet<bool> set(m_metavars[midx].m_mark, true);
+                    occ_core(m_metavars[midx].m_assignment);
+                }
+            }
+        };
+        for_each_fn<decltype(proc)> visitor(proc);
+        visitor(t);
+    }
+
+    // occurs check
+    bool occ(expr const & t, unsigned midx) {
+        lean_assert(!m_metavars[midx].m_mark);
+        flet<bool> set(m_metavars[midx].m_mark, true);
+        try {
+            occ_core(t);
+            return true;
+        } catch (cycle_detected&) {
+            return false;
+        }
+    }
+
+    [[noreturn]] void throw_unification_exception(constraint const & c) {
+        // display(std::cout);
+        m_constraints.push_back(c);
+        if (c.m_arg_pos != static_cast<unsigned>(-1)) {
+            throw unification_app_mismatch_exception(*m_owner, c.m_source_ctx, c.m_source, c.m_arg_pos);
+        } else {
+            throw unification_type_mismatch_exception(*m_owner, c.m_source_ctx, c.m_source);
+        }
+    }
+
+    void solve_mvar(expr const & m, expr const & t, constraint const & c) {
+        lean_assert(is_metavar(m));
+        unsigned midx = metavar_idx(m);
+        if (m_metavars[midx].m_assignment) {
+            m_constraints.push_back(constraint(m_metavars[midx].m_assignment, t, c));
+        } else if (has_metavar(t, midx) || !occ(t, midx)) {
+            throw_unification_exception(c);
+        } else {
+            m_metavars[midx].m_assignment = t;
+        }
+    }
+
+    bool solve_meta(expr const & e, expr const & t, constraint const & c) {
+        lean_assert(!is_metavar(e));
+        expr const & m = get_metavar(e);
+        unsigned midx  = metavar_idx(m);
+        unsigned i, s, n;
+        expr v, a, b;
+
+        if (m_metavars[midx].m_assignment) {
+            expr s = instantiate_metavar(e, midx, m_metavars[midx].m_assignment);
+            m_constraints.push_back(constraint(s, t, c));
+            return true;
+        }
+
+        if (!has_metavar(t)) {
+            if (is_lower(e, a, s, n)) {
+                m_constraints.push_back(constraint(a, lift_free_vars_mmv(t, s-n, n), c));
+                return true;
+            }
+
+            if (is_lift(e, a, s, n)) {
+                if (!has_free_var(t, s, s+n)) {
+                    m_constraints.push_back(constraint(a, lower_free_vars_mmv(t, s+n, n), c));
+                    return true;
+                } else {
+                    // display(std::cout);
+                    throw_unification_exception(c);
+                }
+            }
+        }
+
+        if (has_assigned_metavar(t)) {
+            m_constraints.push_back(constraint(e, instantiate(t), c));
+            return true;
+        }
+
+        if (is_subst(e, a, i, v) && is_lift(a, b, s, n) && has_free_var(t, s, s+n)) {
+            // subst (lift b s n) i v  ==  t
+            // (lift b s n) does not have free-variables in the range [s, s+n)
+            // Thus, if t has a free variables in [s, s+n), then the only possible solution is
+            //    (lift b s n) == i
+            //    v == t
+            m_constraints.push_back(constraint(a, mk_var(i), c));
+            m_constraints.push_back(constraint(v, t, c));
+            return true;
+        }
+
+        return false;
+    }
+
+    void solve_core() {
+        unsigned delayed = 0;
+        unsigned last_num_constraints = 0;
+        while (!m_constraints.empty()) {
+            check_interrupted(m_interrupted);
+            constraint c = m_constraints.front();
+            m_constraints.pop_front();
+            expr const & lhs = c.m_lhs;
+            expr const & rhs = c.m_rhs;
+            // std::cout << "Solving " << lhs << " === " << rhs << "\n";
+            if (lhs == rhs || (!has_metavar(lhs) && !has_metavar(rhs))) {
+                // do nothing
+                delayed = 0;
+            } else if (is_metavar(lhs)) {
+                delayed = 0;
+                solve_mvar(lhs, rhs, c);
+            } else if (is_metavar(rhs)) {
+                delayed = 0;
+                solve_mvar(rhs, lhs, c);
+            } else if (is_meta(lhs) || is_meta(rhs)) {
+                if (is_meta(lhs) && solve_meta(lhs, rhs, c)) {
+                    delayed = 0;
+                } else if (is_meta(rhs) && solve_meta(rhs, lhs, c)) {
+                    delayed = 0;
+                } else {
+                    m_constraints.push_back(c);
+                    if (delayed == 0) {
+                        last_num_constraints = m_constraints.size();
+                        delayed++;
+                    } else if (delayed > last_num_constraints) {
+                        throw_unification_exception(c);
+                    } else {
+                        delayed++;
+                    }
+                }
+            } else if (is_type(lhs) && is_type(rhs)) {
+                delayed = 0;
+                return; // ignoring type universe levels. We let the kernel check that
+            } else if (is_abstraction(lhs) && is_abstraction(rhs)) {
+                delayed = 0;
+                m_constraints.push_back(constraint(abst_domain(lhs), abst_domain(rhs), c));
+                m_constraints.push_back(constraint(abst_body(lhs),   abst_body(rhs), extend(c.m_ctx, abst_name(lhs), abst_domain(lhs)), c));
+            } else if (is_eq(lhs) && is_eq(rhs)) {
+                delayed = 0;
+                m_constraints.push_back(constraint(eq_lhs(lhs), eq_lhs(rhs), c));
+                m_constraints.push_back(constraint(eq_rhs(lhs), eq_rhs(rhs), c));
+            } else {
+                expr new_lhs = head_reduce_mmv(lhs, m_env, m_available_defs);
+                expr new_rhs = head_reduce_mmv(rhs, m_env, m_available_defs);
+                if (!is_eqp(lhs, new_lhs) || !is_eqp(rhs, new_rhs)) {
+                    delayed = 0;
+                    m_constraints.push_back(constraint(new_lhs, new_rhs, c));
+                } else if (is_app(new_lhs) && is_app(new_rhs) && num_args(new_lhs) == num_args(new_rhs)) {
+                    delayed = 0;
+                    unsigned num = num_args(new_lhs);
+                    for (unsigned i = 0; i < num; i++) {
+                        m_constraints.push_back(constraint(arg(new_lhs, i), arg(new_rhs, i), c));
+                    }
+                } else if (is_simple_ho_match(new_lhs, new_rhs, c.m_ctx)) {
+                    delayed = 0;
+                    unify_simple_ho_match(new_lhs, new_rhs, c);
+                } else if (is_simple_ho_match(new_rhs, new_lhs, c.m_ctx)) {
+                    delayed = 0;
+                    unify_simple_ho_match(new_rhs, new_lhs, c);
+                } else {
+                    throw_unification_exception(c);
+                }
+            }
+        }
+    }
+
+    struct found_assigned {};
+    bool has_assigned_metavar(expr const & e) {
+        auto proc = [&](expr const & n, unsigned offset) {
+            if (is_metavar(n)) {
+                unsigned midx = metavar_idx(n);
+                if (m_metavars[midx].m_assignment)
+                    throw found_assigned();
+            }
+        };
+        for_each_fn<decltype(proc)> visitor(proc);
+        try {
+            visitor(e);
+            return false;
+        } catch (found_assigned&) {
+            return true;
+        }
+    }
+
+    expr instantiate(expr const & e) {
+        auto proc = [&](expr const & n, unsigned offset) {
+            if (is_meta(n)) {
+                expr const & m = get_metavar(n);
+                unsigned midx = metavar_idx(m);
+                if (m_metavars[midx].m_assignment) {
+                    if (has_assigned_metavar(m_metavars[midx].m_assignment)) {
+                        m_metavars[midx].m_assignment = instantiate(m_metavars[midx].m_assignment);
+                    }
+                    return instantiate_metavar(n, midx, m_metavars[midx].m_assignment);
+                }
+            }
+            return n;
+        };
+        replace_fn<decltype(proc)> replacer(proc);
+        return replacer(e);
+    }
+
+    void solve(unsigned num_meta) {
+        m_add_constraints = false;
+        while (true) {
+            solve_core();
+            bool cont     = false;
+            bool progress = false;
+            unsigned unsolved_midx = 0;
+            for (unsigned midx = 0; midx < num_meta; midx++) {
+                if (m_metavars[midx].m_assignment) {
+                    if (has_assigned_metavar(m_metavars[midx].m_assignment)) {
+                        m_metavars[midx].m_assignment = instantiate(m_metavars[midx].m_assignment);
+                    }
+                    if (has_metavar(m_metavars[midx].m_assignment)) {
+                        unsolved_midx = midx;
+                        cont = true; // must continue
+                    } else {
+                        if (m_metavars[midx].m_type) {
+                            try {
+                                expr t = infer(m_metavars[midx].m_assignment, m_metavars[midx].m_ctx);
+                                m_constraints.push_back(constraint(m_metavars[midx].m_type, t, m_metavars[midx].m_ctx,
+                                                                   m_metavars[midx].m_mvar, m_metavars[midx].m_ctx, static_cast<unsigned>(-1)));
+                                progress = true;
+                            } catch (exception&) {
+                                // std::cout << "Failed to infer: " << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
+                                throw unification_type_mismatch_exception(*m_owner, m_metavars[midx].m_ctx, m_metavars[midx].m_mvar);
+                            }
+                        }
+                    }
+                }
+            }
+            if (!cont)
+                return;
+            if (!progress)
+                throw unsolved_placeholder_exception(*m_owner, m_metavars[unsolved_midx].m_ctx, m_metavars[unsolved_midx].m_mvar);
+        }
+    }
+
+
+public:
+    imp(environment const & env, name_set const * defs):
+        m_env(env),
+        m_available_defs(defs) {
+        m_interrupted = false;
+        m_owner = nullptr;
+    }
+
+    expr mk_metavar() {
+        unsigned midx = m_metavars.size();
+        expr r = ::lean::mk_metavar(midx);
+        m_metavars.push_back(metavar_info());
+        return r;
+    }
+
+    void clear() {
+        m_constraints.clear();
+        m_metavars.clear();
+    }
+
+    void set_interrupt(bool flag) {
+        m_interrupted = flag;
+    }
+
+    void display(std::ostream & out) {
+        for (unsigned i = 0; i < m_metavars.size(); i++) {
+            out << "#" << i << " ";
+            auto m = m_metavars[i];
+            if (m.m_assignment)
+                out << m.m_assignment;
+            else
+                out << "[unassigned]";
+            if (m.m_type)
+                out << ", type: " << m.m_type;
+            out << "\n";
+        }
+
+        for (auto c : m_constraints) {
+            out << c.m_lhs << " === " << c.m_rhs << "\n";
+        }
+    }
+
+    environment const & get_environment() const {
+        return m_env;
+    }
+
+    expr operator()(expr const & e, elaborator const & elb) {
+        m_owner = &elb;
+        unsigned num_meta = m_metavars.size();
+        m_add_constraints = true;
+        infer(e, context());
+        solve(num_meta);
+        return instantiate(e);
+    }
+};
+elaborator::elaborator(environment const & env):m_ptr(new imp(env, nullptr)) {}
+elaborator::~elaborator() {}
+expr elaborator::mk_metavar() { return m_ptr->mk_metavar(); }
+expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, *this); }
+void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
+void elaborator::clear() { m_ptr->clear(); }
+environment const & elaborator::get_environment() const { return m_ptr->get_environment(); }
+void elaborator::display(std::ostream & out) const { m_ptr->display(out); }
 }
diff --git a/src/library/elaborator.h b/src/library/elaborator.h
index f4b21417ef..823d597a99 100644
--- a/src/library/elaborator.h
+++ b/src/library/elaborator.h
@@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "metavar_env.h"
+#include <memory>
+#include "environment.h"
 
 namespace lean {
 /**
@@ -14,31 +15,26 @@ namespace lean {
    the value of implicit arguments.
 */
 class elaborator {
-    environment const & m_env;
-    metavar_env         m_metaenv;
-
-    expr lookup(context const & c, unsigned i);
-    void unify(expr const & e1, expr const & e2, context const & ctx);
-    expr check_pi(expr const & e, context const & ctx);
-    level check_universe(expr const & e, context const & ctx);
-    expr process(expr const & e, context const & ctx);
-
+    class imp;
+    std::shared_ptr<imp> m_ptr;
 public:
-    elaborator(environment const & env);
+    explicit elaborator(environment const & env);
+    ~elaborator();
+
+    expr mk_metavar();
+
     expr operator()(expr const & e);
 
-    metavar_env & menv() { return m_metaenv; }
-
-    void clear() { m_metaenv.clear(); }
-    expr mk_metavar(unsigned ctx_sz) { return m_metaenv.mk_metavar(ctx_sz); }
-
-    void set_interrupt(bool flag) { m_metaenv.set_interrupt(flag); }
+    void set_interrupt(bool flag);
     void interrupt() { set_interrupt(true); }
     void reset_interrupt() { set_interrupt(false); }
 
-    void display(std::ostream & out) const { m_metaenv.display(out); }
-};
+    void clear();
 
+    environment const & get_environment() const;
+
+    void display(std::ostream & out) const;
+};
 /** \brief Return true iff \c e is a special constant used to mark application of overloads. */
 bool is_overload_marker(expr const & e);
 /** \brief Return the overload marker */
diff --git a/src/library/elaborator_exception.h b/src/library/elaborator_exception.h
new file mode 100644
index 0000000000..bb340e5ba7
--- /dev/null
+++ b/src/library/elaborator_exception.h
@@ -0,0 +1,56 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "elaborator.h"
+#include "kernel_exception.h"
+
+namespace lean {
+/**
+    \brief Base class for elaborator exceptions.
+
+    \remark We reuse kernel exceptions to sign type errors during
+    elaboration. Perhaps we should wrap them as elaborator exceptions.
+*/
+class elaborator_exception : public exception {
+protected:
+    elaborator m_elb;
+    context    m_context;
+    expr       m_expr;
+public:
+    elaborator_exception(elaborator const & elb, context const & ctx, expr const & e):m_elb(elb), m_context(ctx), m_expr(e) {}
+    virtual ~elaborator_exception() noexcept {}
+    elaborator const & get_elaborator() const { return m_elb; }
+    expr const & get_expr() const { return m_expr; }
+    context const & get_context() const { return m_context; }
+};
+
+class invalid_placeholder_exception : public elaborator_exception {
+public:
+    invalid_placeholder_exception(elaborator const & elb, context const & ctx, expr const & e):elaborator_exception(elb, ctx, e) {}
+    virtual char const * what() const noexcept { return "invalid placeholder occurrence, placeholder cannot be used as application head"; }
+};
+
+class unsolved_placeholder_exception : public elaborator_exception {
+public:
+    unsolved_placeholder_exception(elaborator const & elb, context const & ctx, expr const & e):elaborator_exception(elb, ctx, e) {}
+    virtual char const * what() const noexcept { return "unsolved placeholder, system could not fill this placeholder"; }
+};
+
+class unification_app_mismatch_exception : public elaborator_exception {
+    unsigned m_arg_pos;
+public:
+    unification_app_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, unsigned pos):elaborator_exception(elb, ctx, s), m_arg_pos(pos) {}
+    unsigned get_arg_pos() const { return m_arg_pos; }
+    virtual char const * what() const noexcept { return "failed to solve unification problem during elaboration"; }
+};
+
+class unification_type_mismatch_exception : public elaborator_exception {
+public:
+    unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s):elaborator_exception(elb, ctx, s) {}
+    virtual char const * what() const noexcept { return "failed to solve unification problem during elaboration"; }
+};
+}
diff --git a/src/library/metavar.cpp b/src/library/metavar.cpp
index e5b77f778b..8b44725be4 100644
--- a/src/library/metavar.cpp
+++ b/src/library/metavar.cpp
@@ -9,6 +9,8 @@ Author: Leonardo de Moura
 #include "for_each.h"
 #include "environment.h"
 
+#include "printer.h"
+
 namespace lean {
 static name g_metavar_prefix(name(name(name(0u), "library"), "metavar"));
 static name g_subst_prefix(name(name(name(0u), "library"), "subst"));
@@ -67,13 +69,20 @@ bool is_subst_fn(expr const & n) {
 }
 
 expr mk_subst(expr const & e, unsigned i, expr const & c) {
-    return mk_app(mk_subst_fn(i), e, c);
+    unsigned s, n;
+    expr a;
+    if (is_lift(e, a, s, n) && s <= i && i < s+n) {
+        return e;
+    } else {
+        return mk_eq(mk_subst_fn(i), mk_eq(e, c));
+    }
 }
 
-bool is_subst(expr const & e, unsigned & i, expr & c) {
-    if (is_app(e) && is_subst_fn(arg(e,0))) {
-        i = const_name(arg(e,0)).get_numeral();
-        c = arg(e,2);
+bool is_subst(expr const & e, expr & c, unsigned & i, expr & v) {
+    if (is_eq(e) && is_subst_fn(eq_lhs(e))) {
+        i = const_name(eq_lhs(e)).get_numeral();
+        c = eq_lhs(eq_rhs(e));
+        v = eq_rhs(eq_rhs(e));
         return true;
     } else {
         return false;
@@ -81,7 +90,7 @@ bool is_subst(expr const & e, unsigned & i, expr & c) {
 }
 
 bool is_subst(expr const & e) {
-    return is_app(e) && is_subst_fn(arg(e,0));
+    return is_eq(e) && is_subst_fn(eq_lhs(e));
 }
 
 expr mk_lift_fn(unsigned s, unsigned n) {
@@ -97,12 +106,13 @@ bool is_lift_fn(expr const & n) {
 }
 
 expr mk_lift(expr const & e, unsigned s, unsigned n) {
-    return mk_app(mk_lift_fn(s, n), e);
+    return mk_eq(mk_lift_fn(s, n), e);
 }
 
-bool is_lift(expr const & e, unsigned & s, unsigned & n) {
-    if (is_app(e) && is_lift_fn(arg(e,0))) {
-        name const & l = const_name(arg(e,0));
+bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n) {
+    if (is_eq(e) && is_lift_fn(eq_lhs(e))) {
+        name const & l = const_name(eq_lhs(e));
+        c = eq_rhs(e);
         n = l.get_numeral();
         s = l.get_prefix().get_numeral();
         return true;
@@ -112,7 +122,7 @@ bool is_lift(expr const & e, unsigned & s, unsigned & n) {
 }
 
 bool is_lift(expr const & e) {
-    return is_app(e) && is_lift_fn(arg(e,0));
+    return is_eq(e) && is_lift_fn(eq_lhs(e));
 }
 
 expr mk_lower_fn(unsigned s, unsigned n) {
@@ -127,13 +137,24 @@ bool is_lower_fn(expr const & n) {
         const_name(n).get_prefix().get_prefix() == g_lower_prefix;
 }
 
-expr mk_lower(expr const & e, unsigned s, unsigned n) {
-    return mk_app(mk_lower_fn(s, n), e);
+expr mk_lower(expr const & e, unsigned s2, unsigned n2) {
+    unsigned s1, n1;
+    expr c;
+    if (is_lift(e, c, s1, n1) && s1 <= s2 - n2 && s2 <= s1 + n1) {
+        n1 -= n2;
+        if (n1 == 0)
+            return c;
+        else
+            return mk_lift(c, s1, n1);
+    } else {
+        return mk_eq(mk_lower_fn(s2, n2), e);
+    }
 }
 
-bool is_lower(expr const & e, unsigned & s, unsigned & n) {
-    if (is_app(e) && is_lower_fn(arg(e,0))) {
-        name const & l = const_name(arg(e,0));
+bool is_lower(expr const & e, expr & c, unsigned & s, unsigned & n) {
+    if (is_eq(e) && is_lower_fn(eq_lhs(e))) {
+        name const & l = const_name(eq_lhs(e));
+        c = eq_rhs(e);
         n = l.get_numeral();
         s = l.get_prefix().get_numeral();
         return true;
@@ -143,16 +164,16 @@ bool is_lower(expr const & e, unsigned & s, unsigned & n) {
 }
 
 bool is_lower(expr const & e) {
-    return is_app(e) && is_lower_fn(arg(e,0));
+    return is_eq(e) && is_lower_fn(eq_lhs(e));
 }
 
 bool is_meta(expr const & e) {
     return is_metavar(e) || is_subst(e) || is_lift(e) || is_lower(e);
 }
 
-expr lower_free_vars_mmv(expr const & e, unsigned s, unsigned n) {
+expr lower_free_vars_mmv(expr const & a, unsigned s, unsigned n) {
     if (n == 0)
-        return e;
+        return a;
     lean_assert(s >= n);
     auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_var(e) && var_idx(e) >= s + offset) {
@@ -163,12 +184,12 @@ expr lower_free_vars_mmv(expr const & e, unsigned s, unsigned n) {
             return e;
         }
     };
-    return replace_fn<decltype(f)>(f)(e);
+    return replace_fn<decltype(f)>(f)(a);
 }
 
-expr lift_free_vars_mmv(expr const & e, unsigned s, unsigned n) {
+expr lift_free_vars_mmv(expr const & a, unsigned s, unsigned n) {
     if (n == 0)
-        return e;
+        return a;
     auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_var(e) && var_idx(e) >= s + offset) {
             return mk_var(var_idx(e) + n);
@@ -178,10 +199,10 @@ expr lift_free_vars_mmv(expr const & e, unsigned s, unsigned n) {
             return e;
         }
     };
-    return replace_fn<decltype(f)>(f)(e);
+    return replace_fn<decltype(f)>(f)(a);
 }
 
-expr instantiate_free_var_mmv(expr const & e, unsigned i, expr const & c) {
+expr instantiate_free_var_mmv(expr const & a, unsigned i, expr const & c) {
     auto f = [&](expr const & e, unsigned offset) -> expr {
         if (is_var(e)) {
             unsigned vidx = var_idx(e);
@@ -197,10 +218,10 @@ expr instantiate_free_var_mmv(expr const & e, unsigned i, expr const & c) {
             return e;
         }
     };
-    return replace_fn<decltype(f)>(f)(e);
+    return replace_fn<decltype(f)>(f)(a);
 }
 
-expr subst_mmv(expr const & e, unsigned i, expr const & c) {
+expr subst_mmv(expr const & a, unsigned i, expr const & c) {
     auto f = [&](expr const & e, unsigned offset) -> expr {
         if (is_var(e)) {
             unsigned vidx = var_idx(e);
@@ -214,7 +235,7 @@ expr subst_mmv(expr const & e, unsigned i, expr const & c) {
             return e;
         }
     };
-    return replace_fn<decltype(f)>(f)(e);
+    return replace_fn<decltype(f)>(f)(a);
 }
 
 expr get_metavar(expr const & e) {
@@ -222,29 +243,40 @@ expr get_metavar(expr const & e) {
     if (is_metavar(e)) {
         return e;
     } else {
-        return get_metavar(arg(e, 1));
+        unsigned i, s, n;
+        expr c, v;
+        if (is_lift(e, c, s, n)) {
+            return get_metavar(c);
+        } else if (is_lower(e, c, s, n)) {
+            return get_metavar(c);
+        } else if (is_subst(e, c, i, v)) {
+            return get_metavar(c);
+        } else {
+            lean_unreachable();
+            return e;
+        }
     }
 }
 
 expr instantiate_metavar_core(expr const & e, expr const & v) {
     lean_assert(is_meta(e));
     unsigned i, s, n;
-    expr c;
+    expr c, a;
     if (is_metavar(e)) {
         return v;
-    } else if (is_subst(e, i, c)) {
-        return subst_mmv(instantiate_metavar_core(arg(e, 1), v), i, c);
-    } else if (is_lift(e, s, n)) {
-        return lift_free_vars_mmv(instantiate_metavar_core(arg(e, 1), v), s, n);
-    } else if (is_lower(e, s, n)) {
-        return lower_free_vars_mmv(instantiate_metavar_core(arg(e, 1), v), s, n);
+    } else if (is_subst(e, c, i, a)) {
+        return subst_mmv(instantiate_metavar_core(c, v), i, a);
+    } else if (is_lift(e, c, s, n)) {
+        return lift_free_vars_mmv(instantiate_metavar_core(c, v), s, n);
+    } else if (is_lower(e, c, s, n)) {
+        return lower_free_vars_mmv(instantiate_metavar_core(c, v), s, n);
     } else {
         lean_unreachable();
         return e;
     }
 }
 
-expr instantiate_metavar(expr const & e, unsigned midx, expr const & v) {
+expr instantiate_metavar(expr const & a, unsigned midx, expr const & v) {
     auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_meta(e)) {
             expr m = get_metavar(e);
@@ -258,7 +290,7 @@ expr instantiate_metavar(expr const & e, unsigned midx, expr const & v) {
             return e;
         }
     };
-    return replace_fn<decltype(f)>(f)(e);
+    return replace_fn<decltype(f)>(f)(a);
 }
 
 expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs) {
@@ -272,15 +304,14 @@ expr head_reduce_mmv(expr const & e, environment const & env, name_set const * d
             if (!is_lambda(r))
                 break;
         }
-        if (i == num) {
-            return r;
-        } else {
+        if (i < num) {
             buffer<expr> args;
             args.push_back(r);
             for (; i < num; i++)
                 args.push_back(arg(e,i));
-            return mk_app(args.size(), args.data());
+            r = mk_app(args.size(), args.data());
         }
+        return r;
     } else if (is_let(e)) {
         return instantiate_free_var_mmv(let_body(e), 0, let_value(e));
     } else if (is_constant(e)) {
diff --git a/src/library/metavar.h b/src/library/metavar.h
index abc33ff1a2..ba8392c2d9 100644
--- a/src/library/metavar.h
+++ b/src/library/metavar.h
@@ -91,7 +91,7 @@ expr head_reduce_mmv(expr const & e, environment const & env, name_set const * d
    of the form (subst:i c v). The meaning of the expression is
    substitute free variable \c i in \c c with expression \c v.
 */
-bool is_subst(expr const & e, unsigned & i, expr & v);
+bool is_subst(expr const & e, expr & c, unsigned & i, expr & v);
 
 /**
     \brief Return true iff \c e is a delayed substitution expression.
@@ -103,7 +103,7 @@ bool is_subst(expr const & e);
     form (lift:s:n c). The meaning of the expression is lift the free
     variables >= \c s by \c n in \c c.
 */
-bool is_lift(expr const & e, unsigned & s, unsigned & n);
+bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n);
 
 /**
     \brief Return true iff \c e is a delayed lift expression.
@@ -115,7 +115,7 @@ bool is_lift(expr const & e);
     form (lower:s:n c). The meaning of the expression is lower the free
     variables >= \c s by \c n in \c c.
 */
-bool is_lower(expr const & e, unsigned & s, unsigned & n);
+bool is_lower(expr const & e, expr & c, unsigned & s, unsigned & n);
 
 /**
     \brief Return true iff \c e is a delayed lower expression.
@@ -128,5 +128,11 @@ bool is_lower(expr const & e);
     delayed lower expression.
 */
 bool is_meta(expr const & e);
-}
 
+/**
+   \brief Return nested metavar in \c e
+
+   \pre is_meta(e)
+*/
+expr get_metavar(expr const & e);
+}
diff --git a/src/library/metavar_env.cpp b/src/library/metavar_env.cpp
deleted file mode 100644
index c84e766d33..0000000000
--- a/src/library/metavar_env.cpp
+++ /dev/null
@@ -1,344 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <limits>
-#include <iomanip>
-#include "metavar_env.h"
-#include "name_set.h"
-#include "free_vars.h"
-#include "exception.h"
-#include "for_each.h"
-#include "replace.h"
-#include "printer.h"
-#include "beta.h"
-#include "flet.h"
-
-namespace lean {
-metavar_env::cell::cell(expr const & e, unsigned ctx_size, unsigned find):
-    m_expr(e),
-    m_ctx_size(ctx_size),
-    m_find(find),
-    m_rank(0),
-    m_state(state::Unprocessed) {
-}
-
-/** \brief Return true iff the cell midx is the root of its equivalence class */
-bool metavar_env::is_root(unsigned midx) const {
-    return m_cells[midx].m_find == midx;
-}
-
-/** \brief Return the root cell index of the equivalence class of \c midx */
-unsigned metavar_env::root_midx(unsigned midx) const {
-    while (!is_root(midx)) {
-        midx = m_cells[midx].m_find;
-    }
-    return midx;
-}
-
-/** \brief Return the root cell of the equivalence class of \c midx */
-metavar_env::cell & metavar_env::root_cell(unsigned midx) {
-    return m_cells[root_midx(midx)];
-}
-
-metavar_env::cell const & metavar_env::root_cell(unsigned midx) const {
-    return m_cells[root_midx(midx)];
-}
-
-/**
-   \brief Return the root cell of the equivalence class of the
-   metavariable \c m.
-
-   \pre is_metavar(m)
-*/
-metavar_env::cell & metavar_env::root_cell(expr const & m) {
-    lean_assert(is_metavar(m));
-    return root_cell(metavar_idx(m));
-}
-
-metavar_env::cell const & metavar_env::root_cell(expr const & m) const {
-    lean_assert(is_metavar(m));
-    return root_cell(metavar_idx(m));
-}
-
-/** \brief Auxiliary function for computing the new rank of an equivalence class. */
-unsigned metavar_env::new_rank(unsigned r1, unsigned r2) {
-    if (r1 == r2) return r1 + 1;
-    else return std::max(r1, r2);
-}
-
-[[noreturn]] void metavar_env::failed_to_unify() {
-    throw exception("failed to unify");
-}
-
-metavar_env::metavar_env(environment const & env, name_set const * available_defs, unsigned max_depth):
-    m_env(env) {
-    m_available_definitions = available_defs;
-    m_max_depth = max_depth;
-    m_depth     = 0;
-    m_interrupted = false;
-    m_modified    = false;
-}
-
-metavar_env::metavar_env(environment const & env, name_set const * available_defs):
-    metavar_env(env, available_defs, std::numeric_limits<unsigned>::max()) {
-}
-
-metavar_env::metavar_env(environment const & env):metavar_env(env, nullptr) {
-}
-
-expr metavar_env::mk_metavar(unsigned ctx_sz) {
-    m_modified    = true;
-    unsigned vidx = m_cells.size();
-    expr m = ::lean::mk_metavar(vidx);
-    m_cells.push_back(cell(m, ctx_sz, vidx));
-    return m;
-}
-
-bool metavar_env::is_assigned(expr const & m) const {
-    return !is_metavar(root_cell(m).m_expr);
-}
-
-expr metavar_env::root_at(expr const & e, unsigned ctx_size) const {
-    if (is_metavar(e)) {
-        cell const & c = root_cell(e);
-        if (is_metavar(c.m_expr)) {
-            return c.m_expr;
-        } else {
-            lean_assert(c.m_ctx_size <= ctx_size);
-            return lift_free_vars(c.m_expr, ctx_size - c.m_ctx_size);
-        }
-    } else {
-        return e;
-    }
-}
-
-/**
-   \brief Make sure that the metavariables in \c s can only access
-   ctx_size free variables.
-
-   \pre s does not contain assigned metavariables.
-*/
-void metavar_env::reduce_metavars_ctx_size(expr const & s, unsigned ctx_size) {
-    auto proc = [&](expr const & m, unsigned offset) {
-        if (is_metavar(m)) {
-            lean_assert(!is_assigned(m));
-            cell & mc = root_cell(m);
-            if (mc.m_ctx_size > ctx_size + offset)
-                mc.m_ctx_size = ctx_size + offset;
-        }
-    };
-    for_each_fn<decltype(proc)> visitor(proc);
-    visitor(s);
-}
-
-void metavar_env::assign(expr const & m, expr const & s, unsigned ctx_size) {
-    lean_assert(is_metavar(m));
-    lean_assert(!is_assigned(m));
-    if (m == s)
-        return;
-    m_modified = true;
-    cell & mc = root_cell(m);
-    lean_assert(is_metavar(mc.m_expr));
-    lean_assert(metavar_idx(mc.m_expr) == mc.m_find);
-    expr _s = instantiate_metavars(s, ctx_size);
-    if (is_metavar(_s)) {
-        // both are unassigned meta-variables...
-        lean_assert(!is_assigned(_s));
-        cell & sc = root_cell(_s);
-        lean_assert(is_metavar(sc.m_expr));
-        unsigned new_ctx_sz = std::min(mc.m_ctx_size, sc.m_ctx_size);
-        mc.m_ctx_size = new_ctx_sz;
-        sc.m_ctx_size = new_ctx_sz;
-        if (mc.m_rank > sc.m_rank) {
-            // we want to make mc the root of the equivalence class.
-            mc.m_rank    = new_rank(mc.m_rank, sc.m_rank);
-            sc.m_find    = mc.m_find;
-        } else {
-            // sc is the root
-            sc.m_rank  = new_rank(mc.m_rank, sc.m_rank);
-            mc.m_find  = sc.m_find;
-        }
-    } else {
-        lean_assert(!is_metavar(_s));
-        if (has_metavar(_s, mc.m_find)) {
-            failed_to_unify();
-        }
-        reduce_metavars_ctx_size(_s, mc.m_ctx_size);
-        if (ctx_size < mc.m_ctx_size) {
-            // mc is used in a context with more free variables.
-            // but s free variables are references to a smaller context.
-            // So, we must lift _s free variables.
-            _s = lift_free_vars(_s, mc.m_ctx_size - ctx_size);
-        } else if (ctx_size > mc.m_ctx_size) {
-            // _s must only contain free variables that are available
-            // in the context of mc
-            if (has_free_var(_s, 0, ctx_size - mc.m_ctx_size)) {
-                failed_to_unify();
-            }
-            _s = lower_free_vars(_s, ctx_size - mc.m_ctx_size);
-        }
-        mc.m_expr = _s;
-    }
-}
-
-expr metavar_env::instantiate_metavars(expr const & e, unsigned outer_offset) {
-    auto it = [&](expr const & c, unsigned offset) -> expr {
-        if (is_metavar(c)) {
-            unsigned midx = metavar_idx(c);
-            if (midx < m_cells.size()) {
-                cell & rc = root_cell(midx);
-                if (is_metavar(rc.m_expr)) {
-                    return rc.m_expr;
-                } else {
-                    switch (rc.m_state) {
-                    case state::Unprocessed:
-                        rc.m_state = state::Processing;
-                        rc.m_expr  = instantiate_metavars(rc.m_expr, rc.m_ctx_size);
-                        rc.m_state = state::Processed;
-                        lean_assert(rc.m_ctx_size <= offset + outer_offset);
-                        return lift_free_vars(rc.m_expr, offset + outer_offset - rc.m_ctx_size);
-                    case state::Processing: throw exception("cycle detected");
-                    case state::Processed:
-                        lean_assert(rc.m_ctx_size <= offset + outer_offset);
-                        return lift_free_vars(rc.m_expr, offset + outer_offset - rc.m_ctx_size);
-                    }
-                }
-            }
-        }
-        return c;
-    };
-
-    replace_fn<decltype(it)> proc(it);
-    return proc(e);
-}
-
-bool metavar_env::is_definition(expr const & e) {
-    if (is_constant(e)) {
-        name const & n = const_name(e);
-        if (m_available_definitions && m_available_definitions->find(n) == m_available_definitions->end()) {
-            return false;
-        } else {
-            object const & obj = m_env.find_object(const_name(e));
-            return obj && obj.is_definition() && !obj.is_opaque();
-        }
-    } else {
-        return false;
-    }
-}
-
-expr const & metavar_env::get_definition(expr const & e) {
-    lean_assert(is_definition(e));
-    return m_env.find_object(const_name(e)).get_value();
-}
-
-// Little hack for matching (?m #0) with t
-// TODO: implement some support for higher order unification.
-bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
-    if (is_app(e1) && is_metavar(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && length(ctx) > 0) {
-        return true;
-    } else {
-        return false;
-    }
-}
-
-// Little hack for matching (?m #0) with t
-// TODO: implement some support for higher order unification.
-void metavar_env::unify_simple_ho_match(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) {
-    unify(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), ctx_size, ctx);
-}
-
-/**
-   \brief Auxiliary function for unifying expressions \c e1 and
-   \c e2 when none of them are metavariables.
-*/
-void metavar_env::unify_core(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) {
-    check_interrupted(m_interrupted);
-    lean_assert(!is_metavar(e1));
-    lean_assert(!is_metavar(e2));
-    if (e1 == e2) {
-        return;
-    } else if (is_type(e1) && is_type(e2)) {
-        return; // ignoring type universe levels. We let the kernel check that
-    } else if (is_abstraction(e1) && is_abstraction(e2)) {
-        unify(abst_domain(e1), abst_domain(e2), ctx_size, ctx);
-        unify(abst_body(e1),   abst_body(e2), ctx_size+1, extend(ctx, abst_name(e1), abst_domain(e1)));
-    } else if (is_eq(e1) && is_eq(e2)) {
-        unify(eq_lhs(e1), eq_lhs(e2), ctx_size, ctx);
-        unify(eq_rhs(e1), eq_rhs(e2), ctx_size, ctx);
-    } else {
-        expr r1 = head_reduce(e1, m_env, m_available_definitions);
-        expr r2 = head_reduce(e2, m_env, m_available_definitions);
-        if (!is_eqp(e1, r1) || !is_eqp(e2, r2)) {
-            return unify(r1, r2, ctx_size, ctx);
-        } else if (is_app(e1) && is_app(e2) && num_args(e1) == num_args(e2)) {
-            unsigned num = num_args(e1);
-            for (unsigned i = 0; i < num; i++) {
-                unify(arg(e1, i), arg(e2, i), ctx_size, ctx);
-            }
-        } else if (is_simple_ho_match(e1, e2, ctx)) {
-            unify_simple_ho_match(e1, e2, ctx_size, ctx);
-        } else if (is_simple_ho_match(e2, e1, ctx)) {
-            unify_simple_ho_match(e2, e1, ctx_size, ctx);
-        } else {
-            failed_to_unify();
-        }
-    }
-}
-
-void metavar_env::unify(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) {
-    lean_assert(ctx_size == length(ctx));
-    flet<unsigned> l(m_depth, m_depth+1);
-    if (m_depth > m_max_depth)
-        throw exception("unifier maximum recursion depth exceeded");
-    expr const & r1 = root_at(e1, ctx_size);
-    expr const & r2 = root_at(e2, ctx_size);
-    if (is_metavar(r1)) {
-        assign(r1, r2, ctx_size);
-    } else {
-        if (is_metavar(r2)) {
-            assign(r2, r1, ctx_size);
-        } else {
-            unify_core(r1, r2, ctx_size, ctx);
-        }
-    }
-}
-
-void metavar_env::unify(expr const & e1, expr const & e2, context const & ctx) {
-    unify(e1, e2, length(ctx), ctx);
-}
-
-void metavar_env::set_interrupt(bool flag) {
-    m_interrupted = flag;
-}
-
-void metavar_env::clear() {
-    m_cells.clear();
-}
-
-void metavar_env::display(std::ostream & out) const {
-    for (unsigned i = 0; i < m_cells.size(); i++) {
-        out << "?" << i << " --> ";
-        out << "?" << std::left << std::setw(4) << m_cells[i].m_find
-            << std::left << std::setw(3) << m_cells[i].m_rank;
-        cell const & c = root_cell(i);
-        if (!is_metavar(c.m_expr))
-            out << c.m_expr;
-        else
-            out << "[unassigned]";
-        out << ", ctx_sz: " << c.m_ctx_size;
-        out << "\n";
-    }
-}
-
-bool metavar_env::check_invariant() const {
-    for (unsigned i = 0; i < m_cells.size(); i++) {
-        lean_assert(root_midx(i) == root_midx(m_cells[i].m_find));
-        lean_assert(m_cells[i].m_rank <= root_cell(i).m_rank);
-    }
-    return true;
-}
-}
-void print(lean::metavar_env const & env) { env.display(std::cout); }
diff --git a/src/library/metavar_env.h b/src/library/metavar_env.h
deleted file mode 100644
index 8e40cade8c..0000000000
--- a/src/library/metavar_env.h
+++ /dev/null
@@ -1,136 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <vector>
-#include "environment.h"
-#include "context.h"
-#include "name_set.h"
-#include "metavar.h"
-
-namespace lean {
-/**
-   \brief Metavariable environment. It is used for solving
-   unification constraints generated by expression elaborator
-   module. The elaborator compute implicit arguments that were not
-   provided by the user.
-*/
-class metavar_env {
-    enum class state { Unprocessed, Processing, Processed };
-    struct cell {
-        expr     m_expr;
-        unsigned m_ctx_size; // size of the context where the metavariable is defined
-        unsigned m_find;
-        unsigned m_rank;
-        state    m_state;
-        cell(expr const & e, unsigned ctx_size, unsigned find);
-    };
-    environment const & m_env;
-    std::vector<cell>   m_cells;
-    unsigned            m_max_depth;
-    unsigned            m_depth;
-    // If m_available_definitions != nullptr, then only the
-    // definitions in m_available_definitions are unfolded during unification.
-    name_set const *    m_available_definitions;
-    bool                m_modified;
-    volatile bool       m_interrupted;
-
-    bool is_root(unsigned midx) const;
-    unsigned root_midx(unsigned midx) const;
-    cell & root_cell(unsigned midx);
-    cell const & root_cell(unsigned midx) const;
-    cell & root_cell(expr const & m);
-    cell const & root_cell(expr const & m) const;
-    unsigned new_rank(unsigned r1, unsigned r2);
-    [[noreturn]] void failed_to_unify();
-    bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx);
-    void unify_simple_ho_match(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx);
-    void unify_core(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx);
-    void reduce_metavars_ctx_size(expr const & s, unsigned ctx_size);
-    void unify(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx);
-
-public:
-    metavar_env(environment const & env, name_set const * available_defs, unsigned max_depth);
-    metavar_env(environment const & env, name_set const * available_defs);
-    metavar_env(environment const & env);
-
-    /** \brief Create a new meta-variable for a context of size ctx_sz. */
-    expr mk_metavar(unsigned ctx_sz = 0);
-
-    /**
-       \brief Return true iff the given metavariable representative is
-       assigned.
-
-       \pre is_metavar(m)
-    */
-    bool is_assigned(expr const & m) const;
-
-    /**
-        \brief If the given expression is a metavariable, then return the root
-        of the equivalence class. Otherwise, return itself.
-
-        If the the metavariable was defined in smaller context, we lift the
-        free variables to match the size of the given context.
-    */
-    expr root_at(expr const & m, unsigned ctx_size) const;
-    expr root_at(expr const & m, context const & ctx) const {
-        return root_at(m, length(ctx));
-    }
-
-    /**
-       \brief Assign m <- s
-
-       \remark s is a term that occurs in a context of size \c
-       ctx_size. We need this information to adjust \c s to the
-       metavariable \c m, since \c m maybe was created in context of
-       different size, or was unified with another metavariable
-       created in a smaller context.
-
-       \pre is_metavar(m)
-
-    */
-    void assign(expr const & m, expr const & s, unsigned ctx_size);
-
-    /**
-       \brief Replace the metavariables occurring in \c e with the
-       substitutions in this metaenvironment.
-    */
-    expr instantiate_metavars(expr const & e, unsigned ctx_size = 0);
-
-    /**
-        \brief Return true iff the given expression is an available
-        definition.
-    */
-    bool is_definition(expr const & e);
-
-    /**
-       \brief Return the definition of the given expression in the
-       environment m_env.
-    */
-    expr const & get_definition(expr const & e);
-
-    /**
-       \brief Check if \c e1 and \c e2 can be unified in the given
-       metavariable environment. The environment may be updated with
-       new assignments. An exception is throw if \c e1 and \c e2 can't
-       be unified.
-    */
-    void unify(expr const & e1, expr const & e2, context const & ctx = context());
-
-    /**
-       \brief Clear/Reset the state.
-    */
-    void clear();
-
-    bool modified() const { return m_modified; }
-    void reset_modified() { m_modified = false; }
-
-    void set_interrupt(bool flag);
-
-    void display(std::ostream & out) const;
-    bool check_invariant() const;
-};
-}
diff --git a/src/library/printer.cpp b/src/library/printer.cpp
index 793de9ed99..a995deb835 100644
--- a/src/library/printer.cpp
+++ b/src/library/printer.cpp
@@ -54,21 +54,11 @@ struct print_expr_fn {
         print_child(eq_rhs(a), c);
     }
 
-    void print_app(expr const & a, context const & c) {
-        unsigned i, s, n;
-        expr v;
-        if (is_lower(a, s, n)) {
-            out() << "lower:" << s << ":" << n << " "; print_child(arg(a, 1), c);
-        } else if (is_lift(a, s, n)) {
-            out() << "lift:" << s << ":" << n << " "; print_child(arg(a, 1), c);
-        } else if (is_subst(a, i, v)) {
-            out() << "subst:" << i << " "; print_child(arg(a, 1), c); out() << " "; print_child(v, context());
-        } else {
-            print_child(arg(a, 0), c);
-            for (unsigned i = 1; i < num_args(a); i++) {
-                out() << " ";
-                print_child(arg(a, i), c);
-            }
+    void print_app(expr const & e, context const & c) {
+        print_child(arg(e, 0), c);
+        for (unsigned i = 1; i < num_args(e); i++) {
+            out() << " ";
+            print_child(arg(e, i), c);
         }
     }
 
@@ -80,58 +70,68 @@ struct print_expr_fn {
     }
 
     void print(expr const & a, context const & c) {
-        switch (a.kind()) {
-        case expr_kind::Var:
-            try {
-                out() << lookup(c, var_idx(a)).get_name();
-            } catch (exception & ex) {
-                out() << "#" << var_idx(a);
-            }
-            break;
-        case expr_kind::Constant:
-            if (is_metavar(a)) {
-                out() << "?M:" << metavar_idx(a);
-            } else {
-                out() << const_name(a);
-            }
-            break;
-        case expr_kind::App:
-            print_app(a, c);
-            break;
-        case expr_kind::Eq:
-            print_eq(a, c);
-            break;
-        case expr_kind::Lambda:
-            out() << "fun " << abst_name(a) << " : ";
-            print_child(abst_domain(a), c);
-            out() << ", ";
-            print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a)));
-            break;
-        case expr_kind::Pi:
-            if (!is_arrow(a)) {
-                out() << "Pi " << abst_name(a) << " : ";
+        unsigned i, s, n;
+        expr v, ch;
+        if (is_lower(a, ch, s, n)) {
+            out() << "lower:" << s << ":" << n << " "; print_child(ch, c);
+        } else if (is_lift(a, ch, s, n)) {
+            out() << "lift:" << s << ":" << n << " "; print_child(ch, c);
+        } else if (is_subst(a, ch, i, v)) {
+            out() << "subst:" << i << " "; print_child(ch, c); out() << " "; print_child(v, context());
+        } else {
+            switch (a.kind()) {
+            case expr_kind::Var:
+                try {
+                    out() << lookup(c, var_idx(a)).get_name();
+                } catch (exception & ex) {
+                    out() << "#" << var_idx(a);
+                }
+                break;
+            case expr_kind::Constant:
+                if (is_metavar(a)) {
+                    out() << "?M:" << metavar_idx(a);
+                } else {
+                    out() << const_name(a);
+                }
+                break;
+            case expr_kind::App:
+                print_app(a, c);
+                break;
+            case expr_kind::Eq:
+                print_eq(a, c);
+                break;
+            case expr_kind::Lambda:
+                out() << "fun " << abst_name(a) << " : ";
                 print_child(abst_domain(a), c);
                 out() << ", ";
                 print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a)));
                 break;
-            } else {
-                print_child(abst_domain(a), c);
-                out() << " -> ";
-                print_arrow_body(abst_body(a), extend(c, abst_name(a), abst_domain(a)));
+            case expr_kind::Pi:
+                if (!is_arrow(a)) {
+                    out() << "Pi " << abst_name(a) << " : ";
+                    print_child(abst_domain(a), c);
+                    out() << ", ";
+                    print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a)));
+                    break;
+                } else {
+                    print_child(abst_domain(a), c);
+                    out() << " -> ";
+                    print_arrow_body(abst_body(a), extend(c, abst_name(a), abst_domain(a)));
+                }
+                break;
+            case expr_kind::Let:
+                out() << "let " << let_name(a) << " := ";
+                print(let_value(a), c);
+                out() << " in ";
+                print_child(let_body(a), extend(c, let_name(a), let_value(a)));
+                break;
+            case expr_kind::Type:
+                print_type(a);
+                break;
+            case expr_kind::Value:
+                print_value(a);
+                break;
             }
-            break;
-        case expr_kind::Let:
-            out() << "let " << let_name(a) << " := ";
-            print(let_value(a), c);
-            out() << " in ";
-            print_child(let_body(a), extend(c, let_name(a), let_value(a)));
-            break;
-        case expr_kind::Type:
-            print_type(a);
-            break;
-        case expr_kind::Value:
-            print_value(a);
-            break;
         }
     }
 
diff --git a/src/tests/library/implicit_args.cpp b/src/tests/library/implicit_args.cpp
index 5c1c68e2cf..83f33bc0f6 100644
--- a/src/tests/library/implicit_args.cpp
+++ b/src/tests/library/implicit_args.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "test.h"
-#include "metavar_env.h"
+#include "metavar.h"
 #include "elaborator.h"
 #include "free_vars.h"
 #include "printer.h"
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "basic_thms.h"
 #include "type_check.h"
 #include "kernel_exception.h"
+#include "elaborator_exception.h"
 using namespace lean;
 
 static name g_placeholder_name("_");
@@ -35,36 +36,34 @@ bool has_placeholder(expr const & e) {
     return occurs(mk_placholder(), e);
 }
 
-std::ostream & operator<<(std::ostream & out, metavar_env const & uf) { uf.display(out); return out; }
-
 /**
    \brief Auxiliary function for #replace_placeholders_with_metavars
 */
-static expr replace(expr const & e, context const & ctx, metavar_env & menv) {
+static expr replace(expr const & e, context const & ctx, elaborator & elb) {
     switch (e.kind()) {
     case expr_kind::Constant:
         if (is_placeholder(e)) {
-            return menv.mk_metavar(length(ctx));
+            return elb.mk_metavar();
         } else {
             return e;
         }
     case expr_kind::Var: case expr_kind::Type: case expr_kind::Value:
         return e;
     case expr_kind::App:
-        return update_app(e, [&](expr const & c) { return replace(c, ctx, menv); });
+        return update_app(e, [&](expr const & c) { return replace(c, ctx, elb); });
     case expr_kind::Eq:
-        return update_eq(e, [&](expr const & l, expr const & r) { return mk_pair(replace(l, ctx, menv), replace(r, ctx, menv)); });
+        return update_eq(e, [&](expr const & l, expr const & r) { return mk_pair(replace(l, ctx, elb), replace(r, ctx, elb)); });
     case expr_kind::Lambda:
     case expr_kind::Pi:
         return update_abst(e, [&](expr const & d, expr const & b) {
-                expr new_d = replace(d, ctx, menv);
-                expr new_b = replace(b, extend(ctx, abst_name(e), new_d), menv);
+                expr new_d = replace(d, ctx, elb);
+                expr new_b = replace(b, extend(ctx, abst_name(e), new_d), elb);
                 return mk_pair(new_d, new_b);
             });
     case expr_kind::Let:
         return update_let(e, [&](expr const & v, expr const & b) {
-                expr new_v = replace(v, ctx, menv);
-                expr new_b = replace(b, extend(ctx, abst_name(e), expr(), new_v), menv);
+                expr new_v = replace(v, ctx, elb);
+                expr new_b = replace(b, extend(ctx, let_name(e), expr(), new_v), elb);
                 return mk_pair(new_v, new_b);
             });
     }
@@ -75,27 +74,47 @@ static expr replace(expr const & e, context const & ctx, metavar_env & menv) {
 /**
    \brief Replace placeholders with fresh meta-variables.
 */
-expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv) {
-    return replace(e, context(), menv);
+expr replace_placeholders_with_metavars(expr const & e, elaborator & elb) {
+    return replace(e, context(), elb);
 }
 
 expr elaborate(expr const & e, environment const & env) {
     elaborator elb(env);
-    expr new_e = replace_placeholders_with_metavars(e, elb.menv());
+    expr new_e = replace_placeholders_with_metavars(e, elb);
     return elb(new_e);
 }
 
 // Check elaborator success
 static void success(expr const & e, expr const & expected, environment const & env) {
-    std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n";
+    std::cout << "\n" << e << "\n------>\n";
+    try {
+        std::cout << elaborate(e, env) << "\n";
+    } catch (unification_app_mismatch_exception & ex) {
+        std::cout << "Error at argumet " << ex.get_arg_pos() << " of " << mk_pair(ex.get_expr(), ex.get_context()) << "\n";
+    } catch (unification_type_mismatch_exception & ex) {
+        std::cout << "Error at " << mk_pair(ex.get_expr(), ex.get_context()) << " " << ex.what() << "\n";
+        std::cout << "Elaborator:\n"; ex.get_elaborator().display(std::cout); std::cout << "-----------------\n";
+    }
     lean_assert(elaborate(e, env) == expected);
-    std::cout << infer_type(elaborate(e, env), env) << "\n";
+    try {
+        std::cout << infer_type(elaborate(e, env), env) << "\n";
+    } catch (app_type_mismatch_exception & ex) {
+        context const & ctx = ex.get_context();
+        std::cout << "Application type mismatch at argument " << ex.get_arg_pos() << "\n"
+                  << "  " << mk_pair(ex.get_application(), ctx) << "\n"
+                  << "expected type\n"
+                  << "  " << mk_pair(ex.get_expected_type(), ctx) << "\n"
+                  << "given type\n"
+                  << "  " << mk_pair(ex.get_given_type(), ctx) << "\n";
+        lean_unreachable();
+    }
 }
 
 // Check elaborator failure
 static void fails(expr const & e, environment const & env) {
     try {
-        elaborate(e, env);
+        expr new_e = elaborate(e, env);
+        std::cout << "new_e: " << new_e << std::endl;
         lean_unreachable();
     } catch (exception &) {
     }
@@ -123,7 +142,7 @@ static void tst1() {
     expr _ = mk_placholder();
     expr f = Const("f");
     success(F(_,_,f), F(Nat, Real, f), env);
-    fails(F(_,Bool,f), env);
+    // fails(F(_,Bool,f), env);
     success(F(_,_,Fun({a, Nat},a)), F(Nat,Nat,Fun({a,Nat},a)), env);
 }
 
@@ -389,6 +408,45 @@ void tst12() {
             env);
 }
 
+void tst13() {
+    environment env = mk_toplevel();
+    expr A  = Const("A");
+    expr h  = Const("h");
+    expr f  = Const("f");
+    expr a  = Const("a");
+    expr _  = mk_placholder();
+    env.add_var("h", Pi({A, Type()}, A) >> Bool);
+    success(Fun({{f, Pi({A, Type()}, _)}, {a, Bool}}, h(f)),
+            Fun({{f, Pi({A, Type()}, A)}, {a, Bool}}, h(f)),
+            env);
+}
+
+void tst14() {
+    environment env = mk_toplevel();
+    expr R  = Const("R");
+    expr A  = Const("A");
+    expr r  = Const("r");
+    expr eq = Const("eq");
+    expr f  = Const("f");
+    expr g  = Const("g");
+    expr h  = Const("h");
+    expr D  = Const("D");
+    expr _  = mk_placholder();
+    env.add_var("R", Type() >> Bool);
+    env.add_var("r", Pi({A, Type()},R(A)));
+    env.add_var("h", Pi({A, Type()}, R(A)) >> Bool);
+    env.add_var("eq", Pi({A, Type(level()+1)}, A >> (A >> Bool)));
+    success(Let({{f, Fun({A, Type()}, r(_))},
+                 {g, Fun({A, Type()}, r(_))},
+                 {D, Fun({A, Type()}, eq(_, f(A), g(_)))}},
+                h(f)),
+            Let({{f, Fun({A, Type()}, r(A))},
+                 {g, Fun({A, Type()}, r(A))},
+                 {D, Fun({A, Type()}, eq(R(A), f(A), g(A)))}},
+                h(f)),
+            env);
+}
+
 int main() {
     tst1();
     tst2();
@@ -402,5 +460,7 @@ int main() {
     tst10();
     tst11();
     tst12();
+    tst13();
+    tst14();
     return has_violations() ? 1 : 0;
 }