diff --git a/src/library/abstract_context_cache.cpp b/src/library/abstract_context_cache.cpp
index f366d00015..d65f1d894c 100644
--- a/src/library/abstract_context_cache.cpp
+++ b/src/library/abstract_context_cache.cpp
@@ -49,14 +49,14 @@ bool get_smart_unfolding(options const & o) {
     return o.get_bool(*g_smart_unfolding, LEAN_DEFAULT_SMART_UNFOLDING);
 }
 
-abstract_context_cache::abstract_context_cache():
+context_cacheless::context_cacheless():
     m_unfold_lemmas(LEAN_DEFAULT_UNFOLD_LEMMAS),
     m_nat_offset_cnstr_threshold(LEAN_DEFAULT_NAT_OFFSET_CNSTR_THRESHOLD),
     m_smart_unfolding(LEAN_DEFAULT_SMART_UNFOLDING),
     m_class_instance_max_depth(LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH) {
 }
 
-abstract_context_cache::abstract_context_cache(options const & o):
+context_cacheless::context_cacheless(options const & o):
     m_options(o),
     m_unfold_lemmas(::lean::get_unfold_lemmas(o)),
     m_nat_offset_cnstr_threshold(::lean::get_nat_offset_cnstr_threshold(o)),
@@ -64,15 +64,15 @@ abstract_context_cache::abstract_context_cache(options const & o):
     m_class_instance_max_depth(::lean::get_class_instance_max_depth(o)) {
 }
 
