diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 4ba9ab1b68..85b847b5dd 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -204,6 +204,26 @@ bool type_context::tmp_locals::all_let_decls() const {
    ===================== */
 MK_THREAD_LOCAL_GET_DEF(type_context_cache_manager, get_tcm);
 
+void type_context::cache_failure(expr const & t, expr const & s) {
+    if (t.hash() <= s.hash())
+        get_failure_cache().insert(mk_pair(t, s));
+    else
+        get_failure_cache().insert(mk_pair(s, t));
+}
+
+bool type_context::is_cached_failure(expr const & t, expr const & s) {
+    type_context_cache::failure_cache fcache = get_failure_cache();
+    if (t.hash() < s.hash()) {
+        return fcache.find(mk_pair(t, s)) != fcache.end();
+    } else if (t.hash() > s.hash()) {
+        return fcache.find(mk_pair(s, t)) != fcache.end();
+    } else {
+        return
+            fcache.find(mk_pair(t, s)) != fcache.end() ||
+            fcache.find(mk_pair(s, t)) != fcache.end();
+    }
+}
+
 void type_context::init_local_instances() {
     m_local_instances = list<pair<name, expr>>();
     m_lctx.for_each([&](local_decl const & decl) {
@@ -2632,13 +2652,15 @@ bool type_context::is_def_eq_core_core(expr const & t, expr const & s) {
     if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
         return true;
 
-    if (is_app(t_n) && is_app(s_n)) {
+    if (is_app(t_n) && is_app(s_n) && !is_cached_failure(t_n, s_n)) {
         scope s(*this);
         if (is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) &&
             is_def_eq_args(t_n, s_n) &&
             process_postponed(s)) {
             s.commit();
             return true;
+        } else if (!has_expr_metavar(t_n) && !has_expr_metavar(s_n)) {
+            cache_failure(t_n, s_n);
         }
     }
 
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 95c26672bd..d5b25239c8 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -42,6 +42,8 @@ class type_context_cache {
     typedef expr_struct_map<expr> whnf_cache;
     typedef expr_struct_map<optional<expr>> instance_cache;
     typedef expr_struct_map<optional<expr>> subsingleton_cache;
+    typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> failure_cache;
+
     environment                   m_env;
     options                       m_options;
     name_map<projection_info>     m_proj_info;
@@ -77,6 +79,8 @@ class type_context_cache {
 
     equiv_manager                 m_equiv_manager[4];
 
+    failure_cache                 m_failure_cache[4];
+
     whnf_cache                    m_whnf_cache[4];
 
     name2bool                     m_aux_recursor_cache;
@@ -275,6 +279,10 @@ class type_context : public abstract_type_context {
         if (is_equiv_cache_target(e1, e2)) get_equiv_cache().add_equiv(e1, e2);
     }
 
+    type_context_cache::failure_cache & get_failure_cache() { return m_cache->m_failure_cache[static_cast<unsigned>(m_transparency_mode)]; }
+    void cache_failure(expr const & t, expr const & s);
+    bool is_cached_failure(expr const & t, expr const & s);
+
     void init_local_instances();
     void flush_instance_cache();
     void update_local_instances(expr const & new_local, expr const & new_type);