lean2/src/library/class_instance_resolution.cpp

/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
*/
#include <vector>
#include "util/lbool.h"
#include "util/interrupt.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "kernel/metavar.h"
#include "kernel/abstract.h"
#include "kernel/for_each_fn.h"
#include "library/normalize.h"
#include "library/reducible.h"
#include "library/class.h"
#include "library/local_context.h"
#include "library/generic_exception.h"
#include "library/io_state_stream.h"
#include "library/replace_visitor.h"
#include "library/constants.h"
#include "library/pp_options.h"
#include "library/choice_iterator.h"
#include "library/type_inference.h"
#include "library/class_instance_resolution.h"
// The following include files are need by the old type class resolution procedure
#include "util/lazy_list_fn.h"
#include "library/unifier.h"
#include "library/metavar_closure.h"

#ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES
#define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false
#endif

#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH
#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32
#endif

#ifndef LEAN_DEFAULT_CLASS_TRANS_INSTANCES
#define LEAN_DEFAULT_CLASS_TRANS_INSTANCES true
#endif

namespace lean {
[[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
[[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); }

static name * g_class_trace_instances        = nullptr;
static name * g_class_instance_max_depth     = nullptr;
static name * g_class_trans_instances        = nullptr;
static name * g_class_force_new              = nullptr;
static name * g_prefix                       = nullptr;

LEAN_THREAD_PTR(ci_local_metavar_types, g_lm_types);
LEAN_THREAD_PTR(io_state,               g_ios);

bool get_class_trace_instances(options const & o) {
    return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES);
}

unsigned get_class_instance_max_depth(options const & o) {
    return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH);
}

bool get_class_trans_instances(options const & o) {
    return o.get_bool(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES);
}

bool get_class_force_new(options const & o) {
    return o.get_bool(*g_class_force_new, false);
}

class default_ci_local_metavar_types : public ci_local_metavar_types {
public:
    virtual expr infer_local(expr const & e) { return mlocal_type(e); }
    virtual expr infer_metavar(expr const & e) { return mlocal_type(e); }
};

static void finalize_lm_types(void * p) {
    delete reinterpret_cast<ci_local_metavar_types*>(p);
    g_lm_types = nullptr;
}

static ci_local_metavar_types & get_lm_types() {
    if (!g_lm_types) {
        g_lm_types = new default_ci_local_metavar_types();
        register_thread_finalizer(finalize_lm_types, g_lm_types);
    }
    return *g_lm_types;
}

static expr ci_infer_local(expr const & e) {
    return get_lm_types().infer_local(e);
}

static expr ci_infer_metavar(expr const & e) {
    return get_lm_types().infer_metavar(e);
}

/** \brief The following global thread local constant is a big hack for mk_subsingleton_instance.
    When g_subsingleton_hack is true, the following type-class resolution problem fails
    Given (A : Type{?u}), where ?u is a universe meta-variable created by an external module,

    ?Inst : subsingleton.{?u} A := subsingleton_prop ?M

    This case generates the unification problem

       subsingleton.{?u} A =?= subsingleton.{0} ?M

    which can be solved by assigning (?u := 0) and (?M := A)
    when the hack is enabled, the is_def_eq method in the type class module fails at the subproblem:
                ?u =?= 0

    That is, when the hack is on, type-class resolution cannot succeed by instantiating an external universe
    meta-variable with 0.
*/
LEAN_THREAD_VALUE(bool, g_subsingleton_hack, false);

struct cienv {
    typedef rb_map<unsigned, level, unsigned_cmp> uassignment;
    typedef rb_map<unsigned, expr,  unsigned_cmp> eassignment;
    typedef std::unique_ptr<type_inference>       ti_ptr;
    environment               m_env;
    pos_info_provider const * m_pip;
    ti_ptr                    m_ti_ptr;
    optional<pos_info>        m_pos;
    expr_struct_map<expr>     m_cache;
    name_predicate            m_not_reducible_pred;

    list<expr>                m_ctx;
    buffer<pair<name, expr>>  m_local_instances;

    unsigned                  m_next_local_idx;
    unsigned                  m_next_uvar_idx;
    unsigned                  m_next_mvar_idx;

    struct stack_entry {
        // We only use transitive instances when we can solve the problem in a single step.
        // That is, the transitive instance does not have any instance argument, OR
        // it uses local instances to fill them.
        // We accomplish that by not considering global instances when solving
        // transitive instance subproblems.
        expr     m_mvar;
        unsigned m_depth;
        bool     m_trans_inst_subproblem;
        stack_entry(expr const & m, unsigned d, bool s = false):
            m_mvar(m), m_depth(d), m_trans_inst_subproblem(s) {}
    };

    struct state {
        bool               m_trans_inst_subproblem;
        list<stack_entry>  m_stack; // stack of meta-variables that need to be synthesized;
        uassignment        m_uassignment;
        eassignment        m_eassignment;
        state():m_trans_inst_subproblem(false) {}
    };

    state                     m_state; // active state

    struct choice {
        list<expr>            m_local_instances;
        list<name>            m_trans_instances;
        list<name>            m_instances;
        state                 m_state;
    };

    std::vector<choice>       m_choices;
    expr                      m_main_mvar;

    bool                      m_multiple_instances;

    bool                      m_displayed_trace_header;

    // configuration
    options                   m_options; // it is used for pretty printing
    unsigned                  m_max_depth;
    bool                      m_trans_instances;
    bool                      m_trace_instances;

    class ti : public type_inference {
        cienv &            m_cienv;
        std::vector<state> m_stack;
    public:
        ti(cienv & e):type_inference(e.m_env), m_cienv(e) {}
        virtual bool is_extra_opaque(name const & n) const { return m_cienv.is_not_reducible(n); }
        virtual expr mk_tmp_local(expr const & type, binder_info const & bi) { return m_cienv.mk_local(type, bi); }
        virtual bool is_tmp_local(expr const & e) const { return m_cienv.is_internal_local(e); }
        virtual bool is_uvar(level const & l) const { return cienv::is_uvar(l); }
        virtual bool is_mvar(expr const & e) const { return m_cienv.is_mvar(e); }
        virtual level const * get_assignment(level const & u) const { return m_cienv.get_assignment(u); }
        virtual expr const * get_assignment(expr const & m) const { return m_cienv.get_assignment(m); }
        virtual void update_assignment(level const & u, level const & v) { return m_cienv.update_assignment(u, v); }
        virtual void update_assignment(expr const & m, expr const & v) { return m_cienv.update_assignment(m, v); }
        virtual expr infer_local(expr const & e) const { return ci_infer_local(e); }
        virtual expr infer_metavar(expr const & e) const { return ci_infer_metavar(e); }
        virtual void push() { m_stack.push_back(m_cienv.m_state); }
        virtual void pop() { m_cienv.m_state = m_stack.back(); m_stack.pop_back(); }
        virtual void commit() { m_stack.pop_back(); }

