feat(library/type_context): add mk_subsingleton_instance

src/library/class_instance_resolution.cpp

@@ -195,17 +195,10 @@ optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<ex
     return mk_class_instance(tc.env(), ios, ctx, is_hset);
 }
 
-optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
+optional<expr> mk_subsingleton_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & type) {
     cienv & cenv = get_cienv();
-    cenv.ensure_compatible(tc.env(), ios, ctx);
-    flet<bool> set(cenv.m_ti_ptr->get_ignore_if_zero(), true);
-    level lvl    = sort_level(tc.ensure_type(type).first);
-    expr subsingleton;
-    if (is_standard(tc.env()))
-        subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type);
-    else
-        subsingleton = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)).first;
-    return cenv.m_ti_ptr->mk_class_instance(subsingleton);
+    cenv.ensure_compatible(env, ios, ctx);
+    return cenv.m_ti_ptr->mk_subsingleton_instance(type);
 }
 
 void initialize_class_instance_resolution() {

src/library/class_instance_resolution.h

@@ -38,7 +38,7 @@ pair<expr, constraint> mk_class_instance_elaborator(
 optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances);
 optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type);
 optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
-optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
+optional<expr> mk_subsingleton_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & type);
 
 void initialize_class_instance_resolution();
 void finalize_class_instance_resolution();

src/library/tactic/congruence_tactic.cpp

@@ -50,7 +50,7 @@ optional<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios
         if (prop.back()) {
             ss.push_back(true);
         } else {
-            ss.push_back(static_cast<bool>(mk_subsingleton_instance(tc, ios, ctx, mlocal_type(d))));
+            ss.push_back(static_cast<bool>(mk_subsingleton_instance(tc.env(), ios, ctx, mlocal_type(d))));
         }
         codomain_deps_on.push_back(depends_on(codomain, d));
         ctx = cons(d, ctx);
@@ -145,7 +145,7 @@ optional<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios
                 return none_expr();
             buffer<expr> hyps;
             g.get_hyps(hyps);
-            auto spr = mk_subsingleton_instance(tc, ios, to_list(hyps), mlocal_type(new_lhs));
+            auto spr = mk_subsingleton_instance(tc.env(), ios, to_list(hyps), mlocal_type(new_lhs));
             if (!spr)
                 return none_expr();
             expr new_eq    = mk_local(get_unused_name(name(h, eqidx), hyps), mk_eq(tc, new_rhs, new_lhs));

src/library/type_context.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/generic_exception.h"
 #include "library/class.h"
+#include "library/constants.h"
 
 #ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES
 #define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false
@@ -1610,6 +1611,19 @@ optional<expr> type_context::mk_class_instance(expr const & type) {
     return r;
 }
 
+optional<expr> type_context::mk_subsingleton_instance(expr const & type) {
+    expr Type  = whnf(infer(type));
+    if (!is_sort(Type))
+        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);
+}
+
 optional<expr> type_context::next_class_instance() {
     if (!m_ci_multiple_instances)
         return none_expr();
@@ -1751,6 +1765,11 @@ expr default_type_context::mk_mvar(expr const & type) {
     return mk_metavar(name(*g_prefix, idx), type);
 }
 
+optional<expr> default_type_context::mk_subsingleton_instance(expr const & type) {
+    flet<bool> set(m_ignore_if_zero, true);
+    return type_context::mk_subsingleton_instance(type);
+}
+
 bool default_type_context::ignore_universe_def_eq(level const & l1, level const & l2) const {
     if (is_meta(l1) || is_meta(l2)) {
         // The unifier may invoke this module before universe metavariables in the class

src/library/type_context.h

@@ -409,6 +409,10 @@ public:
     /** \brief Try to synthesize an instance of the type class \c type */
     optional<expr> mk_class_instance(expr const & type);
     optional<expr> next_class_instance();
+    /** \brief Try to synthesize an instance of (subsingleton type)
+        \remark This method is virtual because we need a refinement
+        at default_type_context to workaround an integration problem with the elaborator. */
+    virtual optional<expr> mk_subsingleton_instance(expr const & type);
 
     /** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
         ?m to (an abstraction of) v. Return true if success and false otherwise.
@@ -511,6 +515,8 @@ public:
     virtual void push() { m_trail.push_back(m_assignment); }
     virtual void pop() { lean_assert(!m_trail.empty()); m_assignment = m_trail.back(); m_trail.pop_back(); }
     virtual void commit() { lean_assert(!m_trail.empty()); m_trail.pop_back(); }
+    virtual optional<expr> mk_subsingleton_instance(expr const & type);
+    // TODO(REMOVE)
     bool & get_ignore_if_zero() { return m_ignore_if_zero; }
 };