diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 7c0157e1e..7fa585218 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -260,9 +260,9 @@ public:
     macro():m_rc(0) {}
     virtual ~macro() {}
     virtual name get_name() const = 0;
-    virtual expr get_type(buffer<expr> const & arg_types) const = 0;
-    virtual expr expand1(buffer<expr> const & args) const = 0;
-    virtual expr expand(buffer<expr> const & args) const = 0;
+    virtual expr get_type(unsigned num_args, expr const * arg_types) const = 0;
+    virtual optional<expr> expand1(unsigned num_args, expr const * args) const = 0;
+    virtual optional<expr> expand(unsigned num_args, expr const * args) const = 0;
     virtual int push_lua(lua_State * L) const;
     virtual bool operator==(macro const & other) const;
     bool operator<(macro const & other) const;
@@ -340,6 +340,7 @@ template<typename T> expr mk_app(T const & args) { return mk_app(args.size(), ar
        expr mk_rev_app(expr const & f, unsigned num_args, expr const * args);
        expr mk_rev_app(unsigned num_args, expr const * args);
 template<typename T> expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); }
+template<typename T> expr mk_rev_app(expr const & f, T const & args) { return mk_rev_app(f, args.size(), args.data()); }
 inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e) { return expr(new expr_binder(k, n, t, e)); }
 inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); }
 inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index f6e235048..f8d1d95d7 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -4,638 +4,157 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/type_checker.h"
-
-
-
-#if 0
-#include "util/freset.h"
-#include "util/flet.h"
 #include "util/interrupt.h"
-#include "kernel/environment.h"
 #include "kernel/type_checker.h"
 #include "kernel/expr_maps.h"
-#include "kernel/kernel_exception.h"
-#include "kernel/normalizer.h"
 #include "kernel/instantiate.h"