        virtual bool on_is_def_eq_failure(expr & e1, expr & e2) {
            if (is_app(e1) && is_app(e2)) {
                if (auto p1 = m_cienv.find_unsynth_metavar(e1)) {
                    if (m_cienv.mk_nested_instance(p1->first, p1->second)) {
                        e1 = m_cienv.instantiate_uvars_mvars(e1);
                        return true;
                    }
                }
                if (auto p2 = m_cienv.find_unsynth_metavar(e2)) {
                    if (m_cienv.mk_nested_instance(p2->first, p2->second)) {
                        e2 = m_cienv.instantiate_uvars_mvars(e2);
                        return true;
                    }
                }
            }
            return false;
        }

        virtual bool 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
                // have been instantiated. So, we just ignore and assume they will be solved by
                // the unifier.

                // See comment at g_subsingleton_hack declaration.
                if (g_subsingleton_hack && (is_zero(l1) || is_zero(l2)))
                    return false;
                return true; // we ignore
            } else {
                return false;
            }
        }


        virtual bool validate_assignment(expr const & m, buffer<expr> const & locals, expr const & v) {
            // We must check
            //   1. Any (internal) local constant occurring in v occurs in locals
            //   2. m does not occur in v
            bool ok = true;
            for_each(v, [&](expr const & e, unsigned) {
                    if (!ok)
                        return false; // stop search
                    if (is_tmp_local(e)) {
                        if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) {
                                    return mlocal_name(a) != mlocal_name(e); })) {
                            ok = false; // failed 1
                            return false;
                        }
                    } else if (is_mvar(e)) {
                        if (m == e) {
                            ok = false; // failed 2
                            return false;
                        }
                        return false;
                    }
                    return true;
                });
            return ok;
        }
    };

    cienv(bool multiple_instances = false):
        m_next_local_idx(0),
        m_next_uvar_idx(0),
        m_next_mvar_idx(0),
        m_multiple_instances(multiple_instances),
        m_max_depth(LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH),
        m_trans_instances(LEAN_DEFAULT_CLASS_TRANS_INSTANCES),
        m_trace_instances(LEAN_DEFAULT_CLASS_TRACE_INSTANCES) {}

    bool is_not_reducible(name const & n) const {
        return m_not_reducible_pred(n);
    }

    void clear_cache() {
        expr_struct_map<expr> fresh;
        fresh.swap(m_cache);
        if (m_ti_ptr)
            m_ti_ptr->clear_cache();
    }

    void clear_cache_and_ctx() {
        m_next_local_idx = 0;
        m_next_uvar_idx  = 0;
        m_next_mvar_idx  = 0;
        m_ctx = list<expr>();
        m_local_instances.clear();
        clear_cache();
    }

    optional<expr> check_cache(expr const & type) const {
        if (m_multiple_instances) {
            // We do not cache results when multiple instances have to be generated.
            return none_expr();
        }
        auto it = m_cache.find(type);
        if (it != m_cache.end())
            return some_expr(it->second);
        else
            return none_expr();
    }

    void cache_result(expr const & type, expr const & inst) {
        if (m_multiple_instances) {
            // We do not cache results when multiple instances have to be generated.
            return;
        }
        m_cache.insert(mk_pair(type, inst));
    }

    void set_options(options const & o) {
        m_options = o;
        unsigned max_depth    = get_class_instance_max_depth(o);
        bool trans_instances  = get_class_trans_instances(o);
        bool trace_instances  = get_class_trace_instances(o);
        if (trace_instances) {
            m_options = m_options.update_if_undef(get_pp_purify_metavars_name(), false);
            m_options = m_options.update_if_undef(get_pp_implicit_name(), true);
        }
        if (m_max_depth        != max_depth        ||
            m_trans_instances  != trans_instances  ||
            m_trace_instances  != trace_instances) {
            clear_cache_and_ctx();
        }
        m_max_depth        = max_depth;
        m_trans_instances  = trans_instances;
        m_trace_instances  = trace_instances;
    }

    void set_env(environment const & env) {
        // Remark: We can implement the following potential refinement.
        // If env is a descendant of m_env, and env does not add new global instances,
        // then we don't need to reset the cache
        if (!m_env.is_descendant(m_env) || !m_env.is_descendant(env)) {
            m_env                = env;
            m_not_reducible_pred = mk_not_reducible_pred(m_env);
            m_ti_ptr             = nullptr;
            clear_cache_and_ctx();
        }

        if (!m_ti_ptr) {
            m_ti_ptr.reset(new ti(*this));
            clear_cache_and_ctx();
        }
    }

    expr whnf(expr const & e) {
        lean_assert(m_ti_ptr);
        return m_ti_ptr->whnf(e);
    }

    expr infer_type(expr const & e) {
        lean_assert(m_ti_ptr);
        return m_ti_ptr->infer(e);
    }

    bool is_def_eq(expr const & e1, expr const & e2) {
        lean_assert(m_ti_ptr);
        return m_ti_ptr->is_def_eq(e1, e2);
    }

    expr instantiate_uvars_mvars(expr const & e) {
        lean_assert(m_ti_ptr);
        return m_ti_ptr->instantiate_uvars_mvars(e);
    }

    expr mk_local(expr const & type, binder_info const & bi = binder_info()) {
        unsigned idx = m_next_local_idx;
        m_next_local_idx++;
        name n(*g_prefix, idx);
        return lean::mk_local(n, n, type, bi);
    }

    bool is_internal_local(expr const & e) {
        if (!is_local(e))
            return false;
        name const & n = mlocal_name(e);
        return !n.is_atomic() && n.get_prefix() == *g_prefix;
    }

    // Helper function for find_unsynth_metavar
    static bool has_meta_arg(expr e) {
        while (is_app(e)) {
            if (is_meta(app_arg(e)))
                return true;
            e = app_fn(e);
        }
        return false;
    }

    /** IF \c e is of the form (f ... (?m t_1 ... t_n) ...) where ?m is an unassigned
        metavariable whose type is a type class, and (?m t_1 ... t_n) must be synthesized
        by type class resolution, then we return ?m.
        Otherwise, we return none */
    optional<pair<expr, expr>> find_unsynth_metavar(expr const & e) {
        if (!has_meta_arg(e))
            return optional<pair<expr, expr>>();
        buffer<expr> args;
        expr const & fn = get_app_args(e, args);
        expr type       = infer_type(fn);
        unsigned i      = 0;
        while (i < args.size()) {
            type = whnf(type);
            if (!is_pi(type))
                return optional<pair<expr, expr>>();
            expr const & arg = args[i];
           if (binding_info(type).is_inst_implicit() && is_meta(arg)) {
                expr const & m = get_app_fn(arg);
                if (is_mvar(m)) {
                    expr m_type = instantiate_uvars_mvars(infer_type(m));
                    if (!has_expr_metavar_relaxed(m_type)) {
                        return some(mk_pair(m, m_type));
                    }
                }
            }
            type = instantiate(binding_body(type), arg);
            i++;
        }
        return optional<pair<expr, expr>>();
    }

    /** \brief If the constant \c e is a class, return its name */
    optional<name> constant_is_class(expr const & e) {
        name const & cls_name = const_name(e);
        if (lean::is_class(m_env, cls_name)) {
            return optional<name>(cls_name);
        } else {
            return optional<name>();
        }
    }

    optional<name> is_full_class(expr type) {
        type = whnf(type);
        if (is_pi(type)) {
            return is_full_class(instantiate(binding_body(type), mk_local(binding_domain(type))));
        } else {
            expr f = get_app_fn(type);
            if (!is_constant(f))
                return optional<name>();
            return constant_is_class(f);
       }
    }

    /** \brief Partial/Quick test for is_class. Result
        l_true:   \c type is a class, and the name of the class is stored in \c result.
        l_false:  \c type is not a class.
        l_undef:  procedure did not establish whether \c type is a class or not.
    */
    lbool is_quick_class(expr const & type, name & result) {
        expr const * it         = &type;
        while (true) {
            switch (it->kind()) {
            case expr_kind::Var:  case expr_kind::Sort:   case expr_kind::Local:
            case expr_kind::Meta: case expr_kind::Lambda:
                return l_false;
            case expr_kind::Macro:
                return l_undef;
            case expr_kind::Constant:
                if (auto r = constant_is_class(*it)) {
                    result = *r;
                    return l_true;
                } else if (is_not_reducible(const_name(*it))) {
                    return l_false;
                } else {
                    return l_undef;
                }
            case expr_kind::App: {
                expr const & f = get_app_fn(*it);
                if (is_constant(f)) {
                    if (auto r = constant_is_class(f)) {
                        result = *r;
                        return l_true;
                    } else if (is_not_reducible(const_name(f))) {
                        return l_false;
                    } else {
                        return l_undef;
                    }
                } else if (is_lambda(f) || is_macro(f)) {
                    return l_undef;
                } else {
                    return l_false;
                }
            }
            case expr_kind::Pi:
                it = &binding_body(*it);
                break;
            }
        }
    }

    /** \brief Return true iff \c type is a class or Pi that produces a class. */
    optional<name> is_class(expr const & type) {
        name result;
        switch (is_quick_class(type, result)) {
        case l_true:  return optional<name>(result);
        case l_false: return optional<name>();
        case l_undef: break;
        }
        return is_full_class(type);
    }


    // Auxiliary method for set_ctx
    void set_local_instance(unsigned i, name const & cname, expr const & e) {
        lean_assert(i <= m_local_instances.size());
        if (i == m_local_instances.size()) {
            clear_cache();
            m_local_instances.push_back(mk_pair(cname, e));
        } else if (e != m_local_instances[i].second) {
            clear_cache();
            m_local_instances[i] = mk_pair(cname, e);
        } else {
            // we don't need to reset the cache since this local instance
            // is equal to the one used in a previous call
        }
    }

    void set_ctx(list<expr> const & ctx) {
        if (is_eqp(m_ctx, ctx)) {
            // we can keep the cache because the local context
            // is still pointing to the same object.
            return;
        }
        m_ctx = ctx;
        unsigned i = 0;
        for (expr const & e : ctx) {
            // Remark: we use infer_type(e) instead of mlocal_type because we want to allow
            // customers (e.g., blast) of this class to store the type of local constants
            // in a different place.
            if (auto cname = is_class(infer_type(e))) {
                set_local_instance(i, *cname, e);
                i++;
            }
        }
        if (i < m_local_instances.size()) {
            // new ctx has fewer local instances than previous one
            m_local_instances.resize(i);
            clear_cache();
        }
    }

    void set_pos_info(pos_info_provider const * pip, expr const & pos_ref) {
        m_pip = pip;
        if (m_pip)
            m_pos = m_pip->get_pos_info(pos_ref);
    }

    // Create an internal universal metavariable
    level mk_uvar() {
        unsigned idx = m_next_uvar_idx;
        m_next_uvar_idx++;
        return mk_meta_univ(name(*g_prefix, idx));
    }

    // Return true iff \c l is an internal universe metavariable created by this module.
    static bool is_uvar(level const & l) {
        if (!is_meta(l))
            return false;
        name const & n = meta_id(l);
        return !n.is_atomic() && n.get_prefix() == *g_prefix;
    }

    static unsigned uvar_idx(level const & l) {
        lean_assert(is_uvar(l));
        return meta_id(l).get_numeral();
    }

    level const * get_assignment(level const & u) const {
        return m_state.m_uassignment.find(uvar_idx(u));
    }

    bool is_assigned(level const & u) const {
        return get_assignment(u) != nullptr;
    }

    // Assign \c v to the universe metavariable \c u.
    void update_assignment(level const & u, level const & v) {
        m_state.m_uassignment.insert(uvar_idx(u), v);
    }

    // Create an internal metavariable.
    expr mk_mvar(expr const & type) {
        unsigned idx = m_next_mvar_idx;
        m_next_mvar_idx++;
        return mk_metavar(name(*g_prefix, idx), type);
    }

    // Return true iff \c e is an internal metavariable created by this module.
    static bool is_mvar(expr const & e) {
        if (!is_metavar(e))
            return false;
        name const & n = mlocal_name(e);
        return !n.is_atomic() && n.get_prefix() == *g_prefix;
    }

    static unsigned mvar_idx(expr const & m) {
        lean_assert(is_mvar(m));
        return mlocal_name(m).get_numeral();
    }

    expr const * get_assignment(expr const & m) const {
        return m_state.m_eassignment.find(mvar_idx(m));
    }

    bool is_assigned(expr const & m) const {
        return get_assignment(m) != nullptr;
    }

    void update_assignment(expr const & m, expr const & v) {
        m_state.m_eassignment.insert(mvar_idx(m), v);
        lean_assert(is_assigned(m));
    }

    // Assign \c v to the metavariable \c m.
    void assign(expr const & m, expr const & v) {
        lean_assert(!is_assigned(m));
        update_assignment(m, v);
    }

    io_state_stream diagnostic() {
        io_state ios(*g_ios);
        ios.set_options(m_options);
        return lean::diagnostic(m_env, ios);
    }

    void trace(unsigned depth, expr const & mvar, expr const & mvar_type, expr const & r) {
        lean_assert(m_trace_instances);
        auto out = diagnostic();
        if (!m_displayed_trace_header && m_choices.size() == 1) {
            if (m_pip) {
                if (auto fname = m_pip->get_file_name()) {
                    out << fname << ":";
                }
                if (m_pos)
                    out << m_pos->first << ":" << m_pos->second << ":";
            }
            out << " class-instance resolution trace" << endl;
            m_displayed_trace_header = true;
        }
        for (unsigned i = 0; i < depth; i++)
            out << " ";
        if (depth > 0)
            out << "[" << depth << "] ";
        out << mvar << " : " << instantiate_uvars_mvars(mvar_type) << " := " << r << endl;
    }

    // Try to synthesize e.m_mvar using instance inst : inst_type.
    // trans_inst is true if inst is a transitive instance.
    bool try_instance(stack_entry const & e, expr const & inst, expr const & inst_type, bool trans_inst) {
        try {
            buffer<expr> locals;
            expr const & mvar = e.m_mvar;
            expr mvar_type = mlocal_type(mvar);
            while (true) {
                mvar_type = whnf(mvar_type);
                if (!is_pi(mvar_type))
                    break;
                expr local  = mk_local(binding_domain(mvar_type));
                locals.push_back(local);
                mvar_type = instantiate(binding_body(mvar_type), local);
            }
            expr type  = inst_type;
            expr r     = inst;
            buffer<expr> new_inst_mvars;
            while (true) {
                type = whnf(type);
                if (!is_pi(type))
                    break;
                expr new_mvar = mk_mvar(Pi(locals, binding_domain(type)));
                if (binding_info(type).is_inst_implicit()) {
                    new_inst_mvars.push_back(new_mvar);
                }
                expr new_arg = mk_app(new_mvar, locals);
                r    = mk_app(r, new_arg);
                type = instantiate(binding_body(type), new_arg);
            }
            if (m_trace_instances) {
                trace(e.m_depth, mk_app(mvar, locals), mvar_type, r);
            }
            if (!is_def_eq(mvar_type, type)) {
                return false;
            }
            r = Fun(locals, r);
            if (is_assigned(mvar)) {
                // Remark: if the metavariable is already assigned, we should check whether
                // the previous assignment (obtained by solving unification constraints) and the
                // synthesized one are definitionally equal. We don't do that for performance reasons.
                // Moreover, the is_def_eq defined here is not complete (e.g., it only unfolds reducible constants).
                update_assignment(mvar, r);
            } else {
                assign(mvar, r);
            }
            // copy new_inst_mvars to stack
            unsigned i = new_inst_mvars.size();
            while (i > 0) {
                --i;
                m_state.m_stack = cons(stack_entry(new_inst_mvars[i], e.m_depth+1, trans_inst), m_state.m_stack);
            }
            return true;
        } catch (exception &) {
            return false;
        }
    }

    bool try_instance(stack_entry const & e, name const & inst_name, bool trans_inst) {
        if (auto decl = m_env.find(inst_name)) {
            buffer<level> ls_buffer;
            unsigned num_univ_ps = decl->get_num_univ_params();
            for (unsigned i = 0; i < num_univ_ps; i++)
                ls_buffer.push_back(mk_uvar());
            levels ls = to_list(ls_buffer.begin(), ls_buffer.end());
            expr inst_cnst = mk_constant(inst_name, ls);
            expr inst_type = instantiate_type_univ_params(*decl, ls);
            return try_instance(e, inst_cnst, inst_type, trans_inst);
        } else {
            return false;
        }
    }

    list<expr> get_local_instances(name const & cname) {
        buffer<expr> selected;
        for (pair<name, expr> const & p : m_local_instances) {
            if (p.first == cname)
                selected.push_back(p.second);
        }
        return to_list(selected);
    }

    bool is_done() const {
        return empty(m_state.m_stack);
    }

    bool mk_choice_point(expr const & mvar) {
        lean_assert(is_mvar(mvar));
        if (m_choices.size() > m_max_depth) {
            throw_class_exception("maximum class-instance resolution depth has been reached "
                                  "(the limit can be increased by setting option 'class.instance_max_depth') "
                                  "(the class-instance resolution trace can be visualized by setting option 'class.trace_instances')",
                                  mlocal_type(m_main_mvar));
        }
        // Remark: we initially tried to reject branches where mvar_type contained unassigned metavariables.
        // The idea was to make the procedure easier to understand.
        // However, it turns out this is too restrictive. The group_theory folder contains the following instance.
        //     nsubg_setoid : Π {A : Type} [s : group A] (N : set A) [is_nsubg : @is_normal_subgroup A s N], setoid A
        // When it is used, it creates a subproblem for
        //    is_nsubg : @is_normal_subgroup A s ?N
        // where ?N is not known. Actually, we can only find the value for ?N by constructing the instance is_nsubg.
        expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar));
        bool toplevel_choice = m_choices.empty();
        m_choices.push_back(choice());
        choice & r = m_choices.back();
        auto cname = is_class(mvar_type);
        if (!cname)
            return false;
        r.m_local_instances = get_local_instances(*cname);
        if (m_trans_instances && toplevel_choice) {
            // we only use transitive instances in the top-level
            r.m_trans_instances = get_class_derived_trans_instances(m_env, *cname);
        }
        r.m_instances = get_class_instances(m_env, *cname);
        if (empty(r.m_local_instances) && empty(r.m_trans_instances) && empty(r.m_instances))
            return false;
        r.m_state = m_state;
        return true;
    }

    bool process_next_alt_core(stack_entry const & e, list<expr> & insts) {
        while (!empty(insts)) {
            expr inst       = head(insts);
            insts           = tail(insts);
            expr inst_type  = infer_type(inst);
            bool trans_inst = false;
            if (try_instance(e, inst, inst_type, trans_inst))
                return true;
        }
        return false;
    }

    bool process_next_alt_core(stack_entry const & e, list<name> & inst_names, bool trans_inst) {
        while (!empty(inst_names)) {
            name inst_name    = head(inst_names);
            inst_names        = tail(inst_names);
            if (try_instance(e, inst_name, trans_inst))
                return true;
        }
        return false;
    }

    bool process_next_alt(stack_entry const & e) {
        lean_assert(!m_choices.empty());
        choice & c = m_choices.back();
        if (process_next_alt_core(e, c.m_local_instances))
            return true;
        if (!e.m_trans_inst_subproblem) {
            if (process_next_alt_core(e, c.m_trans_instances, true))
                return true;
            if (process_next_alt_core(e, c.m_instances, false))
                return true;
        }
        return false;
    }

    bool process_next_mvar() {
        lean_assert(!is_done());
        stack_entry e = head(m_state.m_stack);
        if (!mk_choice_point(e.m_mvar))
            return false;
        m_state.m_stack = tail(m_state.m_stack);
        return process_next_alt(e);
    }

    bool backtrack() {
        if (m_choices.empty())
            return false;
        while (true) {
            m_choices.pop_back();
            if (m_choices.empty())
                return false;
            m_state         = m_choices.back().m_state;
            stack_entry e   = head(m_state.m_stack);
            m_state.m_stack = tail(m_state.m_stack);
            if (process_next_alt(e))
                return true;
        }
    }

    optional<expr> search() {
        while (!is_done()) {
            if (!process_next_mvar()) {
                if (!backtrack())
                    return none_expr();
            }
        }
        return some_expr(instantiate_uvars_mvars(m_main_mvar));
    }

    optional<expr> next_solution() {
        if (m_choices.empty())
            return none_expr();
        m_state         = m_choices.back().m_state;
        stack_entry e   = head(m_state.m_stack);
        m_state.m_stack = tail(m_state.m_stack);
        if (process_next_alt(e))
            return search();
        else if (backtrack())
            return search();
        else
            return none_expr();
    }

    void init_search(expr const & type) {
        m_state         = state();
        m_main_mvar     = mk_mvar(type);
        m_state.m_stack = cons(stack_entry(m_main_mvar, 0), m_state.m_stack);
        m_choices.clear();
    }

    optional<expr> ensure_no_meta(optional<expr> r) {
        while (true) {
            if (!r)
                return none_expr();
            if (!has_expr_metavar_relaxed(*r)) {
                cache_result(mlocal_type(m_main_mvar), *r);
                return r;
            }
            r = next_solution();
        }
    }

    optional<expr> mk_instance_core(expr const & type) {
        if (auto r = check_cache(type)) {
            if (m_trace_instances) {
                auto out = diagnostic();
                out << "cached instance for " << type << "\n" << *r << "\n";
            }
            return r;
        }

        init_search(type);
        auto r = search();
        return ensure_no_meta(r);
    }

    optional<expr> operator()(environment const & env, options const & o, pos_info_provider const * pip, list<expr> const & ctx, expr const & type,
                              expr const & pos_ref) {
        set_env(env);
        set_options(o);
        set_ctx(ctx);
        set_pos_info(pip, pos_ref);
        m_displayed_trace_header = false;

        return mk_instance_core(type);
    }

    optional<expr> next() {
        if (!m_multiple_instances)
            return none_expr();
        auto r = next_solution();
        return ensure_no_meta(r);
    }

    /** \brief Create a nested type class instance of the given type
        \remark This method is used to resolve nested type class resolution problems. */
    optional<expr> mk_nested_instance(expr const & type) {
        std::vector<choice> choices;
        m_choices.swap(choices); // save choice stack
        flet<state> save_state(m_state, state());
        flet<expr>  save_main_mvar(m_main_mvar, expr());
        auto r = mk_instance_core(type);
        m_choices.swap(choices); // restore choice stack
        return r;
    }

    /** \brief Create a nested type class instance of the given type, and assign it to metavariable \c m.
        Return true iff the instance was successfully created.
        \remark This method is used to resolve nested type class resolution problems. */
    bool mk_nested_instance(expr const & m, expr const & m_type) {
        lean_assert(is_mvar(m));
        if (auto r = mk_nested_instance(m_type)) {
            update_assignment(m, *r);
            return true;
        } else {
            return false;
        }
    }
};

