diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 0d98e6d25..c9a10d9d4 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1223,6 +1223,7 @@ expr type_context::infer(expr const & e) {
 
 void type_context::clear_cache() {
     m_ci_cache.clear();
+    m_ss_cache.clear();
 }
 
 /** \brief If the constant \c e is a class, return its name */
@@ -1729,16 +1730,23 @@ optional<expr> type_context::mk_class_instance(expr const & type) {
 }
 
 optional<expr> type_context::mk_subsingleton_instance(expr const & type) {
+    auto it = m_ss_cache.find(type);
+    if (it != m_ss_cache.end())
+        return it->second;
     expr Type  = whnf(infer(type));
-    if (!is_sort(Type))
+    if (!is_sort(Type)) {
+        m_ss_cache.insert(mk_pair(type, none_expr()));
         return none_expr();
+    }
     level lvl    = sort_level(Type);
     expr subsingleton;
     if (is_standard(m_env))
         subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type);
     else
         subsingleton = whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type));
-    return mk_class_instance(subsingleton);
+    auto r = mk_class_instance(subsingleton);
+    m_ss_cache.insert(mk_pair(type, r));
+    return r;
 }
 
 optional<expr> type_context::next_class_instance() {
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 2ef8152a0..e02dd3be8 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -280,6 +280,9 @@ class type_context {
     bool                          m_ci_displayed_trace_header;
     optional<pos_info>            m_ci_pos;
 
+    /* subsingleton instance cache, we also cache failures */
+    expr_struct_map<optional<expr>> m_ss_cache;
+
     // configuration options
     unsigned                      m_ci_max_depth;
     bool                          m_ci_trans_instances;