-#include "kernel/free_vars.h"
-#include "kernel/error_msgs.h"
-#include "kernel/constraint.h"
-#include "kernel/metavar.h"
+#include "kernel/max_sharing.h"
 
 namespace lean {
-expr pi_body_at(expr const & pi, expr const & a) {
-    lean_assert(is_pi(pi));
-    if (closed(binder_body(pi)))
-        return binder_body(pi);
-    else
-        return instantiate(binder_body(pi), a);
-}
 
-/** \brief Auxiliary functional object used to implement infer_type. */
-class type_checker::imp {
-    typedef expr_map<expr> cache;
+/** \brief Auxiliary functional object used to implement type checker. */
+struct type_checker::imp {
+    environment           m_env;
+    name_generator        m_gen;
+    constraint_handler &  m_chandler;
+    bool                  m_memoize;
+    name_set              m_extra_opaque;
+    max_sharing_fn        m_sharing;
+    expr_map<expr>        m_cache;
+    expr_map<expr>        m_whnf_cache;
 
-    ro_environment::weak_ref  m_env;
-    normalizer                m_normalizer;
-    cache                     m_cache;
-    name_generator *          m_name_gen;
-    constraints               m_constraints; // constraints generated so far
-    bool                      m_infer_only;
+    imp(environment const & env, name_generator const & g, constraint_handler & h, bool memoize, name_set const & extra_opaque):
+        m_env(env), m_gen(g), m_chandler(h), m_memoize(memoize), m_extra_opaque(extra_opaque) {}
 
-    ro_environment env() const { return ro_environment(m_env); }
-    expr normalize(expr const & e) { return m_normalizer(e); }
-
-    level mk_meta_univ() {
-        return ::lean::mk_meta_univ(m_name_gen->next());
-    }
-
-    void add_eq_constraint(expr const & t, expr const & s, justification const & j) {
-        m_constraints = add(m_constraints, mk_eq_cnstr(t, s, j));
-    }
-
-    expr check_sort(expr const & e, expr const & s) {
-        if (is_sort(e))
-            return e;
-        expr u = normalize(e);
-        if (is_sort(u))
-            return u;
-        if (has_metavar(u)) {
-            expr r = mk_sort(mk_meta_univ());
-            justification j = mk_justification(s, [=](formatter const & fmt, options const & o, substitution const & s) {
-                    return pp_type_expected(fmt, o, s.instantiate_metavars_wo_jst(e));
-                });
-            add_eq_constraint(e, r, j);
-            return r;
-        }
-        throw_kernel_exception(env(), s, [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, o, e); });
-    }
-
-    expr check_pi(expr const & e, expr const & s, context const & ctx) {
-        if (is_pi(e))
-            return e;
-        expr u = normalize(e);
-        if (is_pi(u))
-            return u;
-        if (has_metavar(u)) {
-            // Create two fresh variables A and B,
-            // and assign r == (Pi(x : A), B)
-            expr A   = m_menv->mk_metavar(ctx);
-            expr B   = m_menv->mk_metavar(extend(ctx, g_x_name, A));
-            expr p   = mk_pi(g_x_name, A, B);
-            justification jst = mk_function_expected_justification(ctx, s);
-            m_uc->push_back(mk_eq_constraint(ctx, e, p, jst));
-            return p;
-        }
-        throw function_expected_exception(env(), ctx, s);
-    }
-};
-
-static name g_x_name("x");
-/** \brief Auxiliary functional object used to implement infer_type. */
-class type_checker::imp {
-    // TODO(Leo): we should consider merging check_pi and check_sigma.
-    // They are very similar
-    expr check_sigma(expr const & e, expr const & s, context const & ctx) {
-        if (is_sigma(e))
-            return e;
-        expr r = normalize(e, ctx, false);
-        if (is_sigma(r))
-            return r;
-        if (has_metavar(r) && m_menv && m_uc) {
-            // Create two fresh variables A and B,
-            // and assign r == (Pi(x : A), B)
-            expr A   = m_menv->mk_metavar(ctx);
-            expr B   = m_menv->mk_metavar(extend(ctx, g_x_name, A));
-            expr p   = mk_sigma(g_x_name, A, B);
-            justification jst = mk_pair_expected_justification(ctx, s);
-            m_uc->push_back(mk_eq_constraint(ctx, e, p, jst));
-            return p;
-        }
-        throw pair_expected_exception(env(), ctx, s);
-    }
-
-    /**
-       \brief Given \c t (a Pi term), this method returns the body (aka range)
-       of the function space for the element e in the domain of the Pi.
-    */
-    expr get_pi_body(expr const & t, expr const & e) {
-        lean_assert(is_pi(t));
-        if (is_arrow(t))
-            return lower_free_vars(abst_body(t), 1, 1);
+    expr max_sharing(expr const & e) { return m_memoize ? m_sharing(e) : e; }
+    expr instantiate(expr const & e, unsigned n, expr const * s) { return max_sharing(lean::instantiate(e, n, s)); }
+    expr instantiate(expr const & e, expr const & s) { return max_sharing(lean::instantiate(e, s)); }
+    expr mk_rev_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_rev_app(f, num, args)); }
+    optional<expr> expand_macro(expr const & m, unsigned num, expr const * args) {
+        lean_assert(is_macro(m));
+        if (auto new_m = to_macro(m).expand(num, args))
+            return some_expr(max_sharing(*new_m));
         else
-            return instantiate(abst_body(t), e);
+            return none_expr();
+    }
+    expr instantiate_params(expr const & e, param_names const & ps, levels const & ls) {
+        return max_sharing(lean::instantiate_params(e, ps, ls));
     }
 
-    expr get_range(expr t, expr const & e, context const & ctx) {
-        unsigned num = num_args(e);
-        for (unsigned i = 1; i < num; i++) {
-            expr const & a = arg(e, i);
-            if (is_pi(t)) {
-                t = get_pi_body(t, a);
-            } else {
-                t = normalize(t, ctx, false);
-                if (is_pi(t)) {
-                    t = get_pi_body(t, a);
-                } else if (has_metavar(t) && m_menv && m_uc) {
-                    // Create two fresh variables A and B,
-                    // and assign r == (Pi(x : A), B)
-                    expr A   = m_menv->mk_metavar(ctx);
-                    expr B   = m_menv->mk_metavar(extend(ctx, g_x_name, A));
-                    expr p   = mk_pi(g_x_name, A, B);
-                    justification jst = mk_function_expected_justification(ctx, e);
-                    m_uc->push_back(mk_eq_constraint(ctx, t, p, jst));
-                    t        = get_pi_body(p, a);
-                } else {
-                    throw function_expected_exception(env(), ctx, e);
-                }
-            }
-        }
-        return t;
+    bool check_memoized(expr const & e) const {
+        return !m_memoize || m_sharing.already_processed(e);
     }
 
-    expr save_result(expr const & e, expr const & r, bool shared) {
-        if (shared)
-            m_cache[e] = r;
-        return r;
-    }
+    /** \brief Weak head normal form core procedure. It does not perform delta reduction nor extensions. */
+    expr whnf_core(expr const & e) {
+        check_system("whnf");
+        lean_assert(check_memoized(e));
 
-    expr infer_type_core(expr const & e, context const & ctx) {
-        check_system("type checker");
-        // cheap cases, we do not cache results
+        // handle easy cases
         switch (e.kind()) {
-        case expr_kind::MetaVar:
-            if (m_menv) {
-                if (m_menv->is_assigned(e))
-                    return infer_type_core(*(m_menv->get_subst(e)), ctx);
-                else
-                    return m_menv->get_type(e);
-            } else {
-                throw unexpected_metavar_occurrence(env(), e);
-            }
-        case expr_kind::Constant: {
-            if (const_type(e)) {
-                return *const_type(e);
-            } else {
-                object const & obj = env()->get_object(const_name(e));
-                if (obj.has_type())
-                    return obj.get_type();
-                else
-                    throw has_no_type_exception(env(), e);
-            }
+        case expr_kind::Var:    case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+        case expr_kind::Lambda: case expr_kind::Pi:   case expr_kind::Constant:
+            return e;
+        case expr_kind::Macro:  case expr_kind::Let:  case expr_kind::App:
             break;
         }
-        case expr_kind::Var: {
-            auto const & entry = lookup(ctx, var_idx(e));
-            if (entry.get_domain())
-                return lift_free_vars(*(entry.get_domain()), var_idx(e) + 1);
-            // Remark: the case where ce.get_domain() is not
-            // available is not considered cheap.
-            break;
-        }
-        case expr_kind::Value:
-            if (m_infer_only) {
-                return to_value(e).get_type();
-            } else {
-                name const & n = to_value(e).get_name();
-                object obj = env()->get_object(n);
-                if ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e))) {
-                    return to_value(e).get_type();
-                } else {
-                    throw invalid_builtin_value_reference(env(), e);
-                }
-            }
-        case expr_kind::Type:
-            return mk_type(ty_level(e) + 1);
-        case expr_kind::App: case expr_kind::Lambda:
-        case expr_kind::Pi:  case expr_kind::Let:
-        case expr_kind::Sigma: case expr_kind::Proj:
-        case expr_kind::Pair:
-            break; // expensive cases
-        }
 
-        bool shared = false;
-        if (is_shared(e)) {
-            shared = true;
-            auto it = m_cache.find(e);
-            if (it != m_cache.end())
+        // check cache
+        if (m_memoize) {
+            auto it = m_whnf_cache.find(e);
+            if (it != m_whnf_cache.end())
                 return it->second;
         }
 
+        // do the actual work
         expr r;
         switch (e.kind()) {
-        case expr_kind::MetaVar: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
-            lean_unreachable(); // LCOV_EXCL_LINE;
-        case expr_kind::Var: {
-            unsigned i = var_idx(e);
-            auto p = lookup_ext(ctx, i);
-            context_entry const & def = p.first;
-            context const & def_ctx   = p.second;
-            lean_assert(ctx.size() > def_ctx.size());
-            lean_assert(!def.get_domain()); // was handled as cheap
-            optional<expr> const & b = def.get_body();
-            lean_assert(b);
-            expr t = infer_type_core(*b, def_ctx);
-            r = lift_free_vars(t, var_idx(e) + 1);
+        case expr_kind::Var:    case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+        case expr_kind::Lambda: case expr_kind::Pi:   case expr_kind::Constant:
+            lean_unreachable(); // LCOV_EXCL_LINE
+        case expr_kind::Macro:
+            if (auto m = expand_macro(e, 0, 0))
+                r = whnf_core(*m);
+            else
+                r = e;
             break;
-        }
-        case expr_kind::App:
-            if (m_infer_only) {
-                expr const & f = arg(e, 0);
-                expr f_t = infer_type_core(f, ctx);
-                r = get_range(f_t, e, ctx);
-            } else {
-                unsigned num = num_args(e);
-                lean_assert(num >= 2);
-                buffer<expr> arg_types;
-                for (unsigned i = 0; i < num; i++) {
-                    arg_types.push_back(infer_type_core(arg(e, i), ctx));
+        case expr_kind::Let:
+            r = whnf_core(instantiate(let_body(e), let_value(e)));
+            break;
+        case expr_kind::App: {
+            buffer<expr> args;
+            expr const * it = &e;
+            while (is_app(*it)) {
+                args.push_back(app_arg(*it));
+                it = &(app_fn(*it));
+            }
+            expr f = whnf_core(*it);
+            if (is_lambda(f)) {
+                unsigned m = 1;
+                unsigned num_args = args.size();
+                while (is_lambda(binder_body(f)) && m < num_args) {
+                    f = binder_body(f);
+                    m++;
                 }
-                expr f_t     = check_pi(arg_types[0], e, ctx);
-                unsigned i   = 1;
-                while (true) {
-                    expr const & c   = arg(e, i);
-                    expr const & c_t = arg_types[i];
-                    // thunk for creating justification object if needed
-                    auto mk_justification = [&](){ return mk_app_type_match_justification(ctx, e, i); };
-                    if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_justification))
-                        throw app_type_mismatch_exception(env(), ctx, e, i, arg_types.size(), arg_types.data());
-                    f_t = pi_body_at(f_t, c);
-                    i++;
-                    if (i == num) {
-                        r = f_t;
-                        break;
-                    }
-                    f_t = check_pi(f_t, e, ctx);
-                }
-            }
-            break;
-        case expr_kind::Pair:
-            if (m_infer_only) {
-                r = pair_type(e);
-            } else {
-                expr const & t = pair_type(e);
-                expr sig       = check_sigma(t, t, ctx);
-                expr f_t       = infer_type_core(pair_first(e), ctx);
-                expr s_t       = infer_type_core(pair_second(e), ctx);
-                auto mk_fst_justification = [&]() { return mk_pair_type_match_justification(ctx, e, true); };
-                if (!is_convertible(f_t, abst_domain(sig), ctx, mk_fst_justification))
-                    throw pair_type_mismatch_exception(env(), ctx, e, true, f_t, sig);
-                auto mk_snd_justification = [&]() { return mk_pair_type_match_justification(ctx, e, false); };
-                expr expected  = instantiate(abst_body(sig), pair_first(e));
-                if (!is_convertible(s_t, expected, ctx, mk_snd_justification)) {
-                    throw pair_type_mismatch_exception(env(), ctx, e, false, s_t, sig);
-                }
-                r = sig;
-            }
-            break;
-        case expr_kind::Proj: {
-            expr t = check_sigma(infer_type_core(proj_arg(e), ctx), e, ctx);
-            if (proj_first(e)) {
-                r = abst_domain(t);
-            } else {
-                expr const & b = abst_body(t);
-                if (closed(b))
-                    r = b;
-                else
-                    r = instantiate(b, mk_proj1(proj_arg(e)));
-            }
-            break;
-        }
-        case expr_kind::Lambda:
-            if (!m_infer_only) {
-                expr d = infer_type_core(abst_domain(e), ctx);
-                check_type(d, abst_domain(e), ctx);
-            }
-            {
-                freset<cache> reset(m_cache);
-                r = mk_pi(abst_name(e), abst_domain(e), infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))));
-            }
-            break;
-        case expr_kind::Sigma: case expr_kind::Pi: {
-            expr t1  = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx);
-            if (is_bool(t1))
-                t1 = Type();
-            expr t2;
-            context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
-            {
-                freset<cache> reset(m_cache);
-                t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx);
-            }
-            if (is_bool(t2)) {
-                if (is_pi(e)) {
-                    r = Bool;
+                lean_assert(m <= num_args);
+                r = whnf_core(mk_rev_app(instantiate(binder_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()));
+                break;
+            } else if (is_macro(f)) {
+                auto m = expand_macro(f, args.size(), args.data());
+                if (m) {
+                    r = whnf_core(*m);
                     break;
-                } else {
-                    t2 = Type();
                 }
             }
-            if (is_type(t1) && is_type(t2)) {
-                r = mk_type(max(ty_level(t1), ty_level(t2)));
-            } else {
-                lean_assert(m_uc);
-                justification jst = mk_max_type_justification(ctx, e);
-                r = m_menv->mk_metavar(ctx);
-                m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), t2, r, jst));
-            }
-            break;
-        }
-        case expr_kind::Let: {
-            optional<expr> lt;
-            if (m_infer_only) {
-                lt = let_type(e);
-            } else {
-                if (let_type(e)) {
-                    expr value_ty = infer_type_core(let_value(e), ctx);
-                    expr ty       = infer_type_core(*let_type(e), ctx);
-                    check_type(ty, *let_type(e), ctx); // check if it is really a type
-                    // thunk for creating justification object if needed
-                    auto mk_justification = [&](){ return mk_def_type_match_justification(ctx, let_name(e), let_value(e)); };
-                    if (!is_convertible(value_ty, *let_type(e), ctx, mk_justification))
-                        throw def_type_mismatch_exception(env(), ctx, let_name(e), *let_type(e), let_value(e), value_ty);
-                    lt = let_type(e);
-                } else {
-                    lt = infer_type_core(let_value(e), ctx);
-                }
-            }
-            {
-                freset<cache> reset(m_cache);
-                expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
-                r = instantiate(t, let_value(e));
-            }
+            r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data());
             break;
         }}