MK_THREAD_LOCAL_GET_DEF(cienv, get_cienv);

static void clear_cache_and_ctx() {
    get_cienv().clear_cache_and_ctx();
}

ci_local_metavar_types_scope::ci_local_metavar_types_scope(ci_local_metavar_types & t):
    m_old(g_lm_types) {
    g_lm_types = &t;
    clear_cache_and_ctx();
}

ci_local_metavar_types_scope::~ci_local_metavar_types_scope() {
    clear_cache_and_ctx();
    g_lm_types = m_old;
}

static optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & e, pos_info_provider const * pip,
                                        expr const & pos_ref) {
    flet<io_state*> set_ios(g_ios, const_cast<io_state*>(&ios));
    return get_cienv()(env, ios.get_options(), pip, ctx, e, pos_ref);
}

optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & e, pos_info_provider const * pip) {
    return mk_class_instance(env, ios, ctx, e, pip, e);
}

optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e, pos_info_provider const * pip) {
    return mk_class_instance(env, get_dummy_ios(), ctx, e, pip);
}

// Auxiliary class for generating a lazy-stream of instances.
class class_multi_instance_iterator : public choice_iterator {
    io_state       m_ios;
    cienv          m_cienv;
    expr           m_new_meta;
    justification  m_new_j;
    optional<expr> m_first;
public:
    class_multi_instance_iterator(environment const & env, io_state const & ios, list<expr> const & ctx,
                                  expr const & e, pos_info_provider const * pip, expr const & pos_ref,
                                  expr const & new_meta, justification const & new_j,
                                  bool is_strict):
        choice_iterator(!is_strict),
        m_ios(ios),
        m_cienv(true),
        m_new_meta(new_meta),
        m_new_j(new_j) {
        flet<io_state*> set_ios(g_ios, const_cast<io_state*>(&m_ios));
        m_first = m_cienv(env, ios.get_options(), pip, ctx, e, pos_ref);
    }