-abstract_context_cache::abstract_context_cache(abstract_context_cache const & c, bool):
-    m_options(c.m_options),
-    m_unfold_lemmas(c.m_unfold_lemmas),
-    m_nat_offset_cnstr_threshold(c.m_nat_offset_cnstr_threshold),
-    m_smart_unfolding(c.m_smart_unfolding),
-    m_class_instance_max_depth(c.m_class_instance_max_depth) {
+context_cacheless::context_cacheless(abstract_context_cache const & c, bool):
+    m_options(c.get_options()),
+    m_unfold_lemmas(c.get_unfold_lemmas()),
+    m_nat_offset_cnstr_threshold(c.get_nat_offset_cnstr_threshold()),
+    m_smart_unfolding(c.get_smart_unfolding()),
+    m_class_instance_max_depth(c.get_class_instance_max_depth()) {
 }
 
-bool abstract_context_cache::is_transparent(type_context & ctx, transparency_mode m, declaration const & d) {
+bool context_cacheless::is_transparent(type_context & ctx, transparency_mode m, declaration const & d) {
     if (m == transparency_mode::None)
         return false;
     name const & n = d.get_name();
@@ -92,7 +92,7 @@ bool abstract_context_cache::is_transparent(type_context & ctx, transparency_mod
     return false;
 }
 
-optional<declaration> abstract_context_cache::get_decl(type_context & ctx, transparency_mode m, name const & n) {
+optional<declaration> context_cacheless::get_decl(type_context & ctx, transparency_mode m, name const & n) {
     if (auto d = ctx.env().find(n)) {
         if (d->is_definition() && is_transparent(ctx, m, *d)) {
             return d;
@@ -101,11 +101,11 @@ optional<declaration> abstract_context_cache::get_decl(type_context & ctx, trans
     return optional<declaration>();
 }
 
-projection_info const * abstract_context_cache::get_proj_info(type_context & ctx, name const & n) {
+projection_info const * context_cacheless::get_proj_info(type_context & ctx, name const & n) {
     return get_projection_info(ctx.env(), n);
 }
 
-bool abstract_context_cache::get_aux_recursor(type_context & ctx, name const & n) {
+bool context_cacheless::get_aux_recursor(type_context & ctx, name const & n) {
     return ::lean::is_aux_recursor(ctx.env(), n);
 }
 
diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h
index 68db949d76..04cf12030f 100644
--- a/src/library/abstract_context_cache.h
+++ b/src/library/abstract_context_cache.h
@@ -60,9 +60,6 @@ struct app_builder_info {
    In the type_context, we cache inferred types, whnf, type class instances,
    to cite a few.
 
-   This class do not implement any cache, only its interface. All operations
-   do nothing.
-
    This class has been added to address problems with the former `type_context_cache_manager`.
    The `type_context_cache_manager` objects were stored in thread local objects.
    The correctness of this cache relied on the fact we used to never reuse fresh names in the whole system.
@@ -162,21 +159,8 @@ struct app_builder_info {
      * A tactic that reverses local instances
 */
 class abstract_context_cache {
-protected:
-    options                   m_options;
-    bool                      m_unfold_lemmas;
-    unsigned                  m_nat_offset_cnstr_threshold;
-    unsigned                  m_smart_unfolding;
-    unsigned                  m_class_instance_max_depth;
-    optional<local_instances> m_local_instances;
-    bool is_transparent(type_context & ctx, transparency_mode m, declaration const & d);
 public:
-    abstract_context_cache();
-    abstract_context_cache(options const &);
-    /* Create a "dummy" context_cache with the same configuration options.
-       The bool parameter is not used. It is here just to make sure we don't confuse
-       this constructor with the copy constructor. */
-    abstract_context_cache(abstract_context_cache const &, bool);
+    abstract_context_cache() {}
     abstract_context_cache(abstract_context_cache const &) = delete;
     abstract_context_cache(abstract_context_cache &&) = default;
     virtual ~abstract_context_cache() {}
@@ -185,11 +169,126 @@ public:
     abstract_context_cache & operator=(abstract_context_cache &&) = default;
 
     /* Cached configuration options */
-    options const & get_options() const { return m_options; }
-    bool get_unfold_lemmas() const { return m_unfold_lemmas; }
-    unsigned get_nat_offset_cnstr_threshold() const { return m_nat_offset_cnstr_threshold; }
-    unsigned get_smart_unfolding() const { return m_smart_unfolding; }
-    unsigned get_class_instance_max_depth() const { return m_class_instance_max_depth; }
+    virtual options const & get_options() const = 0;
+    virtual bool get_unfold_lemmas() const = 0;
+    virtual unsigned get_nat_offset_cnstr_threshold() const = 0;
+    virtual unsigned get_smart_unfolding() const = 0;
+    virtual unsigned get_class_instance_max_depth() const = 0;
+
+    /* Operations for accessing environment data more efficiently.
+       The default implementation provided by this class does not have any optimization. */
+
+    virtual optional<declaration> get_decl(type_context &, transparency_mode, name const &) = 0;
+    virtual projection_info const * get_proj_info(type_context &, name const &) = 0;
+    virtual bool get_aux_recursor(type_context &, name const &) = 0;
+
+    /* Cache support for type_context module */
+
+    virtual optional<expr> get_infer(expr const &) = 0;
+    virtual void set_infer(expr const &, expr const &) = 0;
+
+    virtual bool get_equiv(transparency_mode, expr const &, expr const &) = 0;
+    virtual void set_equiv(transparency_mode, expr const &, expr const &) = 0;
+
+    virtual bool get_is_def_eq_failure(transparency_mode, expr const &, expr const &) = 0;
+    virtual void set_is_def_eq_failure(transparency_mode, expr const &, expr const &) = 0;
+
+    virtual optional<expr> get_whnf(transparency_mode, expr const &) = 0;
+    virtual void set_whnf(transparency_mode, expr const &, expr const &) = 0;
+
+    virtual optional<optional<expr>> get_instance(expr const &) = 0;
+    virtual void set_instance(expr const &, optional<expr> const &) = 0;
+
+    virtual optional<optional<expr>> get_subsingleton(expr const &) = 0;
+    virtual void set_subsingleton(expr const &, optional<expr> const &) = 0;
+
+    /* this method should flush the instance and subsingleton cache */
+    virtual void flush_instances() = 0;
+
+    virtual void reset_frozen_local_instances() = 0;
+    virtual void set_frozen_local_instances(local_instances const & lis) = 0;
+    virtual optional<local_instances> get_frozen_local_instances() const = 0;
+
+    /* Cache support for fun_info module */
+
+    virtual optional<fun_info> get_fun_info(type_context &, expr const &) = 0;
+    virtual void set_fun_info(type_context &, expr const &, fun_info const &) = 0;
+
+    virtual optional<fun_info> get_fun_info_nargs(type_context &, expr const &, unsigned) = 0;
+    virtual void set_fun_info_nargs(type_context &, expr const &, unsigned, fun_info const &) = 0;
+
+    virtual optional<unsigned> get_specialization_prefix_size(type_context &, expr const &, unsigned) = 0;
+    virtual void set_specialization_prefix_size(type_context &, expr const &, unsigned, unsigned) = 0;
+
+    virtual optional<ss_param_infos> get_subsingleton_info(type_context &, expr const &) = 0;
+    virtual void set_subsingleton_info(type_context &, expr const &, ss_param_infos const &) = 0;
+
+    virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context &, expr const &, unsigned) = 0;
+    virtual void set_subsingleton_info_nargs(type_context &, expr const &, unsigned, ss_param_infos const &) = 0;
+
+    virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context &, expr const &, unsigned) = 0;
+    virtual void set_specialization_subsingleton_info_nargs(type_context &, expr const &, unsigned, ss_param_infos const &) = 0;
+
+    /* Cache support for congr_lemma module */
+
+    virtual optional<congr_lemma> get_simp_congr_lemma(type_context &, expr const &, unsigned) = 0;
+    virtual void set_simp_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
+
+    virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context &, expr const &, unsigned) = 0;
+    virtual void set_specialized_simp_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
+
+    virtual optional<congr_lemma> get_congr_lemma(type_context &, expr const &, unsigned) = 0;
+    virtual void set_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
+
+    virtual optional<congr_lemma> get_specialized_congr_lemma(type_context &, expr const &, unsigned) = 0;
+    virtual void set_specialized_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
+
+    virtual optional<congr_lemma> get_hcongr_lemma(type_context &, expr const &, unsigned) = 0;
+    virtual void set_hcongr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
+
+    /* Cache support for app_builder */
+
+    virtual optional<app_builder_info> get_app_builder_info(type_context &, expr const &, unsigned) = 0;
+    virtual void set_app_builder_info(type_context &, expr const &, unsigned, app_builder_info const &) = 0;
+
+    virtual optional<app_builder_info> get_app_builder_info(type_context &, expr const &, list<bool> const &) = 0;
+    virtual void set_app_builder_info(type_context &, expr const &, list<bool> const &, app_builder_info const &) = 0;
+};
+
+/* Dummy implementation of the abstract_context_cache interface that does not do cache anything but configuration options. */
+class context_cacheless : public abstract_context_cache {
+protected:
+    bool is_transparent(type_context & ctx, transparency_mode m, declaration const & d);
+private:
+    options                   m_options;
+    bool                      m_unfold_lemmas;
+    unsigned                  m_nat_offset_cnstr_threshold;
+    unsigned                  m_smart_unfolding;
+    unsigned                  m_class_instance_max_depth;
+    optional<local_instances> m_local_instances;
+public:
+    context_cacheless();
+    context_cacheless(options const &);
+    /* Faster version of `context_cacheless(c.get_options())`.
+       The bool parameter is not used. It is here just to make sure we don't confuse
+       this constructor with the copy constructor. */
+    context_cacheless(abstract_context_cache const &, bool);
+    context_cacheless(context_cacheless const &) = delete;
+    context_cacheless(context_cacheless &&) = default;
+    virtual ~context_cacheless() {}
+
+    context_cacheless & operator=(context_cacheless const &) = delete;
+    context_cacheless & operator=(context_cacheless &&) = default;
+
+    virtual options const & get_options() const override { return m_options; }
+    virtual bool get_unfold_lemmas() const override { return m_unfold_lemmas; }
+    virtual unsigned get_nat_offset_cnstr_threshold() const override  { return m_nat_offset_cnstr_threshold; }
+    virtual unsigned get_smart_unfolding() const override  { return m_smart_unfolding; }
+    virtual unsigned get_class_instance_max_depth() const override  { return m_class_instance_max_depth; }
+
+    virtual void reset_frozen_local_instances() override { m_local_instances = optional<local_instances>(); }
+    virtual void set_frozen_local_instances(local_instances const & lis) override { m_local_instances = lis; }
+    virtual optional<local_instances> get_frozen_local_instances() const override { return m_local_instances; }
 
     /* Operations for accessing environment data more efficiently.
        The default implementation provided by this class does not have any optimization. */
@@ -218,13 +317,8 @@ public:
     virtual optional<optional<expr>> get_subsingleton(expr const &) { return optional<optional<expr>>(); }
     virtual void set_subsingleton(expr const &, optional<expr> const &) {}
 
-    /* this method should flush the instance and subsingleton cache */
     virtual void flush_instances() {}
 
-    void reset_frozen_local_instances() { m_local_instances = optional<local_instances>(); }
-    void set_frozen_local_instances(local_instances const & lis) { m_local_instances = lis; }
-    optional<local_instances> get_frozen_local_instances() const { return m_local_instances; }
-
     /* Cache support for fun_info module */
 
     virtual optional<fun_info> get_fun_info(type_context &, expr const &) { return optional<fun_info>(); }
diff --git a/src/library/context_cache.cpp b/src/library/context_cache.cpp
index 200479653e..4173b740fc 100644
--- a/src/library/context_cache.cpp
+++ b/src/library/context_cache.cpp
@@ -8,11 +8,11 @@ Author: Leonardo de Moura
 
 namespace lean {
 context_cache::context_cache():
-    abstract_context_cache() {
+    context_cacheless() {
 }
 
 context_cache::context_cache(options const & o):
-    abstract_context_cache(o) {
+    context_cacheless(o) {
 }
 
 context_cache::~context_cache() {
@@ -24,21 +24,21 @@ optional<declaration> context_cache::get_decl(type_context & ctx, transparency_m
     if (it != cache.end()) {
         return it->second;
     }
-    optional<declaration> r = abstract_context_cache::get_decl(ctx, m, n);
+    optional<declaration> r = context_cacheless::get_decl(ctx, m, n);
     cache.insert(mk_pair(n, r));
     return r;
 }
 
 projection_info const * context_cache::get_proj_info(type_context & ctx, name const & n) {
     // TODO(Leo): check if we really need a cache for get_proj_info
-    return abstract_context_cache::get_proj_info(ctx, n);
+    return context_cacheless::get_proj_info(ctx, n);
 }
 
 bool context_cache::get_aux_recursor(type_context & ctx, name const & n) {
     auto it = m_aux_recursor_cache.find(n);
     if (it != m_aux_recursor_cache.end())
         return it->second;
-    bool r = abstract_context_cache::get_aux_recursor(ctx, n);
+    bool r = context_cacheless::get_aux_recursor(ctx, n);
     m_aux_recursor_cache.insert(mk_pair(n, r));
     return r;
 }
diff --git a/src/library/context_cache.h b/src/library/context_cache.h
index 2b07145d14..b9ce2dd89b 100644
--- a/src/library/context_cache.h
+++ b/src/library/context_cache.h
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "library/abstract_context_cache.h"
 
 namespace lean {
-class context_cache : public abstract_context_cache {
+class context_cache : public context_cacheless {
     typedef std::unordered_map<name, optional<declaration>, name_hash> transparency_cache;
     typedef std::unordered_map<name, bool, name_hash> name2bool;
 
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index d350a107d2..3b2bbbb744 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2295,7 +2295,7 @@ optional<expr> type_context::mk_class_instance_at(local_context const & lctx, ex
         m_cache->get_frozen_local_instances() == lctx.get_frozen_local_instances()) {
         return mk_class_instance(type);
     } else {
-        abstract_context_cache tmp_cache(*m_cache, true);
+        context_cacheless tmp_cache(*m_cache, true);
         type_context tmp_ctx(env(), m_mctx, lctx, tmp_cache, m_transparency_mode);
         auto r = tmp_ctx.mk_class_instance(type);
         if (r)
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 886118c3b3..e1c9e7439d 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -387,10 +387,11 @@ public:
 private:
     typedef buffer<scope_data> scopes;
     typedef abstract_context_cache cache;
+    typedef context_cacheless dummy_cache;
     environment        m_env;
     metavar_context    m_mctx;
     local_context      m_lctx;
-    cache              m_dummy_cache; /* cache used when user does not provide a cache */
+    dummy_cache        m_dummy_cache; /* cache used when user does not provide a cache */
     cache *            m_cache;
     local_instances    m_local_instances;
     /* We only cache results when m_used_assignment is false */