-        return save_result(e, r, shared);
+
+        if (m_memoize)
+            m_whnf_cache.insert(mk_pair(e, r));
+        return r;
     }
 
-    bool is_convertible_core(expr const & given, expr const & expected) {
-        if (given == expected) {
-            return true;
-        } else {
-            expr const * g = &given;
-            expr const * e = &expected;
-            while (true) {
-                if (is_type(*e) && is_type(*g)) {
-                    if (env()->is_ge(ty_level(*e), ty_level(*g)))
-                        return true;
-                }
-
-                if (is_type(*e) && *g == mk_bool_type())
-                    return true;
-
-                if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
-                    g = &abst_body(*g);
-                    e = &abst_body(*e);
-                } else {
-                    return false;
-                }
+    /** \brief Expand \c e if it is non-opaque constant with weight >= w */
+    expr unfold_name_core(expr e, unsigned w) {
+        if (is_constant(e)) {
+            if (auto d = m_env.find(const_name(e))) {
+                if (d->is_definition() && !d->is_opaque() && d->get_weight() >= w && !m_extra_opaque.contains(d->get_name()))
+                    return unfold_name_core(instantiate_params(d->get_value(), d->get_params(), const_level_params(e)), w);
             }
         }
+        return e;
     }
 
-    template<typename MkJustification>
-    bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkJustification const & mk_justification) {
-        if (is_convertible_core(given, expected))
-            return true;
-        expr new_given    = normalize(given, ctx, false);
-        expr new_expected = normalize(expected, ctx, false);
-        if (is_convertible_core(new_given, new_expected))
-            return true;
-        if (m_menv && m_uc && (has_metavar(new_given) || has_metavar(new_expected))) {
-            m_uc->push_back(mk_convertible_constraint(ctx, given, expected, mk_justification()));
-            return true;
-        }
-        return false;
-    }
+    /**
+       \brief Expand constants and application where the function is a constant.
 
-    void set_ctx(context const & ctx) {
-        if (!is_eqp(m_ctx, ctx)) {
-            clear();
-            m_ctx = ctx;
+       The unfolding is only performend if the constant corresponds to
+       a non-opaque definition with weight >= w, and it is not in the
+       set of extra_opaque constants.
+    */
+    expr unfold_names(expr const & e, unsigned w) {
+        if (is_app(e)) {
+            expr const * it = &e;
+            while (is_app(*it)) {
+                it = &(app_fn(*it));
+            }
+            expr f = unfold_name_core(*it, w);
+            if (is_eqp(f, *it)) {
+                return e;
+            } else {
+                buffer<expr> args;
+                expr const * it = &e;
+                while (is_app(*it)) {
+                    args.push_back(app_arg(*it));
+                    it = &(app_fn(*it));
+                }
+                return mk_rev_app(f, args.size(), args.data());
+            }
+        } else {
+            return unfold_name_core(e, w);
         }
     }
 
-    void update_menv(optional<metavar_env> const & menv) {
-        if (m_menv.update(menv))
-            clear_cache();
-    }
-
-    struct set_infer_only {
-        imp & m_ref;
-        bool  m_old_infer_only;
-        set_infer_only(imp & r, bool flag):m_ref(r), m_old_infer_only(m_ref.m_infer_only) {
-            if (m_ref.m_infer_only != flag)
-                m_ref.clear_cache();
-            m_ref.m_infer_only = flag;
-        }
-        ~set_infer_only() {
-            if (m_ref.m_infer_only != m_old_infer_only)
-                m_ref.clear_cache();
-            m_ref.m_infer_only = m_old_infer_only;
-        }
-    };
-
-public:
-    imp(ro_environment const & env, bool infer_only):
-        m_env(env),
-        m_normalizer(env) {
-        m_uc              = nullptr;
-        m_infer_only      = infer_only;
-    }
-
-    expr infer_check(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc,
-                     bool infer_only) {
-        clear_cache(); // temp hack
-        set_infer_only set(*this, infer_only);
-        set_ctx(ctx);
-        update_menv(menv);
-        flet<unification_constraints*> set_uc(m_uc, uc);
-        return infer_type_core(e, ctx);
-    }
-
-    expr infer_type(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
-        return infer_check(e, ctx, menv, uc, true);
-    }
-
-    expr check(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
-        return infer_check(e, ctx, menv, uc, false);
-    }
-
-    bool is_convertible(expr const & t1, expr const & t2, context const & ctx, optional<metavar_env> const & menv) {
-        set_ctx(ctx);
-        update_menv(menv);
-        auto mk_justification = [](){
-            lean_unreachable(); return justification(); // LCOV_EXCL_LINE
-        };
-        return is_convertible(t1, t2, ctx, mk_justification);
-    }
-
-    bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx, optional<metavar_env> const & menv) {
-        set_ctx(ctx);
-        update_menv(menv);
-        if (t1 == t2)
-            return true;
-        expr new_t1 = normalize(t1, ctx, false);
-        expr new_t2 = normalize(t2, ctx, false);
-        return new_t1 == new_t2;
-    }
-
-    void check_type(expr const & e, context const & ctx) {
-        set_ctx(ctx);
-        update_menv(none_menv());
-        expr t = infer_type_core(e, ctx);
-        check_type(t, e, ctx);
-    }
-
-    bool is_proposition(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
-        // Catch easy cases
-        switch (e.kind()) {
-        case expr_kind::Lambda: case expr_kind::Type:
-            return false;
-        case expr_kind::Pi:
-            return is_proposition(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)), menv);
-        default:
-            break;
-        }
-        expr t = infer_type(e, ctx, menv, nullptr);
-        if (is_bool(t))
-            return true;
-        else
-            return is_bool(normalize(t, ctx, false));
-    }
-
-    expr ensure_pi(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
-        set_ctx(ctx);
-        update_menv(menv);
-        try {
-            return check_pi(e, expr(), ctx);
-        } catch (exception &) {
-            throw exception("internal bug, expression is not a Pi");
-        }
-    }
-
-    expr ensure_sigma(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
-        set_ctx(ctx);
-        update_menv(menv);
-        try {
-            return check_sigma(e, expr(), ctx);
-        } catch (exception &) {
-            throw exception("internal bug, expression is not a Sigma");
-        }
-    }
-
-    void clear_cache() {
-        m_cache.clear();
-        m_normalizer.clear();
-    }
-
-    void clear() {
-        clear_cache();
-        m_menv.clear();
-        m_ctx = context();
-    }
-
-    normalizer & get_normalizer() {
-        return m_normalizer;
-    }
 };