    virtual ~class_multi_instance_iterator() {}

    virtual optional<constraints> next() {
        optional<expr> r;
        if (m_first) {
            r       = m_first;
            m_first = none_expr();
        } else {
            flet<io_state*> set_ios(g_ios, const_cast<io_state*>(&m_ios));
            r = m_cienv.next();
        }
        if (r) {
            constraint c = mk_eq_cnstr(m_new_meta, *r, m_new_j);
            return optional<constraints>(constraints(c));
        } else {
            return optional<constraints>();
        }
    }
};

static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, local_context const & _ctx, expr const & m, bool is_strict,
                                               bool use_local_instances, pos_info_provider const * pip) {
    justification j         = mk_failed_to_synthesize_jst(env, m);
    auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator &&) {
        cienv & cenv = get_cienv();
        cenv.set_env(env);
        auto cls_name = cenv.is_class(meta_type);
        if (!cls_name) {
            // do nothing, since type is not a class.
            return lazy_list<constraints>(constraints());
        }
        bool multiple_insts = try_multiple_instances(env, *cls_name);
        local_context ctx;
        if (use_local_instances)
            ctx = _ctx.instantiate(substitution(s));
        pair<expr, justification> mj = update_meta(meta, s);
        expr new_meta                = mj.first;
        justification new_j          = mj.second;
        if (multiple_insts) {
            return choose(std::shared_ptr<choice_iterator>(new class_multi_instance_iterator(env, ios, ctx.get_data(),
                                                                                             meta_type, pip, meta,
                                                                                             new_meta, new_j, is_strict)));
        } else {
            if (auto r = mk_class_instance(env, ios, ctx.get_data(), meta_type, pip, meta)) {
                constraint c = mk_eq_cnstr(new_meta, *r, new_j);
                return lazy_list<constraints>(constraints(c));
            } else if (is_strict) {
                return lazy_list<constraints>();
            } else {
                return lazy_list<constraints>(constraints());
            }
        }
    };
    bool owner = false;
    delay_factor factor;
    return mk_choice_cnstr(m, choice_fn, factor, owner, j);
}

