From c0e1d05199f172b964ae8e1634ebbdff2a93d5d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Jun 2018 16:03:16 -0700
Subject: [PATCH] chore(kernel): type_checker ==> old_type_checker

---
 src/checker/simple_pp.cpp                     |  4 +-
 src/checker/text_import.cpp                   |  4 +-
 src/frontends/lean/builtin_cmds.cpp           |  4 +-
 src/frontends/lean/builtin_exprs.cpp          |  3 +-
 src/frontends/lean/decl_cmds.cpp              |  2 +-
 src/frontends/lean/definition_cmds.cpp        |  4 +-
 src/frontends/lean/inductive_cmds.cpp         |  5 +-
 src/frontends/lean/info_manager.cpp           |  1 -
 src/frontends/lean/pp.cpp                     |  3 +-
 src/frontends/lean/print_cmd.cpp              |  3 +-
 src/frontends/lean/structure_cmd.cpp          |  1 +
 src/frontends/lean/util.cpp                   |  4 +-
 src/frontends/lean/util.h                     |  1 -
 src/kernel/CMakeLists.txt                     |  2 +-
 src/kernel/environment.cpp                    |  2 +-
 src/kernel/environment.h                      |  2 +-
 src/kernel/inductive/inductive.cpp            | 14 +--
 src/kernel/inductive/inductive.h              |  2 +-
 src/kernel/init_module.cpp                    |  6 +-
 ...{type_checker.cpp => old_type_checker.cpp} | 98 +++++++++----------
 .../{type_checker.h => old_type_checker.h}    | 12 +--
 src/kernel/quot.cpp                           |  2 +-
 src/library/aux_definition.cpp                |  2 +-
 src/library/class.cpp                         |  6 +-
 src/library/compiler/elim_recursors.cpp       |  4 +-
 src/library/compiler/eta_expansion.cpp        |  1 -
 src/library/compiler/preprocess.cpp           |  4 +-
 src/library/compiler/util.cpp                 |  4 +-
 src/library/constructions/brec_on.cpp         |  6 +-
 src/library/constructions/cases_on.cpp        |  2 +-
 src/library/constructions/drec.cpp            |  4 +-
 src/library/constructions/has_sizeof.cpp      |  2 +-
 src/library/constructions/injective.cpp       |  2 +-
 src/library/constructions/no_confusion.cpp    |  6 +-
 src/library/constructions/projection.cpp      |  4 +-
 src/library/constructions/rec_on.cpp          |  2 +-
 src/library/equations_compiler/equations.cpp  |  1 -
 .../equations_compiler/unbounded_rec.cpp      |  1 -
 src/library/equations_compiler/util.cpp       |  2 +-
 src/library/inductive_compiler/mutual.cpp     |  4 +-
 src/library/inductive_compiler/nested.cpp     |  2 +-
 src/library/inductive_compiler/util.cpp       |  4 +-
 src/library/inverse.cpp                       |  4 +-
 src/library/module.cpp                        |  1 -
 src/library/noncomputable.cpp                 | 12 +--
 src/library/normalize.cpp                     |  4 +-
 src/library/reducible.cpp                     |  1 -
 src/library/sorry.cpp                         |  1 -
 src/library/string.cpp                        |  1 -
 src/library/tactic/eval.cpp                   |  2 +-
 src/library/tactic/tactic_evaluator.cpp       |  1 -
 src/library/tactic/tactic_state.cpp           |  1 -
 src/library/trace.cpp                         |  4 +-
 src/library/user_recursors.cpp                |  4 +-
 src/library/util.cpp                          | 12 +--
 src/library/util.h                            |  2 +-
 src/library/vm/interaction_state_imp.h        |  2 +-
 src/library/vm/vm_environment.cpp             |  2 +-
 src/shell/lean.cpp                            |  1 -
 src/tests/kernel/environment.cpp              |  6 +-
 60 files changed, 148 insertions(+), 155 deletions(-)
 rename src/kernel/{type_checker.cpp => old_type_checker.cpp} (89%)
 rename src/kernel/{type_checker.h => old_type_checker.h} (95%)