-
-type_checker::type_checker(ro_environment const & env, bool infer_only):m_ptr(new imp(env, infer_only)) {}
-type_checker::~type_checker() {}
-expr type_checker::infer_type(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
-    return m_ptr->infer_type(e, ctx, menv, uc);
 }
-expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & uc) {
-    return m_ptr->infer_type(e, ctx, some_menv(menv), &uc);
-}
-expr type_checker::infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv) {
-    // metavariable environment is not updated when unification constraints are not provided
-    return infer_type(e, ctx, some_menv(menv.to_rw()), nullptr);
-}
-expr type_checker::infer_type(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return infer_type(e, ctx, ro_metavar_env::to_rw(menv), nullptr);
-}
-expr type_checker::infer_type(expr const & e, context const & ctx) {
-    return infer_type(e, ctx, none_menv(), nullptr);
-}
-expr type_checker::check(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
-    return m_ptr->check(e, ctx, menv, uc);
-}
-expr type_checker::check(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & uc) {
-    return m_ptr->check(e, ctx, some_menv(menv), &uc);
-}
-expr type_checker::check(expr const & e, context const & ctx, ro_metavar_env const & menv) {
-    // metavariable environment is not updated when unification constraints are not provided
-    return check(e, ctx, some_menv(menv.to_rw()), nullptr);
-}
-expr type_checker::check(expr const & e, context const & ctx) {
-    return check(e, ctx, none_menv(), nullptr);
-}
-bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return m_ptr->is_convertible(t1, t2, ctx, ro_metavar_env::to_rw(menv));
-}
-bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) {
-    return m_ptr->is_convertible(t1, t2, ctx, none_menv());
-}
-bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return m_ptr->is_definitionally_equal(t1, t2, ctx, ro_metavar_env::to_rw(menv));
-}
-bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx) {
-    return m_ptr->is_definitionally_equal(t1, t2, ctx, none_menv());
-}
-void type_checker::check_type(expr const & e, context const & ctx) {
-    m_ptr->check_type(e, ctx);
-}
-expr type_checker::ensure_pi(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return m_ptr->ensure_pi(e, ctx, ro_metavar_env::to_rw(menv));
-}
-expr type_checker::ensure_pi(expr const & e, context const & ctx) {
-    return m_ptr->ensure_pi(e, ctx, none_menv());
-}
-expr type_checker::ensure_sigma(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return m_ptr->ensure_sigma(e, ctx, ro_metavar_env::to_rw(menv));
-}
-expr type_checker::ensure_sigma(expr const & e, context const & ctx) {
-    return m_ptr->ensure_sigma(e, ctx, none_menv());
-}
-bool type_checker::is_proposition(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv));
-}
-bool type_checker::is_proposition(expr const & e, context const & ctx) {
-    return is_proposition(e, ctx, none_ro_menv());
-}
-bool type_checker::is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) {
-    return is_proposition(e, ctx, some_ro_menv(menv));
-}
-bool type_checker::is_flex_proposition(expr e, context ctx, optional<ro_metavar_env> const & menv) {
-    while (is_pi(e)) {
-        ctx = extend(ctx, abst_name(e), abst_domain(e));
-        e   = abst_body(e);
-    }
-    return is_proposition(e, ctx, menv);
-}
-bool type_checker::is_flex_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) {
-    return is_flex_proposition(e, ctx, some_ro_menv(menv));
-}
-bool type_checker::is_flex_proposition(expr const & e, context const & ctx) {
-    return is_flex_proposition(e, ctx, none_ro_menv());
-}
-void type_checker::clear() { m_ptr->clear(); }
-normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
-expr  type_check(expr const & e, ro_environment const & env, context const & ctx) {
-    return type_checker(env).check(e, ctx);
-}
-bool is_convertible(expr const & given, expr const & expected, ro_environment const & env, context const & ctx) {
-    return type_checker(env).is_convertible(given, expected, ctx);
-}
-bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return type_checker(env).is_proposition(e, ctx, menv);
-}
-bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, ro_metavar_env const & menv) {
-    return is_proposition(e, env, ctx, some_ro_menv(menv));
-}
-bool is_proposition(expr const & e, ro_environment const & env, context const & ctx) {
-    return is_proposition(e, env, ctx, none_ro_menv());
-}
-}
-#endif
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index b14d40881..6260cfad9 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include <utility>
 #include "util/name_generator.h"
+#include "util/name_set.h"
 #include "kernel/environment.h"
 #include "kernel/constraint.h"
 
@@ -25,7 +26,7 @@ public:
    The type checker produces constraints, and they are sent to the constraint handler.
 */
 class type_checker {
-    class imp;
+    struct imp;
     std::unique_ptr<imp> m_ptr;
 public:
     /**
@@ -34,15 +35,14 @@ public:
 
        The following set of options is supported:
          - memoize:      inferred types are memoized/cached
-         - unique_expr:  hash consing is performed on input expressions, it improves the effectiveness of memoize
          - extra_opaque: additional definitions that should be treated as opaque
     */
-    type_checker(environment const & env, name_generator const & g, constraint_handler & h, options const & o = options());
+    type_checker(environment const & env, name_generator const & g, constraint_handler & h, bool memoize = false, name_set const & extra_opaque = name_set());
     /**
        \brief Similar to the previous constructor, but if a method tries to create a constraint, then an
        exception is thrown.
     */
-    type_checker(environment const & env, name_generator const & g, options const & o = options());
+    type_checker(environment const & env, name_generator const & g, bool memoize = false, name_set const & extra_opaque = name_set());
     ~type_checker();
 
     /**