/** \brief Create a metavariable, and attach choice constraint for generating
    solutions using class-instances
*/
pair<expr, constraint> mk_new_class_instance_elaborator(
    environment const & env, io_state const & ios, local_context const & ctx,
    name const & prefix, optional<name> const & suffix, bool use_local_instances,
    bool is_strict, optional<expr> const & type, tag g, pos_info_provider const * pip) {
    name_generator ngen(prefix);
    expr m       = ctx.mk_meta(ngen, suffix, type, g);
    constraint c = mk_class_instance_root_cnstr(env, ios, ctx, m, is_strict,
                                                use_local_instances, pip);
    return mk_pair(m, c);
}

optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances) {
    if (use_local_instances)
        return mk_class_instance(env, ios, ctx.get_data(), type, nullptr);
    else
        return mk_class_instance(env, ios, list<expr>(), type, nullptr);
}

optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type) {
    return mk_class_instance(env, ctx.get_data(), type, nullptr);
}

optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
    level lvl        = sort_level(tc.ensure_type(type).first);
    expr is_hset     = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first;
    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) {
    flet<bool> set(g_subsingleton_hack, 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 mk_class_instance(tc.env(), ios, ctx, subsingleton);
}

void initialize_class_instance_resolution() {
    g_prefix                       = new name(name::mk_internal_unique_name());
    g_class_trace_instances        = new name{"class", "trace_instances"};
    g_class_instance_max_depth     = new name{"class", "instance_max_depth"};
    g_class_trans_instances        = new name{"class", "trans_instances"};
    g_class_force_new              = new name{"class", "force_new"};

    register_bool_option(*g_class_trace_instances,  LEAN_DEFAULT_CLASS_TRACE_INSTANCES,
                         "(class) display messages showing the class-instances resolution execution trace");

    register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH,
                             "(class) max allowed depth in class-instance resolution");

    register_bool_option(*g_class_trans_instances,  LEAN_DEFAULT_CLASS_TRANS_INSTANCES,
                         "(class) use automatically derived instances from the transitive closure of "
                         "the structure instance graph");

    register_bool_option(*g_class_force_new,  false,
                         "(class) force new type class resolution procedure to be used even in HoTT mode (THIS IS TEMPORARY OPTION)");
}