diff --git a/src/checker/simple_pp.cpp b/src/checker/simple_pp.cpp
index a51126f6ec..a9964986c3 100644
--- a/src/checker/simple_pp.cpp
+++ b/src/checker/simple_pp.cpp
@@ -6,7 +6,7 @@ Author: Gabriel Ebner
 */
 #include "checker/simple_pp.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/for_each_fn.h"
 
 namespace lean {
@@ -38,7 +38,7 @@ static format pp_name(name n) {
 }
 
 struct simple_pp_fn {
-    type_checker m_tc;
+    old_type_checker m_tc;
     lowlevel_notations m_notations;
     unsigned m_indent = 0;
 
diff --git a/src/checker/text_import.cpp b/src/checker/text_import.cpp
index 3af8c60dc7..28ee6d318b 100644
--- a/src/checker/text_import.cpp
+++ b/src/checker/text_import.cpp
@@ -10,7 +10,7 @@ Author: Gabriel Ebner
 #include "runtime/sstream.h"
 #include "kernel/environment.h"
 #include "kernel/inductive/inductive.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/quot.h"
 #include "checker/text_import.h"
 
@@ -70,7 +70,7 @@ struct text_importer {
         auto ls = read_level_params(in);
 
         auto decl =
-            type_checker(m_env).is_prop(m_expr.at(type_idx)) ?
+            old_type_checker(m_env).is_prop(m_expr.at(type_idx)) ?
                 mk_theorem(m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx)) :
                 mk_definition(m_env, m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx), true, false);
 
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 07ab4bcc77..1b4bfefa77 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "util/timeit.h"
 #include "util/sexpr/option_declarations.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/replace_fn.h"
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
@@ -195,7 +195,7 @@ environment check_cmd(parser & p) {
     expr e; level_param_names ls;
     transient_cmd_scope cmd_scope(p);
     std::tie(e, ls) = parse_local_expr(p, "_check");
-    type_checker tc(p.env(), true, false);
+    old_type_checker tc(p.env(), true, false);
     expr type = tc.check(e, ls);
     if (is_synthetic_sorry(e) && (is_synthetic_sorry(type) || is_metavar(type))) {
         // do not show useless type-checking results such as ?? : ?M_1
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index ade1e6bbb4..11f4bf2f1a 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/option_declarations.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
+#include "kernel/old_type_checker.h"
 #include "library/annotation.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
@@ -1075,7 +1076,7 @@ static expr parse_field(parser & p, unsigned, expr const * args, pos_info const
             metavar_context mctx;
             bool check_unassigned = false;
             lhs = p.elaborate({}, mctx, lhs, check_unassigned).first;
-            type_checker tc(p.env(), true, false);
+            old_type_checker tc(p.env(), true, false);
             lhs_type = tc.infer(lhs);
         } catch (exception &) {
             /* failed to elaborate or infer type */
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 1989d7a8a9..45f70c5b19 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "util/fresh_name.h"
 #include "util/timeit.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
 #include "kernel/for_each_fn.h"
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 7bbf8ce77d..48f9a7df65 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "library/profiling.h"
 #include "library/sorry.h"
 #include "util/timeit.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/declaration.h"
 #include "kernel/instantiate.h"
 #include "kernel/replace_fn.h"
@@ -244,7 +244,7 @@ declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buff
     if (env.find(c_real_name)) {
         throw exception(sstream() << "invalid definition, a declaration named '" << c_real_name << "' has already been declared");
     }
-    if (val && !meta.m_modifiers.m_is_meta && !type_checker(env).is_prop(type)) {
+    if (val && !meta.m_modifiers.m_is_meta && !old_type_checker(env).is_prop(type)) {
         /* We only abstract nested proofs if the type of the definition is not a proposition */
         std::tie(new_env, type) = abstract_nested_proofs(new_env, c_real_name, type);
         std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val);
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index 3689880169..21edd72f57 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -14,9 +14,10 @@ Authors: Daniel Selsam, Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
-#include "kernel/inductive/inductive.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/free_vars.h"
+#include "kernel/inductive/inductive.h"
 #include "library/locals.h"
 #include "library/attribute_manager.h"
 #include "library/deep_copy.h"
@@ -365,7 +366,7 @@ class inductive_cmd_fn {
         while (is_pi(ty)) {
             ir_arg++;
             expr arg_ty = binding_domain(ty);
-            type_checker ctx(m_env);
+            old_type_checker ctx(m_env);
             level arg_level = get_level(ctx, arg_ty);
             if (!(is_geq(constant_resultant_level, arg_level) || is_zero(constant_resultant_level))) {
                 throw exception(sstream() << "universe level of type_of(arg #" << ir_arg << ") "
diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index 7a32317b8e..7440a50038 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include <vector>
 #include <set>
 #include <string>
-#include "kernel/type_checker.h"
 #include "library/trace.h"
 #include "library/documentation.h"
 #include "library/vm/vm.h"
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c2a9c63177..76009fe9f5 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/free_vars.h"
 #include "kernel/abstract.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/instantiate.h"
 #include "library/sorry.h"
 #include "library/annotation.h"
@@ -1911,7 +1912,7 @@ static options mk_options(bool detail) {
 }
 
 static void pp_core(environment const & env, expr const & e, bool detail) {
-    type_checker tc(env);
+    old_type_checker tc(env);
     io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
     regular(env, ios, tc) << e << "\n";
 }
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index c8e97ac701..449108a315 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/option_declarations.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/quot.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/trace.h"
 #include "library/sorry.h"
@@ -322,7 +323,7 @@ static void print_recursor_info(parser & p, message_builder & out) {
 }
 
 static bool print_constant(parser const & p, message_builder & out, char const * kind, declaration const & d, bool is_def = false) {
-    type_checker tc(p.env());
+    old_type_checker tc(p.env());
     print_attributes(p, out, d.get_name());
     if (is_protected(p.env(), d.get_name()))
         out << "protected ";
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 80a8785f1f..698f043c8f 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
 #include "kernel/error_msgs.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/replace_visitor.h"
 #include "library/trace.h"
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index a1b10340ee..118e77316e 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/error_msgs.h"
 #include "kernel/for_each_fn.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "library/kernel_serializer.h"
 #include "library/scoped_ext.h"
 #include "library/annotation.h"
@@ -382,7 +382,7 @@ expr mk_auto_param(expr const & t, name const & tac_name) {
 }
 
 static bool is_tactic_unit(environment const & env, expr const & c) {
-    type_checker tc(env);
+    old_type_checker tc(env);
     return tc.is_def_eq(tc.infer(c), mk_tactic_unit());
 }
 
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index ac83f18818..9f2005ed89 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
-#include "kernel/type_checker.h"
 #include "library/util.h"
 #include "library/locals.h"
 #include "library/vm/vm.h"
diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index e8d4206a3e..8e84496753 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
 replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp local_ctx.cpp
 formatter.cpp declaration.cpp environment.cpp pos_info_provider.cpp
-type_checker.cpp error_msgs.cpp kernel_exception.cpp
+old_type_checker.cpp error_msgs.cpp kernel_exception.cpp
 normalizer_extension.cpp init_module.cpp expr_cache.cpp scope_pos_info_provider.cpp
 equiv_manager.cpp quot.cpp abstract_type_context.cpp inductive.cpp standard_kernel.cpp)
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 77753e717b..2fcea357f6 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "runtime/thread.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/quot.h"
 
 namespace lean {
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index b93c03ffab..73945b75b8 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -25,7 +25,7 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-class type_checker;
+class old_type_checker;
 class environment;
 class certified_declaration;
 namespace inductive { class certified_inductive_decl; }
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 1752261558..4bce1dbee6 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/list_fn.h"
 #include "util/rb_map.h"
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
@@ -228,7 +228,7 @@ environment certified_inductive_decl::add(environment const & env) const {
 
 /** \brief Helper functional object for processing inductive datatype declarations. */
 struct add_inductive_fn {
-    typedef std::unique_ptr<type_checker> type_checker_ptr;
+    typedef std::unique_ptr<old_type_checker> old_type_checker_ptr;
     environment          m_env;
     name_generator       m_name_generator;
     inductive_decl       m_decl;
@@ -237,7 +237,7 @@ struct add_inductive_fn {
     // universe level instantiation
     bool                 m_is_not_zero;
     levels               m_levels;       // m_decl.m_level_params ==> m_levels
-    type_checker_ptr     m_tc;
+    old_type_checker_ptr     m_tc;
 
     level                m_elim_level;   // extra universe level for eliminator.
     bool                 m_dep_elim;     // true if using dependent elimination
@@ -262,7 +262,7 @@ struct add_inductive_fn {
                      inductive_decl const & decl,
                      bool is_meta):
         m_env(env), m_name_generator(*g_ind_fresh), m_decl(decl),
-        m_tc(new type_checker(m_env, true, false)) {
+        m_tc(new old_type_checker(m_env, true, false)) {
         m_is_not_zero = false;
         m_levels      = param_names_to_levels(decl.m_level_params);
         m_is_meta  = is_meta;
@@ -270,10 +270,10 @@ struct add_inductive_fn {
 
     /** \brief Make sure the latest environment is being used by m_tc. */
     void updt_type_checker() {
-        m_tc.reset(new type_checker(m_env, true, false));
+        m_tc.reset(new old_type_checker(m_env, true, false));
     }
 
-    type_checker & tc() { return *(m_tc.get()); }
+    old_type_checker & tc() { return *(m_tc.get()); }
     bool is_def_eq(expr const & t, expr const & s) { return tc().is_def_eq(t, s); }
     expr whnf(expr const & e) { return tc().whnf(e); }
     expr ensure_type(expr const & e) { return tc().ensure_type(e); }
@@ -902,7 +902,7 @@ optional<expr> is_elim_meta_app_core(Ctx & ctx, expr const & e) {
     }
 }
 
-bool is_elim_meta_app(type_checker & tc, expr const & e) {
+bool is_elim_meta_app(old_type_checker & tc, expr const & e) {
     return static_cast<bool>(is_elim_meta_app_core(tc, e));
 }
 
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index f4fcbb9799..d85c337f8f 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -116,7 +116,7 @@ optional<name> is_elim_rule(environment const & env, name const & n);
 
 /** \brief Given the eliminator \c n, this function return the position of major premise */
 optional<unsigned> get_elim_major_idx(environment const & env, name const & n);
-bool is_elim_meta_app(type_checker & tc, expr const & e);
+bool is_elim_meta_app(old_type_checker & tc, expr const & e);
 
 /** \brief Return the number of parameters in the given inductive datatype.
     If \c n is not an inductive datatype in \c env, then return none. */
diff --git a/src/kernel/init_module.cpp b/src/kernel/init_module.cpp
index 71d2af63e0..3bd197fa51 100644
--- a/src/kernel/init_module.cpp
+++ b/src/kernel/init_module.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/expr.h"
 #include "kernel/formatter.h"
 #include "kernel/level.h"
@@ -20,7 +20,7 @@ void initialize_kernel_module() {
     initialize_level();
     initialize_expr();
     initialize_declaration();
-    initialize_type_checker();
+    initialize_old_type_checker();
     initialize_environment();
     initialize_formatter();
     initialize_quot();
@@ -32,7 +32,7 @@ void finalize_kernel_module() {
     finalize_quot();
     finalize_formatter();
     finalize_environment();
-    finalize_type_checker();
+    finalize_old_type_checker();
     finalize_declaration();
     finalize_expr();
     finalize_level();
diff --git a/src/kernel/type_checker.cpp b/src/kernel/old_type_checker.cpp
similarity index 89%
rename from src/kernel/type_checker.cpp
rename to src/kernel/old_type_checker.cpp
index f09df86318..a1bdffabe9 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/old_type_checker.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "util/lbool.h"
 #include "util/fresh_name.h"
 #include "util/task_builder.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/expr_maps.h"
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
@@ -27,14 +27,14 @@ namespace lean {
 static name * g_kernel_fresh = nullptr;
 static expr * g_dont_care    = nullptr;
 
-optional<expr> type_checker::expand_macro(expr const & m) {
+optional<expr> old_type_checker::expand_macro(expr const & m) {
     lean_assert(is_macro(m));
     return macro_def(m).expand(m, *this);
 }
 
 /** \brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
     It also returns the fresh local constant. */
-pair<expr, expr> type_checker::open_binding_body(expr const & e) {
+pair<expr, expr> old_type_checker::open_binding_body(expr const & e) {
     expr local     = mk_local(m_name_generator.next(), binding_name(e), binding_domain(e), binding_info(e));
     return mk_pair(instantiate(binding_body(e), local), local);
 }
@@ -44,7 +44,7 @@ pair<expr, expr> type_checker::open_binding_body(expr const & e) {
 
     \remark \c s is used to extract position (line number information) when an
     error message is produced */
-expr type_checker::ensure_sort_core(expr e, expr const & s) {
+expr old_type_checker::ensure_sort_core(expr e, expr const & s) {
     if (is_sort(e))
         return e;
     auto new_e = whnf(e);
@@ -56,7 +56,7 @@ expr type_checker::ensure_sort_core(expr e, expr const & s) {
 }
 
 /** \brief Similar to \c ensure_sort, but makes sure \c e "is" a Pi. */
-expr type_checker::ensure_pi_core(expr e, expr const & s) {
+expr old_type_checker::ensure_pi_core(expr e, expr const & s) {
     if (is_pi(e))
         return e;
     auto new_e = whnf(e);
@@ -67,7 +67,7 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) {
     }
 }
 
-void type_checker::check_level(level const & l, expr const & s) {
+void old_type_checker::check_level(level const & l, expr const & s) {
     if (m_params) {
         if (auto n2 = get_undef_param(l, *m_params))
             throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '"
@@ -75,7 +75,7 @@ void type_checker::check_level(level const & l, expr const & s) {
     }
 }
 
-expr type_checker::infer_constant(expr const & e, bool infer_only) {
+expr old_type_checker::infer_constant(expr const & e, bool infer_only) {
     declaration d    = m_env.get(const_name(e));
     auto const & ps = d.get_univ_params();
     auto const & ls = const_levels(e);
@@ -94,7 +94,7 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) {
     return instantiate_type_univ_params(d, ls);
 }
 
-expr type_checker::infer_macro(expr const & e, bool infer_only) {
+expr old_type_checker::infer_macro(expr const & e, bool infer_only) {
     auto def = macro_def(e);
     auto t   = def.check_type(e, *this, infer_only);
 // TODO(Leo): macros will be deleted
@@ -105,7 +105,7 @@ expr type_checker::infer_macro(expr const & e, bool infer_only) {
     return t;
 }
 
-expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
+expr old_type_checker::infer_lambda(expr const & _e, bool infer_only) {
     buffer<expr> es, ds, ls;
     expr e = _e;
     while (is_lambda(e)) {
@@ -131,7 +131,7 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
     return r;
 }
 
-expr type_checker::infer_pi(expr const & _e, bool infer_only) {
+expr old_type_checker::infer_pi(expr const & _e, bool infer_only) {
     buffer<expr>  ls;
     buffer<level> us;
     expr e = _e;
@@ -156,7 +156,7 @@ expr type_checker::infer_pi(expr const & _e, bool infer_only) {
     return mk_sort(r);
 }
 
-expr type_checker::infer_app(expr const & e, bool infer_only) {
+expr old_type_checker::infer_app(expr const & e, bool infer_only) {
     if (!infer_only) {
         expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), e);
         expr a_type = infer_type_core(app_arg(e), infer_only);
@@ -188,7 +188,7 @@ expr type_checker::infer_app(expr const & e, bool infer_only) {
     }
 }
 
-expr type_checker::infer_let(expr const & e, bool infer_only) {
+expr old_type_checker::infer_let(expr const & e, bool infer_only) {
     if (!infer_only) {
         if (let_name(e).is_anonymous())
             throw_kernel_exception(m_env, "invalid anonymous let var name", e);
@@ -207,7 +207,7 @@ expr type_checker::infer_let(expr const & e, bool infer_only) {
 
 /** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
     \pre closed(e) */
-expr type_checker::infer_type_core(expr const & e, bool infer_only) {
+expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
     if (is_var(e))
         throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
 
@@ -242,41 +242,41 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
     return r;
 }
 
-expr type_checker::infer_type(expr const & e) {
+expr old_type_checker::infer_type(expr const & e) {
     return infer_type_core(e, true);
 }
 
-expr type_checker::check(expr const & e, level_param_names const & ps) {
+expr old_type_checker::check(expr const & e, level_param_names const & ps) {
     flet<level_param_names const *> updt(m_params, &ps);
     return infer_type_core(e, false);
 }
 
-expr type_checker::check_ignore_undefined_universes(expr const & e) {
+expr old_type_checker::check_ignore_undefined_universes(expr const & e) {
     flet<level_param_names const *> updt(m_params, nullptr);
     return infer_type_core(e, false);
 }
 
-expr type_checker::ensure_sort(expr const & e, expr const & s) {
+expr old_type_checker::ensure_sort(expr const & e, expr const & s) {
     return ensure_sort_core(e, s);
 }
 
-expr type_checker::ensure_pi(expr const & e, expr const & s) {
+expr old_type_checker::ensure_pi(expr const & e, expr const & s) {
     return ensure_pi_core(e, s);
 }
 
-bool type_checker::is_def_eq_types(expr const & t, expr const & s) {
+bool old_type_checker::is_def_eq_types(expr const & t, expr const & s) {
     expr t1 = infer_type_core(t, true);
     expr t2 = infer_type_core(s, true);
     return is_def_eq(t1, t2);
 }
 
 /** \brief Return true iff \c e is a proposition */
-bool type_checker::is_prop(expr const & e) {
+bool old_type_checker::is_prop(expr const & e) {
     return whnf(infer_type(e)) == mk_Prop();
 }
 
 /** \brief Apply normalizer extensions to \c e. */
-optional<expr> type_checker::norm_ext(expr const & e) {
+optional<expr> old_type_checker::norm_ext(expr const & e) {
     if (m_env.is_quot_initialized()) {
         if (optional<expr> r = quot_reduce_rec(e, [&](expr const & e) { return whnf(e); })) {
             return r;
@@ -286,7 +286,7 @@ optional<expr> type_checker::norm_ext(expr const & e) {
 }
 
 /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
-expr type_checker::whnf_core(expr const & e) {
+expr old_type_checker::whnf_core(expr const & e) {
     check_system("whnf");
 
     // handle easy cases
@@ -354,7 +354,7 @@ expr type_checker::whnf_core(expr const & e) {
 
 /** \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
     to be expanded. */
-optional<declaration> type_checker::is_delta(expr const & e) const {
+optional<declaration> old_type_checker::is_delta(expr const & e) const {
     expr const & f = get_app_fn(e);
     if (is_constant(f)) {
         if (auto d = m_env.find(const_name(f)))
@@ -364,7 +364,7 @@ optional<declaration> type_checker::is_delta(expr const & e) const {
     return none_declaration();
 }
 
-optional<expr> type_checker::unfold_definition_core(expr const & e) {
+optional<expr> old_type_checker::unfold_definition_core(expr const & e) {
     if (is_constant(e)) {
         if (auto d = is_delta(e)) {
             if (length(const_levels(e)) == d->get_num_univ_params())
@@ -375,7 +375,7 @@ optional<expr> type_checker::unfold_definition_core(expr const & e) {
 }
 
 /* Unfold head(e) if it is a constant */
-optional<expr> type_checker::unfold_definition(expr const & e) {
+optional<expr> old_type_checker::unfold_definition(expr const & e) {
     if (is_app(e)) {
         expr f0 = get_app_fn(e);
         if (auto f  = unfold_definition_core(f0)) {
@@ -391,7 +391,7 @@ optional<expr> type_checker::unfold_definition(expr const & e) {
 }
 
 /** \brief Put expression \c t in weak head normal form */
-expr type_checker::whnf(expr const & e) {
+expr old_type_checker::whnf(expr const & e) {
     // Do not cache easy cases
     switch (e.kind()) {
     case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
@@ -429,7 +429,7 @@ expr type_checker::whnf(expr const & e) {
         domain(t) is definitionally equal to domain(s)
         and
         body(t) is definitionally equal to body(s) */
-bool type_checker::is_def_eq_binding(expr t, expr s) {
+bool old_type_checker::is_def_eq_binding(expr t, expr s) {
     lean_assert(t.kind() == s.kind());
     lean_assert(is_binding(t));
     expr_kind k = t.kind();
@@ -457,7 +457,7 @@ bool type_checker::is_def_eq_binding(expr t, expr s) {
                      instantiate_rev(s, subst.size(), subst.data()));
 }
 
-bool type_checker::is_def_eq(level const & l1, level const & l2) {
+bool old_type_checker::is_def_eq(level const & l1, level const & l2) {
     if (is_equivalent(l1, l2)) {
         return true;
     } else {
@@ -465,7 +465,7 @@ bool type_checker::is_def_eq(level const & l1, level const & l2) {
     }
 }
 
-bool type_checker::is_def_eq(levels const & ls1, levels const & ls2) {
+bool old_type_checker::is_def_eq(levels const & ls1, levels const & ls2) {
     if (is_nil(ls1) && is_nil(ls2)) {
         return true;
     } else if (!is_nil(ls1) && !is_nil(ls2)) {
@@ -478,7 +478,7 @@ bool type_checker::is_def_eq(levels const & ls1, levels const & ls2) {
 }
 
 /** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
-lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_hash) {
+lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_hash) {
     if (m_eqv_manager.is_equiv(t, s, use_hash))
         return l_true;
     if (t.kind() == s.kind()) {
@@ -500,7 +500,7 @@ lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_has
 
 /** \brief Return true if arguments of \c t are definitionally equal to arguments of \c s.
     This method is used to implement an optimization in the method \c is_def_eq. */
-bool type_checker::is_def_eq_args(expr t, expr s) {
+bool old_type_checker::is_def_eq_args(expr t, expr s) {
     while (is_app(t) && is_app(s)) {
         if (!is_def_eq(app_arg(t), app_arg(s)))
             return false;
@@ -511,7 +511,7 @@ bool type_checker::is_def_eq_args(expr t, expr s) {
 }
 
 /** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
-bool type_checker::try_eta_expansion_core(expr const & t, expr const & s) {
+bool old_type_checker::try_eta_expansion_core(expr const & t, expr const & s) {
     if (is_lambda(t) && !is_lambda(s)) {
         expr s_type = whnf(infer_type(s));
         if (!is_pi(s_type))
@@ -529,7 +529,7 @@ bool type_checker::try_eta_expansion_core(expr const & t, expr const & s) {
     <tt>(f a_1 ... a_n)</tt> <tt>(g b_1 ... b_n)</tt>, and \c f and \c g are definitionally equal, and
     \c a_i and \c b_i are also definitionally equal for every 1 <= i <= n.
     Return false otherwise. */
-bool type_checker::is_def_eq_app(expr const & t, expr const & s) {
+bool old_type_checker::is_def_eq_app(expr const & t, expr const & s) {
     if (is_app(t) && is_app(s)) {
         buffer<expr> t_args;
         buffer<expr> s_args;
@@ -550,14 +550,14 @@ bool type_checker::is_def_eq_app(expr const & t, expr const & s) {
 
 /** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
     Return false otherwise. */
-bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
+bool old_type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
     // Proof irrelevance support for Prop (aka Type.{0})
     expr t_type = infer_type(t);
     expr s_type = infer_type(s);
     return is_prop(t_type) && is_def_eq(t_type, s_type);
 }
 
-bool type_checker::failed_before(expr const & t, expr const & s) const {
+bool old_type_checker::failed_before(expr const & t, expr const & s) const {
     if (t.hash() < s.hash()) {
         return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
     } else if (t.hash() > s.hash()) {
@@ -569,7 +569,7 @@ bool type_checker::failed_before(expr const & t, expr const & s) const {
     }
 }
 
-void type_checker::cache_failure(expr const & t, expr const & s) {
+void old_type_checker::cache_failure(expr const & t, expr const & s) {
     if (t.hash() <= s.hash())
         m_failure_cache.insert(mk_pair(t, s));
     else
@@ -585,7 +585,7 @@ static name * g_id_delta = nullptr;
      - l_undef it the step did not manage to establish whether they are definitionally equal or not.
 
      \remark t_n, s_n and cs are updated. */
-auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
+auto old_type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
     auto d_t = is_delta(t_n);
     auto d_s = is_delta(s_n);
     if (!d_t && !d_s) {
@@ -650,7 +650,7 @@ auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reductio
     lean_unreachable();
 }
 
-lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
+lbool old_type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
     while (true) {
         switch (lazy_delta_reduction_step(t_n, s_n)) {
         case reduction_status::Continue:   break;
@@ -661,7 +661,7 @@ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
     }
 }
 
-bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
+bool old_type_checker::is_def_eq_core(expr const & t, expr const & s) {
     check_system("is_definitionally_equal");
     bool use_hash = true;
     lbool r = quick_is_def_eq(t, s, use_hash);
@@ -709,18 +709,18 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
     return false;
 }
 
-bool type_checker::is_def_eq(expr const & t, expr const & s) {
+bool old_type_checker::is_def_eq(expr const & t, expr const & s) {
     bool r = is_def_eq_core(t, s);
     if (r)
         m_eqv_manager.add_equiv(t, s);
     return r;
 }
 
-type_checker::type_checker(environment const & env, bool memoize, bool non_meta_only):
+old_type_checker::old_type_checker(environment const & env, bool memoize, bool non_meta_only):
     m_env(env), m_name_generator(*g_kernel_fresh), m_memoize(memoize), m_non_meta_only(non_meta_only), m_params(nullptr) {
 }
 
-type_checker::~type_checker() {}
+old_type_checker::~old_type_checker() {}
 
 void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
     if (has_metavar(e))
@@ -755,7 +755,7 @@ static void check_duplicated_params(environment const & env, declaration const &
     }
 }
 
-static void check_definition(environment const & env, declaration const & d, type_checker & checker) {
+static void check_definition(environment const & env, declaration const & d, old_type_checker & checker) {
     check_no_mlocal(env, d.get_name(), d.get_value(), false);
     expr val_type = checker.check(d.get_value(), d.get_univ_params());
     if (!checker.is_def_eq(val_type, d.get_type())) {
@@ -763,7 +763,7 @@ static void check_definition(environment const & env, declaration const & d, typ
     }
 }
 
-static void check_decl_type(environment const & env, declaration const & d, type_checker & checker) {
+static void check_decl_type(environment const & env, declaration const & d, old_type_checker & checker) {
     check_no_mlocal(env, d.get_name(), d.get_type(), true);
     check_name(env, d.get_name());
     check_duplicated_params(env, d);
@@ -773,13 +773,13 @@ static void check_decl_type(environment const & env, declaration const & d, type
 
 void check_decl_type(environment const & env, declaration const & d) {
     bool memoize = true; bool non_meta_only = !d.is_meta();
-    type_checker checker(env, memoize, non_meta_only);
+    old_type_checker checker(env, memoize, non_meta_only);
     check_decl_type(env, d, checker);
 }
 
 void check_decl_value(environment const & env, declaration const & d) {
     bool memoize = true; bool non_meta_only = !d.is_meta();
-    type_checker checker(env, memoize, non_meta_only);
+    old_type_checker checker(env, memoize, non_meta_only);
     if (d.is_definition()) {
         check_definition(env, d, checker);
     }
@@ -787,7 +787,7 @@ void check_decl_value(environment const & env, declaration const & d) {
 
 certified_declaration check(environment const & env, declaration const & d) {
     bool memoize = true; bool non_meta_only = !d.is_meta();
-    type_checker checker(env, memoize, non_meta_only);
+    old_type_checker checker(env, memoize, non_meta_only);
     check_decl_type(env, d, checker);
     if (d.is_definition()) {
         check_definition(env, d, checker);
@@ -808,14 +808,14 @@ certified_declaration certify_unchecked::certify_or_check(environment const & en
         return certify(env, d);
 }
 
-void initialize_type_checker() {
+void initialize_old_type_checker() {
     g_id_delta     = new name("id_delta");
     g_dont_care    = new expr(Const("dontcare"));
     g_kernel_fresh = new name("_kernel_fresh");
     register_name_generator_prefix(*g_kernel_fresh);
 }
 
-void finalize_type_checker() {
+void finalize_old_type_checker() {
     delete g_dont_care;
     delete g_id_delta;
     delete g_kernel_fresh;
diff --git a/src/kernel/type_checker.h b/src/kernel/old_type_checker.h
similarity index 95%
rename from src/kernel/type_checker.h
rename to src/kernel/old_type_checker.h
index 19abe9fb81..4f2c8fedc1 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/old_type_checker.h
@@ -22,7 +22,7 @@ Author: Leonardo de Moura
 namespace lean {
 /** \brief Lean Type Checker. It can also be used to infer types, check whether a
     type \c A is convertible to a type \c B, etc. */
-class type_checker : public abstract_type_context {
+class old_type_checker : public abstract_type_context {
     /* In the type checker cache, we must take into account binder information.
        Examples:
        The type of (lambda x : A, t)   is (Pi x : A, typeof(t))
@@ -82,8 +82,8 @@ public:
         memoize: if true, then inferred types are memoized/cached.
 
     */
-    type_checker(environment const & env, bool memoize = true, bool non_meta_only = true);
-    ~type_checker();
+    old_type_checker(environment const & env, bool memoize = true, bool non_meta_only = true);
+    ~old_type_checker();
 
     virtual environment const & env() const { return m_env; }
 
@@ -138,7 +138,7 @@ public:
     }
 };
 
-typedef std::shared_ptr<type_checker> type_checker_ref;
+typedef std::shared_ptr<old_type_checker> old_type_checker_ref;
 
 void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type);
 void check_no_mlocal(environment const & env, name const & n, expr const & e, bool is_type);
@@ -149,6 +149,6 @@ void check_decl_value(environment const & env, declaration const & d);
     Throw an exception if the declaration is type incorrect. */
 certified_declaration check(environment const & env, declaration const & d);
 
-void initialize_type_checker();
-void finalize_type_checker();
+void initialize_old_type_checker();
+void finalize_old_type_checker();
 }
diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp
index dd2fd27ab5..b7fa2fb2a4 100644
--- a/src/kernel/quot.cpp
+++ b/src/kernel/quot.cpp
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 
 Quotient types.
 */
+#include "kernel/old_type_checker.h"
 #include "kernel/quot.h"
 #include "kernel/abstract.h"
-#include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
 
 namespace lean {
diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp
index 0121ef0ab6..9106307a2b 100644
--- a/src/library/aux_definition.cpp
+++ b/src/library/aux_definition.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
-#include "kernel/type_checker.h"
 #include "kernel/replace_fn.h"
+#include "kernel/old_type_checker.h"
 #include "library/locals.h"
 #include "library/placeholder.h"
 #include "library/module.h"
diff --git a/src/library/class.cpp b/src/library/class.cpp
index 5ad80adfbc..b19c2303b5 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "util/lbool.h"
 #include "util/fresh_name.h"
 #include "util/name_set.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
 #include "library/scoped_ext.h"
@@ -86,7 +86,7 @@ struct class_state {
             m_has_out_params.insert(c);
     }
 
-    void collect_symbols(type_checker & tc, name const & inst, name const & attr) {
+    void collect_symbols(old_type_checker & tc, name const & inst, name const & attr) {
         environment const & env = tc.env();
         name_set S;
         if (auto curr_S = m_attr_symbols.find(attr))
@@ -120,7 +120,7 @@ struct class_state {
         }
         m_priorities.insert(i, p);
         if (auto attrs = m_class_track_attrs.find(c)) {
-            type_checker tc(env);
+            old_type_checker tc(env);
             for (name const & attr : *attrs) {
                 collect_symbols(tc, i, attr);
             }
diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp
index dbba0f6930..b3f2af740b 100644
--- a/src/library/compiler/elim_recursors.cpp
+++ b/src/library/compiler/elim_recursors.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
@@ -30,7 +30,7 @@ protected:
         /* We should use a new type checker because m_env is updated by this object.
            It is safe to use type_checker because value does not contain local_decl_ref objects. */
         level_param_names ps = to_level_param_names(collect_univ_params(value));
-        type_checker tc(m_env);
+        old_type_checker tc(m_env);
         expr type         = tc.infer(value);
         bool meta         = true;
         /* We add declaration as a constant to make sure
diff --git a/src/library/compiler/eta_expansion.cpp b/src/library/compiler/eta_expansion.cpp
index 83f1882fe7..d395a419af 100644
--- a/src/library/compiler/eta_expansion.cpp
+++ b/src/library/compiler/eta_expansion.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index 46f5c22ad8..94ba42f31b 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/declaration.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/replace_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
@@ -177,7 +177,7 @@ class preprocess_fn {
     bool check(declaration const & d, expr const & v) {
         bool memoize       = true;
         bool non_meta_only = false;
-        type_checker tc(m_env, memoize, non_meta_only);
+        old_type_checker tc(m_env, memoize, non_meta_only);
         expr t = tc.check(v, d.get_univ_params());
         if (!tc.is_def_eq(d.get_type(), t))
             throw exception("preprocess failed");
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index d99841a0b9..0b8ae73a96 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include "kernel/find_fn.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/inverse.h"
 #include "library/aux_recursors.h"
@@ -53,7 +53,7 @@ static bool is_typeformer_app(buffer<name> const & typeformer_names, expr const
 
 void get_rec_args(environment const & env, name const & n, buffer<buffer<bool>> & r) {
     lean_assert(inductive::is_inductive_decl(env, n));
-    type_checker tc(env);
+    old_type_checker tc(env);
     declaration ind_decl   = env.get(n);
     declaration rec_decl   = env.get(inductive::get_elim_name(n));
     unsigned nparams       = *inductive::get_num_params(env, n);
diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp
index 5fef98d9c6..9bd4f7554b 100644
--- a/src/library/constructions/brec_on.cpp
+++ b/src/library/constructions/brec_on.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/protected.h"
 #include "library/reducible.h"
@@ -44,7 +44,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
     if (is_inductive_predicate(env, n) || !can_elim_to_type(env, n))
         return env;
     inductive::inductive_decl decl = *inductive::is_inductive_decl(env, n);
-    type_checker tc(env);
+    old_type_checker tc(env);
     unsigned nparams       = decl.m_num_params;
     declaration ind_decl   = env.get(n);
     declaration rec_decl   = env.get(inductive::get_elim_name(n));
@@ -167,7 +167,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
         return env;
     name_generator ngen    = mk_constructions_name_generator();
     inductive::inductive_decl decl = *inductive::is_inductive_decl(env, n);
-    type_checker tc(env);
+    old_type_checker tc(env);
     unsigned nparams       = decl.m_num_params;
     declaration ind_decl   = env.get(n);
     declaration rec_decl   = env.get(inductive::get_elim_name(n));
diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp
index 214a79289e..0748d0874d 100644
--- a/src/library/constructions/cases_on.cpp
+++ b/src/library/constructions/cases_on.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/fresh_name.h"
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/inductive/inductive.h"
 #include "library/module.h"
diff --git a/src/library/constructions/drec.cpp b/src/library/constructions/drec.cpp
index eec2340c07..9f7ed317c5 100644
--- a/src/library/constructions/drec.cpp
+++ b/src/library/constructions/drec.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/inductive/inductive.h"
@@ -23,7 +23,7 @@ enum class drec_kind {DRec, DRecOn, DCasesOn};
 struct mk_drec_fn {
     environment const & env;
     name_generator      ngen;
-    type_checker        tc;
+    old_type_checker        tc;
     name const &        I;
     drec_kind           kind;
     inductive::inductive_decl      I_ind_decl;
diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp
index f6b95ac311..75843df155 100644
--- a/src/library/constructions/has_sizeof.cpp
+++ b/src/library/constructions/has_sizeof.cpp
@@ -8,7 +8,7 @@ Author: Daniel Selsam
 #include "runtime/sstream.h"
 #include "util/fresh_name.h"
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/find_fn.h"
diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp
index a880d062ec..f67c269692 100644
--- a/src/library/constructions/injective.cpp
+++ b/src/library/constructions/injective.cpp
@@ -6,7 +6,7 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/declaration.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/constructions/injective.h"
 #include "library/type_context.h"
diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp
index 9186eb84e4..5493dfcb66 100644
--- a/src/library/constructions/no_confusion.cpp
+++ b/src/library/constructions/no_confusion.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/inductive/inductive.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "library/protected.h"
 #include "library/module.h"
 #include "library/util.h"
@@ -73,7 +73,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     cases_on       = mk_app(cases_on, nindices, args.data() + nparams);
     expr cases_on1 = mk_app(cases_on, v1);
     expr cases_on2 = mk_app(cases_on, v2);
-    type_checker tc(env);
+    old_type_checker tc(env);
     expr t1        = tc.infer(cases_on1);
     expr t2        = tc.infer(cases_on2);
     buffer<expr> outer_cases_on_args;
@@ -134,7 +134,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
     if (!env1)
         return env;
     environment new_env = *env1;
-    type_checker tc(new_env);
+    old_type_checker tc(new_env);
     name_generator ngen                = mk_constructions_name_generator();
     inductive::inductive_decl decl     = *inductive::is_inductive_decl(new_env, n);
     unsigned nparams                   = decl.m_num_params;
diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp
index 565cbbced3..6b58b853ea 100644
--- a/src/library/constructions/projection.cpp
+++ b/src/library/constructions/projection.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "util/fresh_name.h"
 #include "kernel/abstract.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/inductive/inductive.h"
@@ -225,7 +225,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         if (!is_pi(intro_type))
             throw exception(sstream() << "generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
-        type_checker tc(new_env);
+        old_type_checker tc(new_env);
         expr result_type   = binding_domain(intro_type);
         if (is_predicate && !tc.is_prop(result_type)) {
             throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp
index b4aef78aae..5bbf89d8b7 100644
--- a/src/library/constructions/rec_on.cpp
+++ b/src/library/constructions/rec_on.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/module.h"
 #include "library/reducible.h"
diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp
index a4d297610b..cf7d7055db 100644
--- a/src/library/equations_compiler/equations.cpp
+++ b/src/library/equations_compiler/equations.cpp
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include "util/list_fn.h"
 #include "util/fresh_name.h"
 #include "kernel/expr.h"
-#include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/error_msgs.h"
diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp
index afd056c5e5..069989a528 100644
--- a/src/library/equations_compiler/unbounded_rec.cpp
+++ b/src/library/equations_compiler/unbounded_rec.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "kernel/replace_fn.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
 #include "library/locals.h"
 #include "library/private.h"
 #include "library/aliases.h"
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index b3596ea772..69b258c430 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -8,10 +8,10 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/find_fn.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "kernel/scope_pos_info_provider.h"
 #include "kernel/free_vars.h"
-#include "kernel/type_checker.h"
 #include "library/util.h"
 #include "library/module.h"
 #include "library/aliases.h"
diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp
index 82099fb37f..8e2e1ae586 100644
--- a/src/library/inductive_compiler/mutual.cpp
+++ b/src/library/inductive_compiler/mutual.cpp
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Daniel Selsam
 */
-#include "kernel/inductive/inductive.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
 #include "kernel/find_fn.h"
+#include "kernel/inductive/inductive.h"
 #include "util/sexpr/option_declarations.h"
 #include "library/locals.h"
 #include "library/app_builder.h"
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index ea8f53a012..fb25250721 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -9,10 +9,10 @@ Author: Daniel Selsam
 #include "kernel/inductive/inductive.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
 #include "kernel/find_fn.h"
 #include "kernel/expr.h"
 #include "kernel/replace_fn.h"
+#include "kernel/old_type_checker.h"
 #include "util/sexpr/options.h"
 #include "util/sexpr/option_declarations.h"
 #include "util/list_fn.h"
diff --git a/src/library/inductive_compiler/util.cpp b/src/library/inductive_compiler/util.cpp
index 63757eec50..3c072c3260 100644
--- a/src/library/inductive_compiler/util.cpp
+++ b/src/library/inductive_compiler/util.cpp
@@ -7,7 +7,7 @@
 #include "kernel/inductive/inductive.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "util/sexpr/option_declarations.h"
 #include "library/locals.h"
 #include "library/module.h"
@@ -77,7 +77,7 @@ void assert_def_eq(environment const & DEBUG_CODE(env), expr const & DEBUG_CODE(
 }
 
 void assert_type_correct(environment const & env, expr const & e) {
-    type_checker checker(env, true, false /* allow untrusted/meta */);
+    old_type_checker checker(env, true, false /* allow untrusted/meta */);
     try {
         checker.check(e);
     } catch (exception ex) {
diff --git a/src/library/inverse.cpp b/src/library/inverse.cpp
index 2616f29658..e582dabd74 100644
--- a/src/library/inverse.cpp
+++ b/src/library/inverse.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "library/util.h"
 #include "library/scoped_ext.h"
 #include "library/attribute_manager.h"
@@ -80,7 +80,7 @@ void throw_inverse_error() {
 }
 
 environment add_inverse_lemma(environment const & env, name const & lemma, bool persistent) {
-    type_checker tc(env);
+    old_type_checker tc(env);
     declaration d = env.get(lemma);
     buffer<expr> tele;
     expr type     = to_telescope(tc, d.get_type(), tele);
diff --git a/src/library/module.cpp b/src/library/module.cpp
index db4549fb94..8d0f8463f7 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -20,7 +20,6 @@ Author: Leonardo de Moura
 #include "util/buffer.h"
 #include "util/name_map.h"
 #include "util/file_lock.h"
-#include "kernel/type_checker.h"
 #include "library/module.h"
 #include "library/noncomputable.h"
 #include "library/constants.h"
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index c34311573a..862d478f1c 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "library/module.h"
 #include "library/util.h"
 #include "library/fingerprint.h"
@@ -75,7 +75,7 @@ static bool is_builtin_extra(name const & n) {
         n == get_monad_io_random_impl_name();
 }
 
-static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, name const & n) {
+static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ext, name const & n) {
     environment const & env = tc.env();
     if (ext.m_noncomputable.contains(n))
         return true;
@@ -92,7 +92,7 @@ static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, n
 }
 
 bool is_noncomputable(environment const & env, name const & n) {
-    type_checker tc(env);
+    old_type_checker tc(env);
     auto ext = get_extension(env);
     return is_noncomputable(tc, ext, n);
 }
@@ -115,11 +115,11 @@ struct get_noncomputable_reason_fn {
         found(name const & r):m_reason(r) {}
     };
 
-    type_checker &            m_tc;
+    old_type_checker &            m_tc;
     noncomputable_ext const & m_ext;
     expr_set                  m_cache;
 
-    get_noncomputable_reason_fn(type_checker & tc):
+    get_noncomputable_reason_fn(old_type_checker & tc):
         m_tc(tc), m_ext(get_extension(tc.env())) {
     }
 
@@ -211,7 +211,7 @@ optional<name> get_noncomputable_reason(environment const & env, name const & n)
     declaration const & d = env.get(n);
     if (!d.is_definition())
         return optional<name>();
-    type_checker tc(env);
+    old_type_checker tc(env);
     if (tc.is_prop(d.get_type()))
         return optional<name>(); // definition is a proposition, then do nothing
     expr const & v = d.get_value();
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 68dbad85b1..25b90f60d1 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "runtime/interrupt.h"
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/replace_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
@@ -154,7 +154,7 @@ public:
 };
 
 expr normalize(environment const & env, expr const & e, bool eta) {
-    type_checker ctx(env);
+    old_type_checker ctx(env);
     return normalize_fn(ctx, eta)(e);
 }
 
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index 7e04d3ec9e..f7cd01da60 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include <string>
 #include "runtime/sstream.h"
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
 #include "library/kernel_serializer.h"
 #include "library/scoped_ext.h"
 #include "library/reducible.h"
diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp
index 1b4bba7dec..cd1d357078 100644
--- a/src/library/sorry.cpp
+++ b/src/library/sorry.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/find_fn.h"
 #include "kernel/for_each_fn.h"
-#include "kernel/type_checker.h"
 #include "kernel/environment.h"
 #include "library/sorry.h"
 #include "library/constants.h"
diff --git a/src/library/string.cpp b/src/library/string.cpp
index 6253673760..8dba328503 100644
--- a/src/library/string.cpp
+++ b/src/library/string.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include <string>
 #include <algorithm>
 #include "runtime/utf8.h"
-#include "kernel/type_checker.h"
 #include "library/kernel_serializer.h"
 #include "library/string.h"
 #include "library/util.h"
diff --git a/src/library/tactic/eval.cpp b/src/library/tactic/eval.cpp
index f301b8e7de..90ec5a07f0 100644
--- a/src/library/tactic/eval.cpp
+++ b/src/library/tactic/eval.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/error_msgs.h"
 #include "library/trace.h"
 #include "library/util.h"
diff --git a/src/library/tactic/tactic_evaluator.cpp b/src/library/tactic/tactic_evaluator.cpp
index 347a965ac3..2287bc44a9 100644
--- a/src/library/tactic/tactic_evaluator.cpp
+++ b/src/library/tactic/tactic_evaluator.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/type_checker.h"
 #include "library/module.h"
 #include "library/trace.h"
 #include "library/annotation.h"
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index d50fdd84d0..a371fe6a40 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/fresh_name.h"
 #include "util/sexpr/option_declarations.h"
-#include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
 #include "library/constants.h"
 #include "library/type_context.h"
diff --git a/src/library/trace.cpp b/src/library/trace.cpp
index 44418b3975..55eec9f12b 100644
--- a/src/library/trace.cpp
+++ b/src/library/trace.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/sexpr/option_declarations.h"
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "library/io_state.h"
 #include "library/trace.h"
 #include "library/messages.h"
@@ -175,7 +175,7 @@ struct silent_ios_helper {
 };
 
 MK_THREAD_LOCAL_GET_DEF(silent_ios_helper, get_silent_ios_helper);
-MK_THREAD_LOCAL_GET(type_checker, get_dummy_tc, get_dummy_env());
+MK_THREAD_LOCAL_GET(old_type_checker, get_dummy_tc, get_dummy_env());
 
 scope_trace_silent::scope_trace_silent(bool flag) {
     m_old_value = g_silent;
diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index 215d1cf6a6..fff9f8de1b 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "runtime/sstream.h"
 #include "kernel/find_fn.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/util.h"
 #include "library/scoped_ext.h"
@@ -113,7 +113,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
         given_major_pos       = num_params + 1 /* motive */ + num_indices;
     }
     declaration d = env.get(r);
-    type_checker tc(env);
+    old_type_checker tc(env);
     buffer<expr> tele;
     expr rtype    = to_telescope(tc, d.get_type(), tele);
     buffer<expr> C_args;
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 63cb46b00c..720706552d 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
 #include "kernel/error_msgs.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/abstract_type_context.h"
 #include "kernel/inductive/inductive.h"
@@ -246,7 +246,7 @@ level get_datatype_level(environment const & env, expr const & ind_type) {
     if (is_sort(it)) {
         return sort_level(it);
     } else {
-        type_checker ctx(env);
+        old_type_checker ctx(env);
         buffer<expr> telescope;
         expr it = ctx.whnf(to_telescope(ctx, ind_type, telescope));
         if (is_sort(it)) {
@@ -312,7 +312,7 @@ optional<name> is_constructor_app_ext(environment const & env, expr const & e) {
     return is_constructor_app_ext(env, *it);
 }
 
-static bool is_irrelevant_field_type(type_checker & tc, expr const & ftype) {
+static bool is_irrelevant_field_type(old_type_checker & tc, expr const & ftype) {
     if (tc.is_prop(ftype)) return true;
     buffer<expr> tele;
     expr n_ftype = to_telescope(tc, ftype, tele);
@@ -325,7 +325,7 @@ void get_constructor_relevant_fields(environment const & env, name const & n, bu
     name I_name      = *inductive::is_intro_rule(env, n);
     unsigned nparams = *inductive::get_num_params(env, I_name);
     buffer<expr> telescope;
-    type_checker tc(env);
+    old_type_checker tc(env);
     to_telescope(tc, type, telescope);
     lean_assert(telescope.size() >= nparams);
     for (unsigned i = nparams; i < telescope.size(); i++) {
@@ -423,7 +423,7 @@ expr fun_to_telescope(expr const & e, buffer<expr> & telescope,
     return to_telescope(false, e, telescope, binfo);
 }
 
-expr to_telescope(type_checker & ctx, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
+expr to_telescope(old_type_checker & ctx, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
     expr new_type = ctx.whnf(type);
     while (is_pi(new_type)) {
         type = new_type;
@@ -1024,7 +1024,7 @@ expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_k
 }
 
 bool get_constructor_rec_args(environment const & env, expr const & e, buffer<pair<expr, unsigned>> & rec_args) {
-    type_checker ctx(env);
+    old_type_checker ctx(env);
     buffer<expr> args;
     expr const & fn = get_app_args(e, args);
     if (!is_constant(fn)) return false;
diff --git a/src/library/util.h b/src/library/util.h
index 92562099fe..b35627940b 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -153,7 +153,7 @@ expr to_telescope(expr const & type, buffer<expr> & telescope,
 expr fun_to_telescope(expr const & e, buffer<expr> & telescope, optional<binder_info> const & binfo);
 
 /** \brief Similar to previous procedure, but puts \c type in whnf */
-expr to_telescope(type_checker & ctx, expr type, buffer<expr> & telescope,
+expr to_telescope(old_type_checker & ctx, expr type, buffer<expr> & telescope,
                   optional<binder_info> const & binfo = optional<binder_info>());
 
 /** \brief Return the universe where inductive datatype resides
diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h
index 07fecce3dd..df0eefa36e 100644
--- a/src/library/vm/interaction_state_imp.h
+++ b/src/library/vm/interaction_state_imp.h
@@ -7,8 +7,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #pragma once
 #include "runtime/sstream.h"
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
+#include "kernel/old_type_checker.h"
 #include "library/profiling.h"
 #include "library/constants.h"
 #include "library/message_builder.h"
diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp
index 230beafbad..e040880d69 100644
--- a/src/library/vm/vm_environment.cpp
+++ b/src/library/vm/vm_environment.cpp
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include "library/unfold_macros.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "kernel/standard_kernel.h"
 #include "library/module.h"
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index b4c752dd9e..8c58b41466 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -27,7 +27,6 @@ Author: Leonardo de Moura
 #include "util/sexpr/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/type_checker.h"
 #include "kernel/formatter.h"
 #include "kernel/standard_kernel.h"
 #include "library/st_task_queue.h"
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 56dbee0a79..e440fef237 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "util/init_module.h"
 #include "util/sexpr/init_module.h"
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+#include "kernel/old_type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/init_module.h"
@@ -69,12 +69,12 @@ static void tst1() {
     expr Prop = mk_Prop();
     expr c  = mk_local("c", Prop);
     expr id = Const("id");
-    type_checker checker(env3);
+    old_type_checker checker(env3);
     lean_assert(checker.check(mk_app(id, Prop)) == Prop >> Prop);
     lean_assert(checker.whnf(mk_app(id, Prop, c)) == c);
     lean_assert(checker.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))) == c);
 
-    type_checker checker2(env2);
+    old_type_checker checker2(env2);
     lean_assert(checker2.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))) == mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c))));
 }