feat(library,frontends/lean): add support for projections in the elaborator

The idea is to simulate the computation rules such as

    pr1 (mk a b) ==> a

in the elaborator

src/frontends/lean/structure_cmd.cpp

@@ -806,11 +806,7 @@ struct structure_cmd_fn {
             for (unsigned idx : fmap) {
                 expr const & field = m_fields[idx];
                 name proj_name = m_name + mlocal_name(field);
-                expr proj;
-                if (m_env.trust_lvl() == 0)
-                    proj = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), st);
-                else
-                    proj = mk_projection_macro(proj_name, st);
+                expr proj      = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), st);
                 coercion_value     = mk_app(coercion_value, proj);
             }
             coercion_value                 = Fun(m_params, Fun(st, coercion_value));

src/library/projection.cpp

@@ -188,6 +188,134 @@ expr mk_projection_macro(name const & proj_name, expr const & e) {
     return mk_macro(def, 1, &e);
 }
 
+projection_info const * projection_converter::is_projection(expr const & e) const {
+    expr const & f = get_app_fn(e);
+    if (is_constant(f))
+        return m_proj_info.find(const_name(f));
+    else
+        return nullptr;
+}
+
+bool projection_converter::is_opaque(declaration const & d) const {
+    return m_proj_info.find(d.get_name()) != nullptr;
+}
+
+optional<pair<expr, constraint_seq>> projection_converter::reduce_projection(expr const & t) {
+    projection_info const * info = is_projection(t);
+    if (!info)
+        return optional<pair<expr, constraint_seq>>();
+    buffer<expr> args;
+    get_app_args(t, args);
+    if (args.size() <= info->m_nparams) {
+        return optional<pair<expr, constraint_seq>>();
+    }
+    unsigned mkidx  = info->m_nparams;
+    expr const & mk = args[mkidx];
+    pair<expr, constraint_seq> new_mk_cs = whnf(mk);
+    expr new_mk     = new_mk_cs.first;
+    expr const & new_mk_fn = get_app_fn(new_mk);
+    if (!is_constant(new_mk_fn) || const_name(new_mk_fn) != info->m_constructor) {
+        return optional<pair<expr, constraint_seq>>();
+    }
+    buffer<expr> mk_args;
+    get_app_args(new_mk, mk_args);
+    unsigned i = info->m_nparams + info->m_i;
+    if (i >= mk_args.size()) {
+        return optional<pair<expr, constraint_seq>>();
+    }
+    expr r = mk_args[i];
+    r = mk_app(r, args.size() - mkidx - 1, args.data() + mkidx + 1);
+    return optional<pair<expr, constraint_seq>>(r, new_mk_cs.second);
+}
+
+optional<pair<expr, constraint_seq>> projection_converter::norm_ext(expr const & e) {
+    if (auto r = reduce_projection(e)) {
+        return r;
+    } else {
+        return default_converter::norm_ext(e);
+    }
+}
+
+bool projection_converter::postpone_is_def_eq(expr const & t, expr const & s) {
+    if (has_expr_metavar(t) || has_expr_metavar(s)) {
+        auto it1 = is_projection(t);
+        auto it2 = is_projection(s);
+        if (it1 && it2) {
+            return true;
+        }
+        if (it1 && is_stuck(t, *m_tc))
+            return true;
+        if (it2 && is_stuck(s, *m_tc))
+            return true;
+    }
+    return default_converter::postpone_is_def_eq(t, s);
+}
+
+// Apply lazy delta-reduction and then normalizer extensions
+lbool projection_converter::reduce_def_eq(expr & t_n, expr & s_n, constraint_seq & cs) {
+    while (true) {
+        // first, keep applying lazy delta-reduction while applicable
+        lbool r = lazy_delta_reduction(t_n, s_n, cs);
+        if (r != l_undef) return r;
+
+        auto p_t = reduce_projection(t_n);
+        auto p_s = reduce_projection(s_n);
+        if (p_t && p_s) {
+            t_n = whnf_core(p_t->first);
+            s_n = whnf_core(p_s->first);
+            cs += p_t->second;
+            cs += p_s->second;
+        } else if (p_t || p_s) {
+            expr const & f_t = get_app_fn(t_n);
+            expr const & f_s = get_app_fn(s_n);
+            if (is_constant(f_t) && is_constant(f_s) && const_name(f_t) == const_name(f_s) &&
+                (p_t || is_stuck(t_n, *m_tc)) && (p_s || is_stuck(s_n, *m_tc))) {
+                // treat it as a delta-delta step
+                return l_undef;
+            }
+            if (p_t) {
+                t_n = whnf_core(p_t->first);
+                cs += p_t->second;
+            } else if (p_s) {
+                s_n = whnf_core(p_s->first);
+                cs += p_s->second;
+            } else {
+                lean_unreachable();
+            }
+        } else {
+            auto new_t_n = d_norm_ext(t_n, cs);
+            auto new_s_n = d_norm_ext(s_n, cs);
+            if (!new_t_n && !new_s_n)
+                return l_undef;
+            if (new_t_n) {
+                t_n = whnf_core(*new_t_n);
+            }
+            if (new_s_n) {
+                s_n = whnf_core(*new_s_n);
+            }
+        }
+        r = quick_is_def_eq(t_n, s_n, cs);
+        if (r != l_undef) return r;
+    }
+}
+
+optional<expr> projection_converter::is_stuck(expr const & e, type_checker & c) {
+    projection_info const * info = is_projection(e);
+    if (!info)
+        return default_converter::is_stuck(e, c);
+    buffer<expr> args;
+    get_app_args(e, args);
+    if (args.size() <= info->m_nparams)
+        return none_expr();
+    expr mk = whnf(args[info->m_nparams], c).first;
+    return c.is_stuck(mk);
+}
+
+projection_converter::projection_converter(environment const & env):
+    default_converter(env, true) {
+    m_proj_info = ::lean::get_extension(env).m_info;
+}
+
 void initialize_projection() {
     g_ext      = new projection_ext_reg();
     g_proj_key = new std::string("proj");

src/library/projection.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
+#include "kernel/default_converter.h"
 
 namespace lean {
 /** \brief Auxiliary information attached to projections. This information
@@ -62,6 +63,19 @@ expr mk_projection_macro(name const & proj_name, expr const & e);
 */
 bool is_structure_like(environment const & env, name const & S);
 
+class projection_converter : public default_converter {
+    name_map<projection_info> m_proj_info;
+    projection_info const * is_projection(expr const & e) const;
+    optional<pair<expr, constraint_seq>> reduce_projection(expr const & t);
+    virtual optional<pair<expr, constraint_seq>> norm_ext(expr const & e);
+    virtual lbool reduce_def_eq(expr & t_n, expr & s_n, constraint_seq & cs);
+    virtual bool postpone_is_def_eq(expr const & t, expr const & s);
+public:
+    projection_converter(environment const & env);
+    virtual bool is_opaque(declaration const & d) const;
+    virtual optional<expr> is_stuck(expr const & e, type_checker & c);
+};
+
 void initialize_projection();
 void finalize_projection();
 }

src/library/tactic/expr_to_tactic.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/num.h"
 #include "library/constants.h"
+#include "library/projection.h"
 #include "library/kernel_serializer.h"
 #include "library/tactic/expr_to_tactic.h"
 
@@ -263,19 +264,19 @@ optional<unsigned> get_optional_unsigned(type_checker & tc, expr const & e) {
     throw expr_to_tactic_exception(e, "invalid tactic, argument is not an option num");
 }
 
-class tac_builtin_opaque_converter : public default_converter {
+class tac_builtin_opaque_converter : public projection_converter {
 public:
-    tac_builtin_opaque_converter(environment const & env):default_converter(env) {}
+    tac_builtin_opaque_converter(environment const & env):projection_converter(env) {}
     virtual bool is_opaque(declaration const & d) const {
         name n = d.get_name();
         if (!is_prefix_of(get_tactic_name(), n))
-            return default_converter::is_opaque(d);
+            return projection_converter::is_opaque(d);
         expr v = d.get_value();
         while (is_lambda(v))
             v = binding_body(v);
         if (is_constant(v) && const_name(v) == get_tactic_builtin_name())
             return true;
-        return default_converter::is_opaque(d);
+        return projection_converter::is_opaque(d);
     }
 };
 

src/library/tactic/rewrite_tactic.cpp

@@ -609,12 +609,12 @@ class rewrite_fn {
         return m_g.mk_meta(m_ngen.next(), type);
     }
 
-    class rewriter_converter : public default_converter {
+    class rewriter_converter : public projection_converter {
         list<name> const & m_to_unfold;
         bool             & m_unfolded;
     public:
         rewriter_converter(environment const & env, list<name> const & to_unfold, bool & unfolded):
-            default_converter(env),
+            projection_converter(env),
             m_to_unfold(to_unfold), m_unfolded(unfolded) {}
         virtual bool is_opaque(declaration const & d) const {
             if (std::find(m_to_unfold.begin(), m_to_unfold.end(), d.get_name()) != m_to_unfold.end()) {
@@ -1212,7 +1212,8 @@ class rewrite_fn {
                 src = app_arg(rule_type);
             else
                 src = app_arg(app_fn(rule_type));
-            if (!m_tc->is_def_eq(t, src, justification(), cs_seq)) {
+            if (!m_tc->is_def_eq(t, src, justification(), cs_seq) ||
+                !m_tc->is_def_eq_types(t, src, justification(), cs_seq)) {
                 add_target_failure(src, t, failure::Unification);
                 return unify_result();
             }
@@ -1535,7 +1536,7 @@ class rewrite_fn {
             return mk_opaque_type_checker(m_env, m_ngen.mk_child());
         } else {
             auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_reducible_pred(m_env);
-            return mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) {
+            return mk_simple_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) {
                     return is_projection(m_env, n) || aux_pred(n);
                 });
         }

src/library/unifier.cpp

@@ -32,6 +32,8 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/print.h"
 #include "library/expr_lt.h"
+#include "library/projection.h"
+#include "library/coercion.h"
 
 #ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS
 #define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000
@@ -925,6 +927,46 @@ struct unifier_fn {
             return is_owned(cnstr_rhs_expr(c));
     }
 
+    static status to_status(bool b) { return b ? Solved : Failed; }
+
+    status reduce_both_proj_and_check(expr const & lhs, expr const & rhs, justification const & j) {
+        lean_assert(is_projection_app(lhs));
+        lean_assert(is_projection_app(rhs));
+        constraint_seq new_cs;
+        expr new_lhs = whnf(lhs, new_cs);
+        expr new_rhs = whnf(rhs, new_cs);
+        if (lhs != new_lhs || rhs != new_rhs)
+            return to_status(is_def_eq(new_lhs, new_rhs, j) && process_constraints(new_cs));
+        if (const_name(get_app_fn(lhs)) != const_name(get_app_fn(rhs))) {
+            // Two projection applications
+            //     pr_1 ... =?= pr_2 ...
+            // where pr_1 != pr_2 and both are not stuck
+            set_conflict(j);
+            return Failed;
+        } else {
+            return Continue;
+        }
+    }
+
+    status reduce_proj_and_check(expr const & lhs, expr const & rhs, justification const & j) {
+        lean_assert(is_projection_app(lhs));
+        lean_assert(!is_projection_app(rhs));
+        {
+            // First try to reduce projection
+            constraint_seq new_cs;
+            expr new_lhs = whnf(lhs, new_cs);
+            if (lhs != new_lhs)
+                return to_status(is_def_eq(new_lhs, rhs, j) && process_constraints(new_cs));
+        }
+        {
+            constraint_seq new_cs;
+            expr new_rhs = whnf(rhs, new_cs);
+            if (rhs != new_rhs)
+                return to_status(is_def_eq(lhs, new_rhs, j) && process_constraints(new_cs));
+        }
+        return Continue;
+    }
+
     /** \brief Process an equality constraints. */
     bool process_eq_constraint(constraint const & c) {
         lean_assert(is_eq_cnstr(c));
@@ -944,34 +986,61 @@ struct unifier_fn {
 
         expr const & lhs = cnstr_lhs_expr(c);
         expr const & rhs = cnstr_rhs_expr(c);
+        bool is_proj_lhs = is_projection_app(lhs);
+        bool is_proj_rhs = is_projection_app(rhs);
+        bool is_proj_stuck_lhs = is_proj_lhs && m_tc->is_stuck(lhs);
+        bool is_proj_stuck_rhs = is_proj_rhs && m_tc->is_stuck(rhs);
+
+        if (is_proj_lhs && is_proj_rhs && !is_proj_stuck_lhs && !is_proj_stuck_rhs) {
+            if (const_name(get_app_fn(lhs)) == const_name(get_app_fn(rhs))) {
+                return process_same_projection_projection(c);
+            } else {
+                st = reduce_both_proj_and_check(lhs, rhs, c.get_justification());
+                if (st != Continue) return st == Solved;
+            }
+        } else if (is_proj_lhs && !is_proj_stuck_lhs && !is_proj_rhs && !is_meta(rhs)) {
+            st = reduce_proj_and_check(lhs, rhs, c.get_justification());
+            if (st != Continue) return st == Solved;
+        } else if (is_proj_rhs && !is_proj_stuck_rhs && !is_proj_lhs && !is_meta(lhs)) {
+            st = reduce_proj_and_check(rhs, lhs, c.get_justification());
+            if (st != Continue) return st == Solved;
+        }
 
         if (is_eq_deltas(lhs, rhs)) {
             // we need to create a backtracking point for this one
             add_cnstr(c, cnstr_group::Basic);
+            return true;
         } else if (is_meta(lhs) && is_meta(rhs)) {
             // flex-flex constraints are delayed the most.
             unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
             add_meta_occ(lhs, cidx);
             add_meta_occ(rhs, cidx);
+            return true;
         } else if (m_tc->may_reduce_later(lhs) ||
                    m_tc->may_reduce_later(rhs) ||
                    m_plugin->delay_constraint(*m_tc, c)) {
             unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
             add_meta_occs(lhs, cidx);
             add_meta_occs(rhs, cidx);
+            if (is_proj_lhs && is_proj_rhs)
+                return preprocess_projection_projection(c);
+            else
+                return true;
         } else if (is_meta(lhs)) {
             // flex-rigid constraints are delayed.
             unsigned cidx = add_cnstr(c, cnstr_group::FlexRigid);
             add_meta_occ(lhs, cidx);
+            return true;
         } else if (is_meta(rhs)) {
             // flex-rigid constraints are delayed.
             unsigned cidx = add_cnstr(c, cnstr_group::FlexRigid);
             add_meta_occ(rhs, cidx);
+            return true;
         } else {
             // this constraints require the unifier plugin to be solved
             add_cnstr(c, cnstr_group::Basic);
+            return true;
         }
-        return true;
     }
 
     /**
@@ -1240,6 +1309,112 @@ struct unifier_fn {
         return lazy_list<constraints>(cs.to_list());
     }
 
+    /** Return true iff t is a projection application */
+    bool is_projection_app(expr const & t) {
+        expr const & f = get_app_fn(t);
+        return is_constant(f) && is_projection(m_env, const_name(f));
+    }
+
+    // See #preprocess_projection_projection
+    bool is_preprocess_projection_projection_target(projection_info const * info, buffer<expr> const & args) {
+        if (!info->m_inst_implicit)
+            return false;
+        if (args.size() < info->m_nparams+1)
+            return false;
+        unsigned sidx = info->m_nparams;
+        if (!has_expr_metavar(args[sidx]))
+            return false;
+        for (unsigned i = 0; i < info->m_nparams; i++)
+            if (has_expr_metavar(args[i]))
+                return true;
+        // all parameters do not have metavariables, thus type class resolution will be triggered
+        // to synthesize the args[sidx]
+        return false;
+    }
+
+    /**
+      For constraints of the form
+        pr_1 A_1 s_1 a_1 =?= pr_2 A_2 s_2 a_2
+      where pr is a projection, A_{1,2} are parameters, s_{1,2} the structure, and a_{1,2} arguments.
+      If s_1/A_1 or s_2/A_2 contain metavariables, we add the constraint
+          infer_type(pr_1 A_1 s_1) =?= infer_type(pr_2 A_2 s_2)
+      when pr_{1,2} is the projection of a class. The new constraint may force some of the meta-variables occurring
+      in the parameters to be assigned, and then this assignment will trigger type class resolution at s_{1,2}
+
+      \remark Note that whenever we use this step we may be missing solutions.
+      This should only happen in very unusual circumstances. We may add an option to disable this
+      step in the future. This step is essential for processing the algebraic hierarchy.
+    */
+    bool preprocess_projection_projection(constraint const & c) {
+        expr const & lhs = cnstr_lhs_expr(c);
+        expr const & rhs = cnstr_rhs_expr(c);
+        lean_assert(is_projection_app(lhs) && is_projection_app(rhs));
+        buffer<expr> lhs_args, rhs_args;
+        expr const & f_lhs = get_app_args(lhs, lhs_args);
+        expr const & f_rhs = get_app_args(rhs, rhs_args);
+        projection_info const * info_lhs = get_projection_info(m_env, const_name(f_lhs));
+        projection_info const * info_rhs = get_projection_info(m_env, const_name(f_rhs));
+        lean_assert(info_lhs);
+        lean_assert(info_rhs);
+        if (!is_preprocess_projection_projection_target(info_lhs, lhs_args) &&
+            !is_preprocess_projection_projection_target(info_rhs, rhs_args))
+            return true; // do nothing, preprocessing step will not help
+        unsigned l_nparams = info_lhs->m_nparams;
+        unsigned r_nparams = info_rhs->m_nparams;
+        if (lhs_args.size() - l_nparams != rhs_args.size() - r_nparams)
+            return true; // the number of arguments to the projection data do not match.
+        expr new_lhs_app = mk_app(f_lhs, l_nparams+1, lhs_args.data());
+        expr new_rhs_app = mk_app(f_rhs, r_nparams+1, rhs_args.data());
+        constraint_seq cs;
+        auto t1 = infer(new_lhs_app, cs);
+        auto t2 = infer(new_rhs_app, cs);
+        if (!t1 || !t2)
+            return true; // failed to infer types
+        if (!process_constraints(cs))
+            return false;
+        return is_def_eq(*t1, *t2, c.get_justification());
+    }
+
+    bool is_same_projection_projection(expr const & lhs, expr const & rhs) {
+        expr const & f_lhs = get_app_fn(lhs);
+        expr const & f_rhs = get_app_fn(rhs);
+        return
+            is_constant(f_lhs) && is_constant(f_rhs) &&
+            const_name(f_lhs) == const_name(f_rhs) &&
+            is_projection(m_env, const_name(f_lhs));
+    }
+
+    bool is_same_projection_projection(constraint const & c) {
+        return is_same_projection_projection(cnstr_lhs_expr(c), cnstr_rhs_expr(c));
+    }
+
+    bool process_same_projection_projection(constraint const & c) {
+        lean_assert(is_same_projection_projection(c));
+        buffer<expr> lhs_args, rhs_args;
+        expr const & f_lhs = get_app_args(cnstr_lhs_expr(c), lhs_args);
+        expr const & f_rhs = get_app_args(cnstr_rhs_expr(c), rhs_args);
+        justification const & j = c.get_justification();
+        return process_levels(const_levels(f_lhs), const_levels(f_rhs), j) && process_args(lhs_args, rhs_args, j);
+    }
+
+    bool is_projection_projection(constraint const & c) {
+        return is_projection_app(cnstr_lhs_expr(c)) && is_projection_app(cnstr_rhs_expr(c));
+    }
+
+    bool process_projection_projection(constraint const & c, unsigned cidx) {
+        lean_assert(is_projection_projection(c));
+        // postpone constraint
+        if (cidx < get_group_first_index(cnstr_group::ClassInstance)) {
+            // pospone constraint
+            unsigned cidx = add_cnstr(c, cnstr_group::Epilogue);
+            add_meta_occs(cnstr_lhs_expr(c), cidx);
+            add_meta_occs(cnstr_rhs_expr(c), cidx);
+            return true;
+        } else {
+            return false;
+        }
+    }
+
     bool process_plugin_constraint(constraint const & c) {
         lean_assert(!is_choice_cnstr(c));
         lazy_list<constraints> alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child());
@@ -1324,6 +1499,34 @@ struct unifier_fn {
         }
     }
 
+    // Make sure the two lists of levels are definitionally equal.
+    bool process_levels(levels lhs_lvls, levels rhs_lvls, justification const & j) {
+        while (!is_nil(lhs_lvls)) {
+            if (is_nil(rhs_lvls))
+                return false;
+            level lhs = head(lhs_lvls);
+            level rhs = head(rhs_lvls);
+            if (!process_constraint(mk_level_eq_cnstr(lhs, rhs, j)))
+                return false;
+            lhs_lvls = tail(lhs_lvls);
+            rhs_lvls = tail(rhs_lvls);
+        }
+        return is_nil(rhs_lvls);
+    }
+
+    // Make sure the two buffers of arguments are definitionally equal
+    bool process_args(buffer<expr> const & lhs_args, buffer<expr> const & rhs_args, justification const & j) {
+        if (lhs_args.size() != rhs_args.size())
+            return false;
+        unsigned i = lhs_args.size();
+        while (i > 0) {
+            --i;
+            if (!is_def_eq(lhs_args[i], rhs_args[i], j))
+                return false;
+        }
+        return true;
+    }
+
     /**
         \brief Solve constraints of the form (f a_1 ... a_n) =?= (f b_1 ... b_n) where f can be expanded.
         We consider two possible solutions:
@@ -1361,22 +1564,7 @@ struct unifier_fn {
 
         // process first case
         justification new_j = mk_composite1(j, a);
-        while (!is_nil(lhs_lvls)) {
-            level lhs = head(lhs_lvls);
-            level rhs = head(rhs_lvls);
-            if (!process_constraint(mk_level_eq_cnstr(lhs, rhs, new_j)))
-                return false;
-            lhs_lvls = tail(lhs_lvls);
-            rhs_lvls = tail(rhs_lvls);
-        }
-
-        unsigned i = lhs_args.size();
-        while (i > 0) {
-            --i;
-            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j))
-                return false;
-        }
-        return true;
+        return process_levels(lhs_lvls, rhs_lvls, new_j) && process_args(lhs_args, rhs_args, new_j);
     }
 
     /** \brief Return true iff \c c is a flex-rigid constraint. */
@@ -1877,6 +2065,10 @@ struct unifier_fn {
             return false;
         if (m_config.m_computation)
             return true; // if unifier.computation is true, we always consider the additional whnf split
+        // TODO(Leo): perhaps we should use the following heuristic only for coercions
+        // automatically generated by structure manager
+        if (is_coercion(m_env, get_app_fn(rhs)))
+            return false;
         buffer<expr> locals;
         expr const * it = &lhs;
         while (is_app(*it)) {
@@ -2319,6 +2511,10 @@ struct unifier_fn {
                     return process_flex_rigid(c);
                 } else if (is_flex_flex(c)) {
                     return process_flex_flex(c);
+                } else if (is_same_projection_projection(c)) {
+                    return process_same_projection_projection(c);
+                } else if (is_projection_projection(c)) {
+                    return process_projection_projection(c, cidx);
                 } else {
                     return process_plugin_constraint(c);
                 }

src/library/util.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/unfold_macros.h"
 #include "library/pp_options.h"
+#include "library/projection.h"
 
 namespace lean {
 bool is_standard(environment const & env) {
@@ -798,17 +799,6 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con
         });
 }
 
-class extra_opaque_converter : public default_converter {
-    name_predicate m_pred;
-public:
-    extra_opaque_converter(environment const & env, name_predicate const & p):default_converter(env, true), m_pred(p) {}
-    virtual bool is_opaque(declaration const & d) const {
-        if (m_pred(d.get_name()))
-            return true;
-        return default_converter::is_opaque(d);
-    }
-};
-
 format format_goal(formatter const & fmt, buffer<expr> const & hyps, expr const & conclusion, substitution const & s) {
     substitution tmp_subst(s);
     options const & opts = fmt.get_options();
@@ -880,8 +870,25 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
         });
 }
 
+template<typename Converter>
+class extra_opaque_converter : public Converter {
+    name_predicate m_pred;
+public:
+    extra_opaque_converter(environment const & env, name_predicate const & p):Converter(env), m_pred(p) {}
+    virtual bool is_opaque(declaration const & d) const {
+        if (m_pred(d.get_name()))
+            return true;
+        return Converter::is_opaque(d);
+    }
+};
+
 type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) {
     return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-                                         std::unique_ptr<converter>(new extra_opaque_converter(env, pred))));
+                                         std::unique_ptr<converter>(new extra_opaque_converter<projection_converter>(env, pred))));
+}
+
+type_checker_ptr mk_simple_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) {
+    return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
+                                         std::unique_ptr<converter>(new extra_opaque_converter<default_converter>(env, pred))));
 }
 }

src/library/util.h

@@ -234,9 +234,12 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e
     return mk_type_mismatch_jst(v, v_type, t, v);
 }
 
-/** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true */
+/** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true.
+    Projections are reduced using the projection converter */
 type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred);
-
+/** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true.
+    No special support for projections is used */
+type_checker_ptr mk_simple_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred);
 /**
    \brief Generate the format object for <tt>hyps |- conclusion</tt>.
    The given substitution is applied to all elements.