void finalize_class_instance_resolution() {
    delete g_prefix;
    delete g_class_trace_instances;
    delete g_class_instance_max_depth;
    delete g_class_trans_instances;
    delete g_class_force_new;
}

/*
  The rest of this module implements the old more powerful and *expensive* type class
  resolution procedure. We still have it because the HoTT library contains
  type class instances that require full-higher order unification to be solved.

  Example:

  definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A}
    (p : x = y) : (is_equiv (transport P p)) := ...
*/

/** \brief Context for handling class-instance metavariable choice constraint */
struct class_instance_context {
    io_state                  m_ios;
    name_generator            m_ngen;
    type_checker_ptr          m_tc;
    expr                      m_main_meta;
    bool                      m_use_local_instances;
    bool                      m_trace_instances;
    bool                      m_conservative;
    unsigned                  m_max_depth;
    bool                      m_trans_instances;
    char const *              m_fname;
    optional<pos_info>        m_pos;
    class_instance_context(environment const & env, io_state const & ios,
                           name const & prefix, bool use_local_instances):
        m_ios(ios),
        m_ngen(prefix),
        m_use_local_instances(use_local_instances) {
        m_fname           = nullptr;
        m_trace_instances = get_class_trace_instances(ios.get_options());
        m_max_depth       = get_class_instance_max_depth(ios.get_options());
        m_conservative    = true; // We removed the option class.conservative
        m_trans_instances = get_class_trans_instances(ios.get_options());
        m_tc              = mk_class_type_checker(env, m_ngen.mk_child(), m_conservative);
        options opts      = m_ios.get_options();
        opts              = opts.update_if_undef(get_pp_purify_metavars_name(), false);
        opts              = opts.update_if_undef(get_pp_implicit_name(), true);
        m_ios.set_options(opts);
    }

    environment const & env() const { return m_tc->env(); }
    io_state const & ios() const { return m_ios; }
    bool use_local_instances() const { return m_use_local_instances; }
    type_checker & tc() const { return *m_tc; }
    bool trace_instances() const { return m_trace_instances; }
    void set_main_meta(expr const & meta) { m_main_meta = meta; }
    expr const & get_main_meta() const { return m_main_meta; }
    void set_pos(char const * fname, optional<pos_info> const & pos) {
        m_fname = fname;
        m_pos   = pos;
    }
    optional<pos_info> const & get_pos() const { return m_pos; }
    char const * get_file_name() const { return m_fname; }
    unsigned get_max_depth() const { return m_max_depth; }
    bool use_trans_instances() const { return m_trans_instances; }
};

static pair<expr, constraint>
mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
                             optional<expr> const & type, tag g, unsigned depth, bool use_globals);

/** \brief Choice function \c fn for synthesizing class instances.
    The function \c fn produces a stream of alternative solutions for ?m.
    In this case, \c fn will do the following:
    1) if the elaborated type of ?m is a 'class' C, then the stream will start with
         a) all local instances of class C (if elaborator.local_instances == true)
         b) all global instances of class C
*/
struct class_instance_elaborator : public choice_iterator {
    std::shared_ptr<class_instance_context> m_C;
    local_context           m_ctx;
    expr                    m_meta;
    // elaborated type of the metavariable
    expr                    m_meta_type;
    // local instances that should also be included in the
    // class-instance resolution.
    // This information is retrieved from the local context
    list<expr>              m_local_instances;
    // global declaration names that are class instances.
    // This information is retrieved using #get_class_instances.
    list<name>              m_trans_instances;
    list<name>              m_instances;
    justification           m_jst;
    unsigned                m_depth;
    bool                    m_displayed_trace_header;

    class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
                              expr const & meta, expr const & meta_type,
                              list<expr> const & local_insts, list<name> const & trans_insts, list<name> const & instances,
                              justification const & j, unsigned depth):
        choice_iterator(), m_C(C), m_ctx(ctx), m_meta(meta), m_meta_type(meta_type),
        m_local_instances(local_insts), m_trans_instances(trans_insts), m_instances(instances), m_jst(j), m_depth(depth) {
        if (m_depth > m_C->get_max_depth()) {
            throw_class_exception("maximum class-instance resolution depth has been reached "
                                  "(the limit can be increased by setting option 'class.instance_max_depth') "
                                  "(the class-instance resolution trace can be visualized "
                                  "by setting option 'class.trace_instances')",
                                  C->get_main_meta());
        }
        m_displayed_trace_header = false;
    }

    constraints mk_constraints(constraint const & c, buffer<constraint> const & cs) {
        return cons(c, to_list(cs.begin(), cs.end()));
    }

    void trace(expr const & t, expr const & r) {
        if (!m_C->trace_instances())
            return;
        auto out = diagnostic(m_C->env(), m_C->ios());
        if (!m_displayed_trace_header && m_depth == 0) {
            if (auto fname = m_C->get_file_name()) {
                out << fname << ":";
            }
            if (auto pos = m_C->get_pos()) {
                out << pos->first << ":" << pos->second << ":";
            }
            out << " class-instance resolution trace" << endl;
            m_displayed_trace_header = true;
        }
        for (unsigned i = 0; i < m_depth; i++)
            out << " ";
        if (m_depth > 0)
            out << "[" << m_depth << "] ";
        out << m_meta << " : " << t << " := " << r << endl;
    }

    optional<constraints> try_instance(expr const & inst, expr const & inst_type, bool use_globals) {
        type_checker & tc     = m_C->tc();
        name_generator & ngen = m_C->m_ngen;
        tag g                 = inst.get_tag();
        try {
            flet<local_context> scope(m_ctx, m_ctx);
            buffer<expr> locals;
            expr meta_type = m_meta_type;
            while (true) {
                meta_type = tc.whnf(meta_type).first;
                if (!is_pi(meta_type))
                    break;
                expr local  = mk_local(ngen.next(), binding_name(meta_type),
                                       binding_domain(meta_type), binding_info(meta_type));
                m_ctx.add_local(local);
                locals.push_back(local);
                meta_type = instantiate(binding_body(meta_type), local);
            }
            expr type  = inst_type;
            expr r     = inst;
            buffer<constraint> cs;
            while (true) {
                type = tc.whnf(type).first;
                if (!is_pi(type))
                    break;
                expr arg;
                if (binding_info(type).is_inst_implicit()) {
                    pair<expr, constraint> ac = mk_class_instance_elaborator(m_C, m_ctx, some_expr(binding_domain(type)),
                                                                             g, m_depth+1, use_globals);
                    arg = ac.first;
                    cs.push_back(ac.second);
                } else {
                    arg = m_ctx.mk_meta(m_C->m_ngen, some_expr(binding_domain(type)), g);
                }
                r    = mk_app(r, arg, g);
                type = instantiate(binding_body(type), arg);
            }
            r = Fun(locals, r);
            trace(meta_type, r);
            constraint c = mk_eq_cnstr(m_meta, r, m_jst);
            return optional<constraints>(mk_constraints(c, cs));
        } catch (exception &) {
            return optional<constraints>();
        }
    }

    optional<constraints> try_instance(name const & inst, bool use_globals) {
        environment const & env = m_C->env();
        if (auto decl = env.find(inst)) {
            name_generator & ngen = m_C->m_ngen;
            buffer<level> ls_buffer;
            unsigned num_univ_ps = decl->get_num_univ_params();
            for (unsigned i = 0; i < num_univ_ps; i++)
                ls_buffer.push_back(mk_meta_univ(ngen.next()));
            levels ls = to_list(ls_buffer.begin(), ls_buffer.end());
            expr inst_cnst = copy_tag(m_meta, mk_constant(inst, ls));
            expr inst_type = instantiate_type_univ_params(*decl, ls);
            return try_instance(inst_cnst, inst_type, use_globals);
        } else {
            return optional<constraints>();
        }
    }

    virtual optional<constraints> next() {
        while (!empty(m_local_instances)) {
            expr inst         = head(m_local_instances);
            m_local_instances = tail(m_local_instances);
            if (!is_local(inst))
                continue;
            bool use_globals = true;
            if (auto r = try_instance(inst, mlocal_type(inst), use_globals))
                return r;
        }
        while (!empty(m_trans_instances)) {
            bool use_globals  = false;
            name inst         = head(m_trans_instances);
            m_trans_instances = tail(m_trans_instances);
            if (auto cs = try_instance(inst, use_globals))
                return cs;
        }
        while (!empty(m_instances)) {
            bool use_globals = true;
            name inst   = head(m_instances);
            m_instances = tail(m_instances);
            if (auto cs = try_instance(inst, use_globals))
                return cs;
        }
        return optional<constraints>();
    }
};

// Remarks:
//  - we only use get_class_instances and get_class_derived_trans_instances when use_globals is true
static constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context> const & C,
                                          local_context const & ctx, expr const & m, unsigned depth, bool use_globals) {
    environment const & env = C->env();
    justification j         = mk_failed_to_synthesize_jst(env, m);
    auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const &, name_generator const &) {
        if (auto cls_name_it = is_ext_class(C->tc(), meta_type)) {
            name cls_name = *cls_name_it;
            list<expr> const & ctx_lst = ctx.get_data();
            list<expr> local_insts;
            if (C->use_local_instances())
                local_insts = get_local_instances(C->tc(), ctx_lst, cls_name);
            list<name>  trans_insts, insts;
            if (use_globals) {
                if (depth == 0 && C->use_trans_instances())
                    trans_insts = get_class_derived_trans_instances(env, cls_name);
                insts       = get_class_instances(env, cls_name);
            }
            if (empty(local_insts) && empty(insts))
                return lazy_list<constraints>(); // nothing to be done
            // we are always strict with placeholders associated with classes
            return choose(std::make_shared<class_instance_elaborator>(C, ctx, meta, meta_type, local_insts, trans_insts, insts, j, depth));
        } else {
            // do nothing, type is not a class...
            return lazy_list<constraints>(constraints());
        }
    };
    bool owner      = false;
    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic), owner, j);
}

static pair<expr, constraint> mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
                                                           optional<expr> const & type, tag g, unsigned depth, bool use_globals) {
    expr m       = ctx.mk_meta(C->m_ngen, type, g);
    constraint c = mk_class_instance_cnstr(C, ctx, m, depth, use_globals);
    return mk_pair(m, c);
}

static constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context> const & C, local_context const & _ctx,
                                               expr const & m, bool is_strict, unifier_config const & cfg, delay_factor const & factor) {
    environment const & env = C->env();
    justification j         = mk_failed_to_synthesize_jst(env, m);

    auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
                         name_generator && ngen) {
        environment const & env  = C->env();
        auto cls_name_it = is_ext_class(C->tc(), meta_type);
        if (!cls_name_it) {
            // do nothing, since type is not a class.
            return lazy_list<constraints>(constraints());
        }
        local_context ctx        = _ctx.instantiate(substitution(s));
        pair<expr, justification> mj = update_meta(meta, s);
        expr new_meta            = mj.first;
        justification new_j      = mj.second;
        unsigned depth           = 0;
        bool use_globals         = true;
        constraint c             = mk_class_instance_cnstr(C, ctx, new_meta, depth, use_globals);
        unifier_config new_cfg(cfg);
        new_cfg.m_discard        = false;
        new_cfg.m_use_exceptions = false;
        new_cfg.m_pattern        = true;
        new_cfg.m_kind           = C->m_conservative ? unifier_kind::VeryConservative : unifier_kind::Liberal;

        auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) -> constraints {
            substitution new_s = subst;
            // some constraints may have been postponed (example: universe level constraints)
            constraints  postponed = map(cnstrs,
                                         [&](constraint const & c) {
                                             // we erase internal justifications
                                             return update_justification(c, mk_composite1(j, new_j));
                                         });
            metavar_closure cls(new_meta);
            cls.add(meta_type);
            constraints cs = cls.mk_constraints(new_s, new_j);
            return append(cs, postponed);
        };

        auto no_solution_fn = [=]() {
            if (is_strict)
                return lazy_list<constraints>();
            else
                return lazy_list<constraints>(constraints());
        };

        unify_result_seq seq1    = unify(env, 1, &c, std::move(ngen), substitution(), new_cfg);
        unify_result_seq seq2    = filter(seq1, [=](pair<substitution, constraints> const & p) {
                substitution new_s = p.first;
                expr result = new_s.instantiate(new_meta);
                // We only keep complete solutions (modulo universe metavariables)
                return !has_expr_metavar_relaxed(result);
            });

        if (try_multiple_instances(env, *cls_name_it)) {
            lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
                    return to_cnstrs_fn(p.first, p.second);
                });
            if (is_strict) {
                return seq3;
            } else {
                // make sure it does not fail by appending empty set of constraints
                return append(seq3, lazy_list<constraints>(constraints()));
            }
        } else {
            auto p  = seq2.pull();
            if (!p)
                return no_solution_fn();
            else
                return lazy_list<constraints>(to_cnstrs_fn(p->first.first, p->first.second));
        }
    };
    bool owner = false;
    return mk_choice_cnstr(m, choice_fn, factor, owner, j);
}

/** \brief Create a metavariable, and attach choice constraint for generating
    solutions using class-instances
*/
pair<expr, constraint> mk_old_class_instance_elaborator(
    environment const & env, io_state const & ios, local_context const & ctx,
    name const & prefix, optional<name> const & suffix, bool use_local_instances,
    bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
    pos_info_provider const * pip) {
    auto C       = std::make_shared<class_instance_context>(env, ios, prefix, use_local_instances);
    expr m       = ctx.mk_meta(C->m_ngen, suffix, type, g);
    C->set_main_meta(m);
    if (pip)
        C->set_pos(pip->get_file_name(), pip->get_pos_info(m));
    constraint c = mk_class_instance_root_cnstr(C, ctx, m, is_strict, cfg, delay_factor());
    return mk_pair(m, c);
}

pair<expr, constraint> mk_class_instance_elaborator(
    environment const & env, io_state const & ios, local_context const & ctx,
    name const & prefix, optional<name> const & suffix, bool use_local_instances,
    bool is_strict, optional<expr> const & type, tag g,
    pos_info_provider const * pip) {
    if (is_standard(env) || get_class_force_new(ios.get_options())) {
        return mk_new_class_instance_elaborator(env, ios, ctx, prefix, suffix, use_local_instances,
                                                is_strict, type, g, pip);
    } else {
        unifier_config cfg(ios.get_options(), true /* use exceptions */, true /* discard */);
        return mk_old_class_instance_elaborator(env, ios, ctx, prefix, suffix, use_local_instances,
                                                is_strict, type, g, cfg, pip);
    }
}
}