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

Author: Leonardo de Moura
*/
#include <string>
#include "util/flet.h"
#include "kernel/find_fn.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "library/trace.h"
#include "library/user_recursors.h"
#include "library/aux_recursors.h"
#include "library/app_builder.h"
#include "library/constants.h"
#include "library/placeholder.h"
#include "library/explicit.h"
#include "library/scope_pos_info_provider.h"
#include "library/choice.h"
#include "library/util.h"
#include "library/typed_expr.h"
#include "library/annotation.h"
#include "library/pp_options.h"
#include "library/flycheck.h"
#include "library/replace_visitor.h"
#include "library/error_handling.h"
#include "library/locals.h"
#include "library/private.h"
#include "library/attribute_manager.h"
#include "library/vm/vm.h"
#include "library/compiler/rec_fn_macro.h"
#include "library/compiler/vm_compiler.h"
#include "library/tactic/kabstract.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/elaborate.h"
#include "library/equations_compiler/compiler.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/util.h"
#include "frontends/lean/prenum.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/info_annotation.h"

namespace lean {
MK_THREAD_LOCAL_GET(type_context_cache_manager, get_tcm, true /* use binder information at infer_cache */);

static name * g_level_prefix = nullptr;
static name * g_elab_strategy = nullptr;

struct elaborator_strategy_attribute_data : public attr_data {
    elaborator_strategy m_status;
    elaborator_strategy_attribute_data() {}
    elaborator_strategy_attribute_data(elaborator_strategy status) : m_status(status) {}
    virtual unsigned hash() const override { return static_cast<unsigned>(m_status); }
    void write(serializer & s) const { s << static_cast<char>(m_status); }
    void read(deserializer & d) {
        char c; d >> c;
        m_status = static_cast<elaborator_strategy>(c);
    }
};

bool operator==(elaborator_strategy_attribute_data const & d1, elaborator_strategy_attribute_data const & d2) {
    return d1.m_status == d2.m_status;
}

template class typed_attribute<elaborator_strategy_attribute_data>;
typedef typed_attribute<elaborator_strategy_attribute_data> elaborator_strategy_attribute;

static elaborator_strategy_attribute const & get_elaborator_strategy_attribute() {
    return static_cast<elaborator_strategy_attribute const &>(get_system_attribute(*g_elab_strategy));
}

class elaborator_strategy_proxy_attribute : public proxy_attribute<elaborator_strategy_attribute_data> {
    typedef proxy_attribute<elaborator_strategy_attribute_data> parent;
public:
    elaborator_strategy_proxy_attribute(char const * id, char const * descr, elaborator_strategy status):
        parent(id, descr, status) {}

    virtual typed_attribute<elaborator_strategy_attribute_data> const & get_attribute() const {
        return get_elaborator_strategy_attribute();
    }
};

elaborator_strategy get_elaborator_strategy(environment const & env, name const & n) {
    if (auto data = get_elaborator_strategy_attribute().get(env, n))
        return data->m_status;

    if (inductive::is_elim_rule(env, n) ||
        is_aux_recursor(env, n) ||
        is_user_defined_recursor(env, n)) {
        return elaborator_strategy::AsEliminator;
    }

    if (inductive::is_intro_rule(env, n)) {
        return elaborator_strategy::WithExpectedType;
    }

    return elaborator_strategy::Default;
}

#define trace_elab(CODE) lean_trace("elaborator", scope_trace_env _scope(m_env, m_ctx); CODE)
#define trace_elab_detail(CODE) lean_trace("elaborator_detail", scope_trace_env _scope(m_env, m_ctx); CODE)
#define trace_elab_debug(CODE) lean_trace("elaborator_debug", scope_trace_env _scope(m_env, m_ctx); CODE)

elaborator::elaborator(environment const & env, options const & opts, metavar_context const & mctx,
                       local_context const & lctx):
    m_env(env), m_opts(opts),
    m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible) {
}

auto elaborator::mk_pp_ctx() -> pp_fn {
    return ::lean::mk_pp_ctx(m_ctx.env(), m_opts, m_ctx.mctx(), m_ctx.lctx());
}

format elaborator::pp_indent(pp_fn const & pp_fn, expr const & e) {
    unsigned i = get_pp_indent(m_opts);
    return nest(i, line() + pp_fn(e));
}

format elaborator::pp_indent(expr const & e) {
    return pp_indent(mk_pp_ctx(), e);
}

format elaborator::pp_overloads(pp_fn const & pp_fn, buffer<expr> const & fns) {
    format r("overloads:");
    r += space();
    bool first = true;
    for (expr const & fn : fns) {
        if (first) first = false; else r += format(", ");
        r += pp_fn(fn);
    }
    return paren(r);
}

static std::string pos_string_for(expr const & e) {
    pos_info_provider * provider = get_pos_info_provider();
    if (!provider) return "'unknown'";
    pos_info pos  = provider->get_pos_info_or_some(e);
    sstream s;
    s << provider->get_file_name() << ":" << pos.first << ":" << pos.second << ":";
    return s.str();
}

level elaborator::mk_univ_metavar() {
    return m_ctx.mk_univ_metavar_decl();
}

expr elaborator::mk_metavar(expr const & A, expr const & ref) {
    return copy_tag(ref, m_ctx.mk_metavar_decl(m_ctx.lctx(), A));
}

expr elaborator::mk_metavar(optional<expr> const & A, expr const & ref) {
    if (A)
        return mk_metavar(*A, ref);
    else
        return mk_metavar(mk_type_metavar(ref), ref);
}

expr elaborator::mk_type_metavar(expr const & ref) {
    level l = mk_univ_metavar();
    return mk_metavar(mk_sort(l), ref);
}

expr elaborator::mk_instance_core(local_context const & lctx, expr const & C, expr const & ref) {
    optional<expr> inst = m_ctx.mk_class_instance_at(lctx, C);
    if (!inst) {
        metavar_context mctx   = m_ctx.mctx();
        local_context new_lctx = lctx.instantiate_mvars(mctx);
        tactic_state s = ::lean::mk_tactic_state_for(m_env, m_opts, mctx, new_lctx, C);
        throw elaborator_exception(ref, format("failed to synthesize type class instance for") + line() + s.pp());
    }
    return *inst;
}

expr elaborator::mk_instance_core(expr const & C, expr const & ref) {
    return mk_instance_core(m_ctx.lctx(), C, ref);
}

expr elaborator::mk_instance(expr const & C, expr const & ref) {
    if (has_expr_metavar(C)) {
        expr inst = mk_metavar(C, ref);
        m_instances = cons(inst, m_instances);
        return inst;
    } else {
        return mk_instance_core(C, ref);
    }
}

expr elaborator::instantiate_mvars(expr const & e) {
    expr r = m_ctx.instantiate_mvars(e);
    if (r.get_tag() == nulltag)
        r.set_tag(e.get_tag());
    return r;
}

level elaborator::get_level(expr const & A, expr const & ref) {
    expr A_type = whnf(infer_type(A));
    if (is_sort(A_type)) {
        return sort_level(A_type);
    }

    if (is_meta(A_type)) {
        level l = mk_univ_metavar();
        if (try_is_def_eq(A_type, mk_sort(l))) {
            return l;
        }
    }

    auto pp_fn = mk_pp_ctx();
    throw elaborator_exception(ref, format("type expected at") + pp_indent(pp_fn, A));
}

level elaborator::replace_univ_placeholder(level const & l) {
    auto fn = [&](level const & l) {
        if (is_placeholder(l))
            return some_level(mk_univ_metavar());
        else
            return none_level();
    };
    return replace(l, fn);
}

static bool contains_placeholder(level const & l) {
    bool contains = false;
    auto fn = [&](level const & l) {
        if (contains) return false;
        if (is_placeholder(l))
            contains = true;
        return true;
    };
    for_each(l, fn);
    return contains;
}

/* Here, we say a term is first-order IF all applications are of the form (f ...) where f is a constant. */
static bool is_first_order(expr const & e) {
    return !find(e, [&](expr const & e, unsigned) {
            return is_app(e) && !is_constant(get_app_fn(e));
        });
}

bool elaborator::is_elim_elab_candidate(name const & fn) {
    return get_elaborator_strategy(m_env, fn) == elaborator_strategy::AsEliminator;
}

/** See comment at elim_info */
auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info {
    lean_assert(is_aux_recursor(m_env, fn) || inductive::is_elim_rule(m_env, fn));
    /* Remark: this is not just an optimization. The code at use_elim_elab_core
       only works for dependent elimination. */
    lean_assert(!fn.is_atomic());
    name const & I_name    = fn.get_prefix();
    optional<inductive::inductive_decl> decl = inductive::is_inductive_decl(m_env, I_name);
    lean_assert(decl);
    unsigned nparams  = decl->m_num_params;
    unsigned nindices = *inductive::get_num_indices(m_env, I_name);
    unsigned nminors  = length(decl->m_intro_rules);
    elim_info r;
    if (strcmp(fn.get_string(), "brec_on") == 0 || strcmp(fn.get_string(), "binduction_on") == 0) {
        r.m_arity      = nparams + 1 /* motive */ + nindices + 1 /* major */ + 1;
    } else {
        r.m_arity      = nparams + 1 /* motive */ + nindices + 1 /* major */ + nminors;
    }
    r.m_nexplicit  = 1 /* major premise */ + nminors;
    if (nminors == 0) {
        /* The motive is marked as explicit in builtin recursors that do not have
           minor premises */
        r.m_nexplicit++;
    }
    r.m_motive_idx = nparams;
    unsigned major_idx;
    if (inductive::is_elim_rule(m_env, fn)) {
        major_idx = nparams + 1 + nindices + nminors;
    } else {
        major_idx = nparams + 1 + nindices;
    }
    r.m_idxs = to_list(major_idx);
    return r;
}

/** See comment at elim_info */
auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
    if (!is_elim_elab_candidate(fn))
        return optional<elim_info>();
    if (is_aux_recursor(m_env, fn) || inductive::is_elim_rule(m_env, fn)) {
        return optional<elim_info>(get_elim_info_for_builtin(fn));
    }
    type_context::tmp_locals locals(m_ctx);
    declaration d     = m_env.get(fn);
    expr type         = d.get_type();
    while (is_pi(type)) {
        type = instantiate(binding_body(type), locals.push_local_from_binding(type));
    }

    buffer<expr> C_args;
    expr const & C = get_app_args(type, C_args);
    if (!is_local(C) || C_args.empty() || !std::all_of(C_args.begin(), C_args.end(), is_local)) {
        trace_elab_detail(tout() << "'eliminator' elaboration is not used for '" << fn <<
                          "' because resulting type is not of the expected form\n";);
        return optional<elim_info>();
    }

    buffer<expr> const & params = locals.as_buffer();
    optional<unsigned> _midx = params.index_of(C);
    if (!_midx)
        return optional<elim_info>();

    unsigned midx = *_midx;
    buffer<unsigned> idxs;
    buffer<bool>     found;
    found.resize(C_args.size(), false);
    unsigned i    = params.size();
    unsigned nexplicit = 0;
    while (i > 0) {
        --i;
        expr const & param = params[i];

        if (!is_explicit(local_info(param))) {
            continue;
        }
        nexplicit++;

        if (optional<unsigned> pos = C_args.index_of(param)) {
            // Parameter is an argument of the resulting type (C ...)
            if (!found[*pos]) {
                // We store it if we could not infer it using the type of other arguments.
                found[*pos] = true;
                idxs.push_back(i);
            }
            continue;
        }

        expr param_type = m_ctx.infer(param);
        if (!is_first_order(param_type))
            continue;

        bool collected = false;
        for_each(param_type, [&](expr const & e, unsigned) {
                if (is_local(e)) {
                    if (optional<unsigned> pos = C_args.index_of(e)) {
                        if (!found[*pos]) {
                            collected   = true;
                            found[*pos] = true;
                        }
                    }
                }
                return true;
            });
        if (collected)
            idxs.push_back(i);
    }

    for (unsigned i = 0; i < found.size(); i++) {
        if (!found[i]) {
            trace_elab_detail(tout() << "'eliminator' elaboration is not used for '" << fn <<
                              "' because did not find a (reliable) way to synthesize '" << C_args[i] << "' " <<
                              "which occurs in the resulting type\n";);
            return optional<elim_info>();
        }
    }

    std::reverse(idxs.begin(), idxs.end());
    trace_elab_detail(tout() << "'eliminator' elaboration is going to be used for '" << fn << "' applications, "
                      << "the motive is computed using the argument(s):";
                      for (unsigned idx : idxs) tout() << " #" << (idx+1);
                      tout() << "\n";);
    return optional<elim_info>(params.size(), nexplicit, midx, to_list(idxs));
}

/** See comment at elim_info */
auto elaborator::use_elim_elab(name const & fn) -> optional<elim_info> {
    if (auto it = m_elim_cache.find(fn))
        return *it;
    optional<elim_info> r = use_elim_elab_core(fn);
    m_elim_cache.insert(fn, r);
    return r;
}

void elaborator::trace_coercion_failure(expr const & e_type, expr const & type, expr const & ref, char const * error_msg) {
    trace_elab({
            auto pp_fn = mk_pp_ctx();
            format msg("coercion at ");
            msg += format(pos_string_for(ref));
            msg += space() + format("from");
            msg += pp_indent(pp_fn, e_type);
            msg += line() + format("to");
            msg += pp_indent(pp_fn, type);
            msg += line() + format(error_msg);
            tout() << msg << "\n";
        });
}

optional<expr> elaborator::mk_coercion(expr const & e, expr const & _e_type, expr const & _type, expr const & ref) {
    expr e_type = instantiate_mvars(_e_type);
    expr type   = instantiate_mvars(_type);
    if (!has_expr_metavar(e_type) && !has_expr_metavar(type)) {
        expr has_coe_t;
        try {
            has_coe_t = mk_app(m_ctx, get_has_coe_t_name(), e_type, type);
        } catch (app_builder_exception & ex) {
            trace_coercion_failure(e_type, type, ref,
                                   "failed create type class expression 'has_coe_t' "
                                   "('set_option trace.app_builder true' for more information)");
            return none_expr();
        }
        optional<expr> inst = m_ctx.mk_class_instance_at(m_ctx.lctx(), has_coe_t);
        if (!inst) {
            trace_coercion_failure(e_type, type, ref,
                                   "failed to synthesize 'has_coe_t' type class instance "
                                   "('set_option trace.class_instances true' for more information)");
            return none_expr();
        }
        expr coe_to_lift;
        try {
            coe_to_lift = mk_app(m_ctx, get_coe_to_lift_name(), *inst);
        } catch (app_builder_exception & ex) {
            trace_coercion_failure(e_type, type, ref,
                                   "failed convert 'has_coe_t' instance into 'has_lift_t' instance "
                                   "('set_option trace.app_builder true' for more information)");
            return none_expr();
        }
        expr coe;
        try {
            coe = mk_app(m_ctx, get_coe_name(), coe_to_lift, e);
        } catch (app_builder_exception & ex) {
            trace_coercion_failure(e_type, type, ref,
                                   "failed create 'coe' application using generated type class instance "
                                   "('set_option trace.app_builder true' for more information)");
            return none_expr();
        }
        return some_expr(coe);
    } else {
        trace_coercion_failure(e_type, type, ref,
                               "was not considered because types contain metavariables");
        return none_expr();
    }
}

bool elaborator::is_def_eq(expr const & e1, expr const & e2) {
    type_context::approximate_scope scope(m_ctx);
    return m_ctx.is_def_eq(e1, e2);
}

bool elaborator::try_is_def_eq(expr const & e1, expr const & e2) {
    snapshot S(*this);
    try {
        return is_def_eq(e1, e2);
    } catch (exception &) {
        S.restore(*this);
        throw;
    }
    S.restore(*this);
    return false;
}

optional<expr> elaborator::ensure_has_type(expr const & e, expr const & e_type, expr const & type, expr const & ref) {
    if (is_def_eq(e_type, type))
        return some_expr(e);
    return mk_coercion(e, e_type, type, ref);
}

expr elaborator::enforce_type(expr const & e, expr const & expected_type, char const * header, expr const & ref) {
    expr e_type = infer_type(e);
    if (auto r = ensure_has_type(e, e_type, expected_type, ref)) {
        return *r;
    } else {
        format msg = format(header);
        auto pp_fn = mk_pp_ctx();
        msg += format(", expression") + pp_indent(pp_fn, e);
        msg += line() + format("has type") + pp_indent(pp_fn, e_type);
        msg += line() + format("but is expected to have type") + pp_indent(pp_fn, expected_type);
        throw elaborator_exception(ref, msg);
    }
}

void elaborator::trace_coercion_fn_sort_failure(bool is_fn, expr const & e_type, expr const & ref, char const * error_msg) {
    trace_elab({
            format msg("coercion at ");
            auto pp_fn = mk_pp_ctx();
            msg += format(pos_string_for(ref));
            msg += space() + format("from");
            msg += pp_indent(pp_fn, e_type);
            if (is_fn)
                msg += line() + format("to function space");
            else
                msg += line() + format("to sort");
            msg += line() + format(error_msg);
            tout() << msg << "\n";
        });
}

optional<expr> elaborator::mk_coercion_to_fn_sort(bool is_fn, expr const & e, expr const & _e_type, expr const & ref) {
    expr e_type = instantiate_mvars(_e_type);
    if (!has_expr_metavar(e_type)) {
        try {
            bool mask[3] = { true, false, true };
            expr args[2] = { e_type, e };
            expr new_e = mk_app(m_ctx, is_fn ? get_coe_fn_name() : get_coe_sort_name(), 3, mask, args);
            expr new_e_type = whnf(infer_type(new_e));
            if ((is_fn && is_pi(new_e_type)) || (!is_fn && is_sort(new_e_type))) {
                return some_expr(new_e);
            }
            trace_coercion_fn_sort_failure(is_fn, e_type, ref,
                                           "coercion was successfully generated, but resulting type is not the expected one");
            return none_expr();
        } catch (app_builder_exception & ex) {
            trace_coercion_fn_sort_failure(is_fn, e_type, ref,
                                           "failed create coercion application using type class resolution "
                                           "('set_option trace.app_builder true' and 'set_option trace.class_instances true' for more information)");
            return none_expr();
        }
    } else {
        trace_coercion_fn_sort_failure(is_fn, e_type, ref,
                                       "was not considered because type contain metavariables");
        return none_expr();
    }
}

expr elaborator::ensure_function(expr const & e, expr const & ref) {
    expr e_type = whnf(infer_type(e));
    if (is_pi(e_type)) {
        return e;
    }
    if (auto r = mk_coercion_to_fn(e, e_type, ref)) {
        return *r;
    }
    auto pp_fn = mk_pp_ctx();
    throw elaborator_exception(ref, format("function expected at") + pp_indent(pp_fn, e));
}

expr elaborator::ensure_type(expr const & e, expr const & ref) {
    expr e_type = whnf(infer_type(e));
    if (is_sort(e_type)) {
        return e;
    }

    if (is_meta(e_type) && is_def_eq(e_type, mk_sort(mk_univ_metavar()))) {
        return e;
    }

    if (auto r = mk_coercion_to_sort(e, e_type, ref)) {
        return *r;
    }

    auto pp_fn = mk_pp_ctx();
    throw elaborator_exception(ref, format("type expected at") + pp_indent(pp_fn, e));
}

expr elaborator::visit_typed_expr(expr const & e) {
    expr ref          = e;
    expr val          = get_typed_expr_expr(e);
    expr type         = get_typed_expr_type(e);
    expr new_type;
    new_type = ensure_type(visit(type, none_expr()), type);
    synthesize_type_class_instances();
    expr new_val      = visit(val, some_expr(new_type));
    expr new_val_type = infer_type(new_val);
    if (auto r = ensure_has_type(new_val, new_val_type, new_type, ref))
        return *r;

    auto pp_fn = mk_pp_ctx();
    throw elaborator_exception(ref,
                               format("invalid type ascription, expression has type") + pp_indent(pp_fn, new_val_type) +
                               line() + format("but is expected to have type") + pp_indent(pp_fn, new_type));
}

expr elaborator::visit_prenum(expr const & e, optional<expr> const & expected_type) {
    lean_assert(is_prenum(e));
    expr ref = e;
    mpz const & v  = prenum_value(e);
    tag e_tag      = e.get_tag();
    expr A;
    if (expected_type) {
        A = *expected_type;
        if (is_metavar(*expected_type))
            m_numeral_types = cons(A, m_numeral_types);
    } else {
        A = mk_type_metavar(ref);
        m_numeral_types = cons(A, m_numeral_types);
    }
    level A_lvl = get_level(A, ref);
    levels ls(A_lvl);
    if (v.is_neg())
        throw elaborator_exception(ref, "invalid pre-numeral, it must be a non-negative value");
    if (v.is_zero()) {
        expr has_zero_A = mk_app(mk_constant(get_has_zero_name(), ls), A, e_tag);
        expr S          = mk_instance(has_zero_A, ref);
        return mk_app(mk_app(mk_constant(get_zero_name(), ls), A, e_tag), S, e_tag);
    } else {
        expr has_one_A = mk_app(mk_constant(get_has_one_name(), ls), A, e_tag);
        expr S_one     = mk_instance(has_one_A, ref);
        expr one       = mk_app(mk_app(mk_constant(get_one_name(), ls), A, e_tag), S_one, e_tag);
        if (v == 1) {
            return one;
        } else {
            expr has_add_A = mk_app(mk_constant(get_has_add_name(), ls), A, e_tag);
            expr S_add     = mk_instance(has_add_A, ref);
            std::function<expr(mpz const & v)> convert = [&](mpz const & v) {
                lean_assert(v > 0);
                if (v == 1)
                    return one;
                else if (v % mpz(2) == 0) {
                    expr r = convert(v / 2);
                    return mk_app(mk_app(mk_app(mk_constant(get_bit0_name(), ls), A, e_tag), S_add, e_tag), r, e_tag);
                } else {
                    expr r = convert(v / 2);
                    return mk_app(mk_app(mk_app(mk_app(mk_constant(get_bit1_name(), ls), A, e_tag), S_one, e_tag),
                                         S_add, e_tag), r, e_tag);
                }
            };
            return convert(v);
        }
    }
}

expr elaborator::visit_sort(expr const & e) {
    level new_l = replace_univ_placeholder(sort_level(e));
    expr r = update_sort(e, new_l);
    if (contains_placeholder(sort_level(e)))
        m_to_check_sorts.emplace_back(e, r);
    return r;
}

expr elaborator::visit_const_core(expr const & e) {
    declaration d = m_env.get(const_name(e));
    buffer<level> ls;
    for (level const & l : const_levels(e)) {
        level new_l = replace_univ_placeholder(l);
        ls.push_back(new_l);
    }
    unsigned num_univ_params = d.get_num_univ_params();
    if (num_univ_params < ls.size()) {
        format msg("incorrect number of universe levels parameters for '");
        msg += format(const_name(e)) + format("', #") + format(num_univ_params);
        msg += format(" expected, #") + format(ls.size()) + format("provided");
        throw elaborator_exception(e, msg);
    }
    // "fill" with meta universe parameters
    for (unsigned i = ls.size(); i < num_univ_params; i++)
        ls.push_back(mk_univ_metavar());
    lean_assert(num_univ_params == ls.size());
    return update_constant(e, to_list(ls.begin(), ls.end()));
}

expr elaborator::visit_function(expr const & fn, bool has_args, expr const & ref) {
    if (is_placeholder(fn)) {
        throw elaborator_exception(ref, "placeholders '_' cannot be used where a function is expected");
    }
    expr r;
    switch (fn.kind()) {
    case expr_kind::Var:
    case expr_kind::Pi:
    case expr_kind::Meta:
    case expr_kind::Sort:
        throw elaborator_exception(ref, "invalid application, function expected");
    // The expr_kind::App case can only happen when nary notation is used
    case expr_kind::App:       r = visit(fn, none_expr()); break;
    case expr_kind::Local:     r = fn; break;
    case expr_kind::Constant:  r = visit_const_core(fn); break;
    case expr_kind::Macro:     r = visit_macro(fn, none_expr(), true); break;
    case expr_kind::Lambda:    r = visit_lambda(fn, none_expr()); break;
    case expr_kind::Let:       r = visit_let(fn, none_expr()); break;
    }
    if (has_args)
        r = ensure_function(r, ref);
    return r;
}

void elaborator::validate_overloads(buffer<expr> const & fns, expr const & ref) {
    for (expr const & fn_i : fns) {
        if (is_constant(fn_i) && use_elim_elab(const_name(fn_i))) {
            auto pp_fn = mk_pp_ctx();
            format msg("invalid overloaded application, "
                       "elaborator has special support for '");
            msg += pp_fn(fn_i);
            msg += format("' (it is handled as an \"eliminator\"), "
                          "but this kind of constant cannot be overloaded "
                          "(solution: use fully qualified names) ");
            msg += pp_overloads(pp_fn, fns);
            return throw elaborator_exception(ref, msg);
        }
    }
}

format elaborator::mk_app_type_mismatch_error(expr const & t, expr const & arg, expr const & arg_type,
                                              expr const & expected_type) {
    auto pp_fn = mk_pp_ctx();
    format msg = format("type mismatch at application");
    msg += pp_indent(pp_fn, t);
    msg += line() + format("term");
    msg += pp_indent(pp_fn, arg);
    msg += line() + format("has type");
    msg += pp_indent(pp_fn, arg_type);
    msg += line() + format("but is expected to have type");
    msg += pp_indent(pp_fn, expected_type);
    return msg;
}

format elaborator::mk_too_many_args_error(expr const & fn_type) {
    auto pp_fn = mk_pp_ctx();
    return
        format("invalid function application, too many arguments, function type:") +
        pp_indent(pp_fn, fn_type);
}

void elaborator::throw_app_type_mismatch(expr const & t, expr const & arg, expr const & arg_type, expr const & expected_type,
                                         expr const & ref) {
    throw elaborator_exception(ref, mk_app_type_mismatch_error(t, arg, arg_type, expected_type));
}

expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<expr> const & args,
                                optional<expr> const & _expected_type, expr const & ref) {
    trace_elab_detail(tout() << "recursor/eliminator application at " << pos_string_for(ref) << "\n";);
    lean_assert(info.m_nexplicit <= args.size());
    if (!_expected_type) {
        throw elaborator_exception(ref, format("invalid '") + format(const_name(fn)) + format ("' application, ") +
                                   format("elaborator has special support for this kind of application ") +
                                   format("(it is handled as an \"eliminator\"), ") +
                                   format("but the expected type must be known"));
    }

    expr expected_type = instantiate_mvars(*_expected_type);
    if (has_expr_metavar(expected_type)) {
        auto pp_fn = mk_pp_ctx();
        throw elaborator_exception(ref, format("invalid '") + format(const_name(fn)) + format ("' application, ") +
                                   format("elaborator has special support for this kind of application ") +
                                   format("(it is handled as an \"eliminator\"), ") +
                                   format("but expected type must not contain metavariables") +
                                   pp_indent(pp_fn, expected_type));
    }

    trace_elab_debug(
        tout() << "eliminator elaboration for '" << fn << "'\n"
        << "  arity:     " << info.m_arity << "\n"
        << "  nexplicit: " << info.m_nexplicit << "\n"
        << "  motive:    #" << (info.m_motive_idx+1) << "\n"
        << "  \"major\":  ";
        for (unsigned idx : info.m_idxs)
            tout() << " #" << (idx+1);
        tout() << "\n";);

    expr fn_type = try_to_pi(infer_type(fn));
    buffer<expr> new_args;

    /* In the first pass we only process the arguments at info.m_idxs */
    expr type = fn_type;
    unsigned i = 0;
    unsigned j = 0;
    list<unsigned> main_idxs  = info.m_idxs;
    buffer<optional<expr>> postponed_args; // mark arguments that must be elaborated in the second pass.
    {
        while (is_pi(type)) {
            expr const & d = binding_domain(type);
            binder_info const & bi = binding_info(type);
            expr new_arg;
            optional<expr> postponed;
            if (std::find(main_idxs.begin(), main_idxs.end(), i) != main_idxs.end()) {
                {
                    new_arg = visit(args[j], some_expr(d));
                    synthesize();
                    new_arg = instantiate_mvars(new_arg);
                }
                j++;
                if (has_expr_metavar(new_arg)) {
                    auto pp_fn = mk_pp_ctx();
                    throw elaborator_exception(ref, format("invalid '") + format(const_name(fn)) +
                                               format ("' application, ") +
                                               format("elaborator has special support for this kind of application ") +
                                               format("(it is handled as an \"eliminator\"), ") +
                                               format("but term") + pp_indent(pp_fn, new_arg) +
                                               line() + format("must not contain metavariables because") +
                                               format(" it is used to compute the motive"));
                }
                expr new_arg_type = infer_type(new_arg);
                if (!is_def_eq(new_arg_type, d)) {
                    throw elaborator_exception(ref, mk_app_type_mismatch_error(mk_app(fn, i+1, new_args.data()),
                                                                               new_arg, new_arg_type, d));
                }
            } else if (is_explicit(bi)) {
                expr arg_ref = args[j];
                new_arg      = mk_metavar(d, arg_ref);
                postponed    = args[j];
                j++;
            } else if (bi.is_inst_implicit()) {
                new_arg = mk_instance(d, ref);
            } else {
                new_arg = mk_metavar(d, ref);
            }
            new_args.push_back(new_arg);
            postponed_args.push_back(postponed);
            type = try_to_pi(instantiate(binding_body(type), new_arg));
            i++;
        }

        lean_assert(new_args.size() == info.m_arity);

        /* Process extra arguments */
        for (; j < args.size(); j++) {
            new_args.push_back(visit(args[j], none_expr()));
        }
        synthesize();
    }

    /* Compute expected_type for the recursor application without extra arguments */
    buffer<expr> extra_args;
    i = new_args.size();
    while (i > info.m_arity) {
        --i;
        expr new_arg      = instantiate_mvars(new_args[i]);
        expr new_arg_type = instantiate_mvars(infer_type(new_arg));
        expected_type     = ::lean::mk_pi("_a", new_arg_type, kabstract(m_ctx, expected_type, new_arg));
        extra_args.push_back(new_arg);
    }
    new_args.shrink(i);
    std::reverse(extra_args.begin(), extra_args.end());

    // Compute motive */
    trace_elab_debug(tout() << "compute motive by using keyed-abstraction:\n  " <<
                     instantiate_mvars(type) << "\nwith\n  " <<
                     expected_type << "\n";);
    expr motive = expected_type;
    buffer<expr> keys;
    get_app_args(type, keys);
    i = keys.size();
    while (i > 0) {
        --i;
        expr k = instantiate_mvars(keys[i]);
        expr k_type    = infer_type(k);
        motive = ::lean::mk_lambda("_x", k_type, kabstract(m_ctx, motive, k));
    }
    trace_elab_debug(tout() << "motive:\n  " << instantiate_mvars(motive) << "\n";);

    expr motive_arg = new_args[info.m_motive_idx];
    if (!is_def_eq(motive_arg, motive)) {
        throw elaborator_exception(ref, "\"eliminator\" elaborator failed to compute the motive");
    }

    /* Elaborate postponed arguments */
    for (unsigned i = 0; i < new_args.size(); i++) {
        if (optional<expr> arg = postponed_args[i]) {
            lean_assert(is_metavar(new_args[i]));
            expr new_arg_type = instantiate_mvars(infer_type(new_args[i]));
            expr new_arg      = visit(*arg, some_expr(new_arg_type));
            if (!is_def_eq(new_args[i], new_arg)) {
                auto pp_fn = mk_pp_ctx();
                throw elaborator_exception(ref, format("\"eliminator\" elaborator type mismatch, term") +
                                           pp_indent(pp_fn, new_arg) +
                                           line() + format("has type") +
                                           pp_indent(pp_fn, infer_type(new_arg)) +
                                           line() + format("but is expected to have type") +
                                           pp_indent(pp_fn, new_arg_type));
            } else {
                new_args[i] = new_arg;
            }
        }
    }

    expr r = instantiate_mvars(mk_app(mk_app(fn, new_args), extra_args));
    trace_elab_debug(tout() << "elaborated recursor:\n  " << r << "\n";);
    return r;
}

optional<expr> elaborator::visit_app_with_expected(expr const & fn, buffer<expr> const & args,
                                                   expr const & expected_type, expr const & ref) {
    snapshot C(*this);
    buffer<expr> args_mvars;
    buffer<expr> args_expected_types;
    buffer<expr> new_args;
    /* new_args_size[i] contains size of new_args after args_mvars[i] was pushed.
       We need this information for producing error messages. */
    buffer<unsigned> new_args_size;
    expr fn_type          = infer_type(fn);
    expr type_before_whnf = fn_type;
    expr type             = whnf(fn_type);
    buffer<expr>     new_instances;
    /* new_instances_size[i] contains the size of new_instances before (and after) args_mvars[i]
       was pushed. */
    buffer<unsigned> new_instances_size;
    unsigned i   = 0;
    /* First pass: compute type for an fn-application, and unify it with expected_type.
       We don't visit expelicit arguments at this point. */
    while (is_pi(type)) {
        binder_info const & bi = binding_info(type);
        expr const & d = binding_domain(type);
        if (bi.is_strict_implicit() && i == args.size())
            break;
        expr new_arg;
        if (!is_explicit(bi)) {
            // implicit argument
            new_arg = mk_metavar(d, ref);
            if (bi.is_inst_implicit())
                new_instances.push_back(new_arg);
            // implicit arguments are tagged as inaccessible in patterns
            if (m_in_pattern)
                new_arg = copy_tag(ref, mk_inaccessible(new_arg));
        } else if (i < args.size()) {
            // explicit argument
            expr const & arg_ref = args[i];
            i++;
            args_expected_types.push_back(d);
            new_arg      = mk_metavar(d, arg_ref);
            args_mvars.push_back(new_arg);
            new_args_size.push_back(new_args.size());
            new_instances_size.push_back(new_instances.size());
        } else {
            break;
        }
        new_args.push_back(new_arg);
        /* See comment above at visit_default_app_core */
        type_before_whnf = instantiate(binding_body(type), new_arg);
        type             = whnf(type_before_whnf);
    }
    type = type_before_whnf;
    if (i != args.size()) {
        /* failed to consume all explicit arguments, use default elaboration for applications */
        C.restore(*this);
        return none_expr();
    }
    if (!is_def_eq(expected_type, type)) {
        /* failed to unify expected_type and computed type, use default elaboration for applications */
        C.restore(*this);
        return none_expr();
    }
    lean_assert(args_expected_types.size() == args.size());
    lean_assert(args_expected_types.size() == args_mvars.size());
    lean_assert(args_expected_types.size() == new_args_size.size());
    lean_assert(args_expected_types.size() == new_instances_size.size());
    unsigned j = 0; /* for traversing new_instances */
    /* Second pass: visit explicit arguments using the information
       we gained about their expected types */
    for (unsigned i = 0; i < args.size(); i++) {
        /* Process type class instances upto args[i] */
        for (; j < new_instances_size[i]; j++) {
            expr const & mvar = new_instances[j];
            if (!try_synthesize_type_class_instance(mvar))
                m_instances = cons(mvar, m_instances);
        }
        expr ref_arg      = args[i];
        expr new_arg      = visit(args[i], some_expr(args_expected_types[i]));
        expr new_arg_type = infer_type(new_arg);
        if (optional<expr> new_new_arg = ensure_has_type(new_arg, new_arg_type, args_expected_types[i], ref_arg)) {
            new_arg = *new_new_arg;
        } else {
            new_args.shrink(new_args_size[i]);
            new_args.push_back(new_arg);
            format msg = mk_app_type_mismatch_error(mk_app(fn, new_args.size(), new_args.data()),
                                                    new_arg, new_arg_type, args_expected_types[i]);
            throw elaborator_exception(ref, msg);
        }
        if (!is_def_eq(args_mvars[i], new_arg)) {
            throw elaborator_exception(ref_arg, "invalid application, type mismatch when assigning auxiliary metavar");
        } else {
            new_args[new_args_size[i]] = new_arg;
        }
    }
    for (; j < new_instances.size(); j++) {
        expr const & mvar = new_instances[j];
        if (!try_synthesize_type_class_instance(mvar))
            m_instances = cons(mvar, m_instances);
    }
    return some_expr(mk_app(fn, new_args.size(), new_args.data()));
}

bool elaborator::is_with_expected_candidate(expr const & fn) {
    if (!is_constant(fn)) return false;
    return get_elaborator_strategy(m_env, const_name(fn)) == elaborator_strategy::WithExpectedType;
}

expr elaborator::visit_default_app_core(expr const & _fn, arg_mask amask, buffer<expr> const & args,
                                        bool args_already_visited, optional<expr> const & expected_type, expr const & ref) {
    expr fn      = _fn;
    expr fn_type = infer_type(fn);
    unsigned i = 0;
    buffer<expr> new_args;

    /** Check if this application is a candidate for propagating the expected type to arguments */
    if (!args_already_visited && /* if the arguments have already been visited, then there is no point. */
        expected_type &&         /* the expected type must be known */
        amask == arg_mask::Default && /* we do not propagate information when @ and @@ are used */
        is_with_expected_candidate(fn)) {
        if (auto r = visit_app_with_expected(fn, args, *expected_type, ref)) {
            return *r;
        }
    }

    /* We manually track the type before whnf. We do that because after the loop
       we check whether the application type is definitionally equal to expected_type.
       Suppose, the result type is (tactic expr) and the expected type is (?M1 ?M2).
       The unification problem can be solved using first-order unification, but if we
       unfold (tactic expr), we get (tactic_state -> base_tactic_result ...) which cannot.

       The statement
         expr type = try_to_pi(fn_type);
       also does not work because (tactic expr) unfolds into a type. */
    expr type_before_whnf = fn_type;
    expr type             = whnf(fn_type);
    while (true) {
        if (is_pi(type)) {
            binder_info const & bi = binding_info(type);
            expr const & d = binding_domain(type);
            expr new_arg;
            if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size())
                break;
            if ((amask == arg_mask::Default && !is_explicit(bi)) ||
                (amask == arg_mask::Simple && !bi.is_inst_implicit() && !is_first_order(d))) {
                // implicit argument
                if (bi.is_inst_implicit())
                    new_arg = mk_instance(d, ref);
                else
                    new_arg = mk_metavar(d, ref);
                // implicit arguments are tagged as inaccessible in patterns
                if (m_in_pattern)
                    new_arg = copy_tag(ref, mk_inaccessible(new_arg));
            } else if (i < args.size()) {
                // explicit argument
                expr ref_arg = args[i];
                if (args_already_visited)
                    new_arg = args[i];
                else
                    new_arg = visit(args[i], some_expr(d));
                expr new_arg_type = infer_type(new_arg);
                if (optional<expr> new_new_arg = ensure_has_type(new_arg, new_arg_type, d, ref_arg)) {
                    new_arg = *new_new_arg;
                } else {
                    new_args.push_back(new_arg);
                    format msg = mk_app_type_mismatch_error(mk_app(fn, new_args.size(), new_args.data()),
                                                            new_arg, new_arg_type, d);
                    throw elaborator_exception(ref, msg);
                }
                i++;
            } else {
                break;
            }
            new_args.push_back(new_arg);
            /* See comment above at first type_before_whnf assignment */
            type_before_whnf = instantiate(binding_body(type), new_arg);
            type             = whnf(type_before_whnf);
        } else if (i < args.size()) {
            expr new_fn = mk_app(fn, new_args.size(), new_args.data());
            new_args.clear();
            fn = ensure_function(new_fn, ref);
            type_before_whnf = infer_type(fn);
            type = whnf(type_before_whnf);
        } else {
            lean_assert(i == args.size());
            break;
        }
    }

    type = type_before_whnf;

    expr r = mk_app(fn, new_args.size(), new_args.data());
    if (expected_type) {
        if (auto new_r = ensure_has_type(r, instantiate_mvars(type), *expected_type, ref)) {
            return *new_r;
        } else {
            /* We do not generate the error here because we can produce a better one from
               the caller (i.e., place the set the expected_type) */
        }
    }
    return r;
}

expr elaborator::visit_default_app(expr const & fn, arg_mask amask, buffer<expr> const & args,
                                   optional<expr> const & expected_type, expr const & ref) {
    return visit_default_app_core(fn, amask, args, false, expected_type, ref);
}

expr elaborator::visit_overload_candidate(expr const & fn, buffer<expr> const & args,
                                          optional<expr> const & expected_type, expr const & ref) {
    return visit_default_app_core(fn, arg_mask::Default, args, true, expected_type, ref);
}

void elaborator::throw_no_overload_applicable(buffer<expr> const & fns, buffer<elaborator_exception> const & error_msgs, expr const & ref) {
    format r("none of the overloads are applicable");
    lean_assert(error_msgs.size() == fns.size());
    for (unsigned i = 0; i < fns.size(); i++) {
        if (i > 0) r += line();
        auto pp_fn = mk_pp_ctx();
        format f_fmt = (is_constant(fns[i])) ? format(const_name(fns[i])) : pp_fn(fns[i]);
        r += line() + format("error for") + space() + f_fmt;
        r += line() + error_msgs[i].pp();
    }
    throw elaborator_exception(ref, r);
}

expr elaborator::visit_overloaded_app(buffer<expr> const & fns, buffer<expr> const & args,
                                      optional<expr> const & expected_type, expr const & ref) {
    trace_elab_detail(tout() << "overloaded application at " << pos_string_for(ref);
                      auto pp_fn = mk_pp_ctx();
                      tout() << pp_overloads(pp_fn, fns) << "\n";);
    buffer<expr> new_args;
    for (expr const & arg : args) {
        new_args.push_back(copy_tag(arg, visit(arg, none_expr())));
    }

    snapshot S(*this);

    buffer<pair<expr, snapshot>> candidates;
    buffer<elaborator_exception> error_msgs;
    for (expr const & fn : fns) {
        try {
            // Restore state
            S.restore(*this);
            bool has_args = !args.empty();
            expr new_fn   = visit_function(fn, has_args, ref);
            expr c        = visit_overload_candidate(new_fn, new_args, expected_type, ref);
            synthesize_type_class_instances();

            if (expected_type) {
                expr c_type = infer_type(c);
                if (ensure_has_type(c, c_type, *expected_type, ref)) {
                    candidates.emplace_back(c, snapshot(*this));
                } else {
                    auto pp_fn = mk_pp_ctx();
                    throw elaborator_exception(ref, format("invalid overload, expression") + pp_indent(pp_fn, c) +
                                               line() + format("has type") + pp_indent(pp_fn, c_type) +
                                               line() + format("but is expected to have type") +
                                               pp_indent(pp_fn, *expected_type));
                }
            } else {
                candidates.emplace_back(c, snapshot(*this));
            }
        } catch (elaborator_exception & ex) {
            error_msgs.push_back(ex);
        } catch (exception & ex) {
            error_msgs.push_back(elaborator_exception(ref, format(ex.what())));
        }
    }
    lean_assert(candidates.size() + error_msgs.size() == fns.size());

    if (candidates.empty()) {
        S.restore(*this);

        throw_no_overload_applicable(fns, error_msgs, ref);
    } else if (candidates.size() > 1) {
        S.restore(*this);

        options new_opts = m_opts.update_if_undef(get_pp_full_names_name(), true);
        flet<options> set_opts(m_opts, new_opts);
        auto pp_fn = mk_pp_ctx();
        format r("ambiguous overload, possible interpretations");
        for (auto const & c : candidates) {
            r += pp_indent(pp_fn, c.first);
        }
        throw elaborator_exception(ref, r);
    } else {
        // Restore successful state
        candidates[0].second.restore(*this);
        return candidates[0].first;
    }
}

expr elaborator::visit_no_confusion(expr const & fn, buffer<expr> const & args, optional<expr> const & expected_type, expr const & ref) {
    name fn_name = const_name(fn);
    if (!expected_type) {
        throw elaborator_exception(ref, format("invalid '") + format(fn_name) + format ("' application, ") +
                                   format("elaborator has special support for no_confusion ") +
                                   format("but the expected type must be known"));
    }
    if (args.empty()) {
        throw elaborator_exception(ref,
                                   format("invalid occurrence of function '") + format(fn_name) +
                                   format ("', it must be applied to at least one argument (possible solution: use '@')"));
    }
    /* I.no_confusion functions have a type of the form

       Pi (params) (indices) (C : Type) (lhs rhs : I params indices) (H : lhs = rhs), I.no_confusion_type params indices C lhs rhs

       The type (I.no_confusion_type params indices C lhs rhs) is C if lhs and rhs are distinct constructors,
       and (Pi Hs, C) if they are the same constructor where Hs is a sequence of equalities.

       (C : Type) is the expected type.

       To make the elaborator more effective, we first elaborate the first explicit argument (i.e., args[0]) and obtain Heq,
       and create the fake pre-term

       (I.no_confusion _ ... _ (as-is expected_type) _ _ (as-is Heq) args[1] ... args[n-1])

       Then, we elaborate this new fake pre-term.
    */
    expr Heq      = strict_visit(args[0], none_expr());
    name I_name   = fn_name.get_prefix();
    unsigned nparams  = *inductive::get_num_params(m_env, I_name);
    unsigned nindices = *inductive::get_num_indices(m_env, I_name);
    buffer<expr> new_args;
    for (unsigned i = 0; i < nparams + nindices; i++) {
        new_args.push_back(copy_tag(ref, mk_expr_placeholder()));
    }
    new_args.push_back(copy_tag(ref, mk_as_is(*expected_type)));
    new_args.push_back(copy_tag(ref, mk_expr_placeholder())); // lhs
    new_args.push_back(copy_tag(ref, mk_expr_placeholder())); // rhs
    new_args.push_back(copy_tag(args[0], mk_as_is(Heq)));
    for (unsigned i = 1; i < args.size(); i++)
        new_args.push_back(args[i]);
    return visit_default_app_core(fn, arg_mask::All, new_args, false, expected_type, ref);
}

expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type,
                                expr const & ref) {
    arg_mask amask = arg_mask::Default;
    if (is_explicit(fn)) {
        fn   = get_explicit_arg(fn);
        amask = arg_mask::All;
    } else if (is_partial_explicit(fn)) {
        fn   = get_partial_explicit_arg(fn);
        amask = arg_mask::Simple;
    }

    bool has_args = !args.empty();

    if (is_choice(fn)) {
        buffer<expr> fns;
        if (amask != arg_mask::Default)
            throw elaborator_exception(ref, "invalid explicit annotation, symbol is overloaded "
                                       "(solution: use fully qualified names)");
        for (unsigned i = 0; i < get_num_choices(fn); i++) {
            expr const & fn_i = get_choice(fn, i);
            fns.push_back(fn_i);
        }
        validate_overloads(fns, ref);
        return visit_overloaded_app(fns, args, expected_type, ref);
    } else {
        expr new_fn = visit_function(fn, has_args, ref);
        /* Check if we should use a custom elaboration procedure for this application. */
        if (is_constant(new_fn) && amask == arg_mask::Default) {
            if (auto info = use_elim_elab(const_name(new_fn))) {
                if (args.size() >= info->m_nexplicit) {
                    return visit_elim_app(new_fn, *info, args, expected_type, ref);
                } else {
                    trace_elab(tout() << pos_string_for(ref) << " 'eliminator' elaboration is not used for '" << fn <<
                               "' because it is not fully applied, #" << info->m_nexplicit <<
                               " explicit arguments expected\n";);
                }
            } else if (is_no_confusion(m_env, const_name(new_fn))) {
                return visit_no_confusion(new_fn, args, expected_type, ref);
            }
        }
        return visit_default_app(new_fn, amask, args, expected_type, ref);
    }
}

expr elaborator::visit_local(expr const & e, optional<expr> const & expected_type) {
    return visit_app_core(e, buffer<expr>(), expected_type, e);
}

expr elaborator::visit_constant(expr const & e, optional<expr> const & expected_type) {
    return visit_app_core(e, buffer<expr>(), expected_type, e);
}

expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type) {
    buffer<expr> args;
    expr const & fn = get_app_args(e, args);
    if (is_equations(fn))
        return visit_convoy(e, expected_type);
    else
        return visit_app_core(fn, args, expected_type, e);
}

expr elaborator::visit_by(expr const & e, optional<expr> const & expected_type) {
    lean_assert(is_by(e));
    expr tac = strict_visit(get_by_arg(e), some_expr(mk_tactic_unit()));
    expr const & ref = e;
    expr mvar        = mk_metavar(expected_type, ref);
    m_tactics = cons(mk_pair(mvar, tac), m_tactics);
    trace_elab(tout() << "tactic for ?m_" << get_metavar_decl_ref_suffix(mvar) << " at " <<
               pos_string_for(mvar) << "\n" << tac << "\n";);
    return mvar;
}

expr elaborator::visit_anonymous_constructor(expr const & e, optional<expr> const & expected_type) {
    lean_assert(is_anonymous_constructor(e));
    buffer<expr> args;
    expr const & c = get_app_args(get_anonymous_constructor_arg(e), args);
    if (!expected_type)
        throw elaborator_exception(e, "invalid constructor ⟨...⟩, expected type must be known");
    expr I = get_app_fn(m_ctx.relaxed_whnf(instantiate_mvars(*expected_type)));
    if (!is_constant(I))
        throw elaborator_exception(e, format("invalid constructor ⟨...⟩, expected type is not an inductive type") +
                                   pp_indent(*expected_type));
    name I_name = const_name(I);
    if (is_private(m_env, I_name))
        throw elaborator_exception(e, "invalid constructor ⟨...⟩, type is a private inductive datatype");
    if (!inductive::is_inductive_decl(m_env, I_name))
        throw elaborator_exception(e, sstream() << "invalid constructor ⟨...⟩, '" << I_name << "' is not an inductive type");
    buffer<name> c_names;
    get_intro_rule_names(m_env, I_name, c_names);
    if (c_names.size() != 1)
        throw elaborator_exception(e, sstream() << "invalid constructor ⟨...⟩, '" << I_name << "' must have only one constructor");
    expr type = m_env.get(c_names[0]).get_type();
    unsigned num_explicit = 0;
    while (is_pi(type)) {
        if (is_explicit(binding_info(type)))
            num_explicit++;
        type = binding_body(type);
    }
    if (num_explicit > 1 && args.size() > num_explicit) {
        unsigned num_extra = args.size() - num_explicit;
        expr rest = copy_tag(e, mk_app(c, num_extra + 1, args.data() + num_explicit - 1));
        rest = copy_tag(e, mk_anonymous_constructor(rest));
        args.shrink(num_explicit);
        args.back() = rest;
    }
    expr new_e = copy_tag(e, mk_app(mk_constant(c_names[0]), args));
    return visit(new_e, expected_type);
}

static expr get_equations_fn_type(expr const & eqns) {
    buffer<expr> eqs;
    to_equations(eqns, eqs);
    lean_assert(!eqs.empty());
    lean_assert(is_lambda(eqs[0]));
    return binding_domain(eqs[0]);
}

static expr instantiate_rev(expr const & e, type_context::tmp_locals const & locals) {
    return instantiate_rev(e, locals.as_buffer().size(), locals.as_buffer().data());
}

static expr update_equations_fn_type(expr const & eqns, expr const & new_fn_type) {
    expr fn_type = mk_as_is(new_fn_type);
    buffer<expr> eqs;
    to_equations(eqns, eqs);
    for (expr & eq : eqs) {
        lean_assert(is_lambda(eq));
        eq = update_binding(eq, fn_type, binding_body(eq));
    }
    return update_equations(eqns, eqs);
}

expr elaborator::visit_convoy(expr const & e, optional<expr> const & expected_type) {
    lean_assert(is_app(e));
    lean_assert(is_equations(get_app_fn(e)));
    expr const & ref = e;
    buffer<expr> args, new_args;
    expr const & eqns = get_app_args(e, args);
    lean_assert(equations_num_fns(eqns) == 1);
    lean_assert(equations_size(eqns) > 0);
    expr fn_type = get_equations_fn_type(eqns);
    expr new_fn_type;
    if (is_placeholder(fn_type)) {
        /* User did not provide the type for the match,
           we try to infer one using expected_type and the type of the arguments */
        if (!expected_type)
            throw elaborator_exception(ref, "invalid match/convoy expression, expected type is not known");
        for (unsigned i = 0; i < args.size(); i++)
            new_args.push_back(visit(args[i], none_expr()));
        synthesize();
        new_fn_type = *expected_type;
        unsigned i = args.size();
        while (i > 0) {
            --i;
            expr new_arg      = instantiate_mvars(new_args[i]);
            expr new_arg_type = instantiate_mvars(infer_type(new_arg));
            new_fn_type       = ::lean::mk_pi("_a", new_arg_type, kabstract(m_ctx, new_fn_type, new_arg));
        }
    } else {
        // User provided some typing information for the match
        type_context::tmp_locals locals(m_ctx);
        expr it = fn_type;
        for (unsigned i = 0; i < args.size(); i++) {
            if (!is_pi(it))
                throw elaborator_exception(it, "type expected in match-expression");
            expr d        = instantiate_rev(binding_domain(it), locals);
            expr new_d    = visit(d, none_expr());
            new_d         = ensure_type(new_d, binding_domain(it));
            expr expected = replace_locals(new_d, locals.as_buffer(), new_args);
            expr new_arg  = visit(args[i], some_expr(expected));
            new_arg       = enforce_type(new_arg, expected, "type mismatch in match expression", args[i]);
            locals.push_local(binding_name(it), new_d, binding_info(it));
            it            = binding_body(it);
            new_args.push_back(new_arg);
        }
        if (is_placeholder(it)) {
            synthesize();
            if (!expected_type)
                throw elaborator_exception(ref, "invalid match/convoy expression, expected type is not known");
            new_fn_type = *expected_type;
            unsigned i = args.size();
            while (i > 0) {
                --i;
                new_args[i]  = instantiate_mvars(new_args[i]);
                new_fn_type  = instantiate(kabstract(m_ctx, new_fn_type, new_args[i]), locals.as_buffer()[i]);
            }
            new_fn_type = locals.mk_pi(new_fn_type);
        } else {
            expr b      = instantiate_rev(it, locals);
            expr new_b  = visit(b, none_expr());
            synthesize();
            new_fn_type = locals.mk_pi(instantiate_mvars(new_b));
        }
    }
    new_fn_type = instantiate_mvars(new_fn_type);
    if (has_expr_metavar(new_fn_type)) {
        auto pp_fn = mk_pp_ctx();
        throw elaborator_exception(ref, format("invalid match/convoy expression, type contains meta-variables") +
                                   pp_indent(pp_fn, new_fn_type));
    }
    trace_elab(tout() << "match/convoy function type: " << new_fn_type << "\n";);
    expr new_eqns = visit_equations(update_equations_fn_type(eqns, new_fn_type));
    expr fn       = get_equations_result(new_eqns, 0);
    return mk_app(fn, new_args);
}

/** \brief Given two binding expressions \c source and \c target
    s.t. they have at least \c num binders, replace the first \c num binders of \c target with \c source.
    The binder types are wrapped with \c mk_as_is to make sure the elaborator will not process
    them again. */
static expr copy_domain(unsigned num, expr const & source, expr const & target) {
    if (num == 0) {
        return target;
    } else {
        lean_assert(is_binding(source) && is_binding(target));
        return update_binding(source, mk_as_is(binding_domain(source)),
                              copy_domain(num-1, binding_body(source), binding_body(target)));
    }
}

static void check_equations_arity(buffer<expr> const & eqns) {
    buffer<optional<unsigned>> fidx2arity;
    for (expr eqn : eqns) {
        unsigned nbinders = 0;
        expr curr = eqn;
        while (is_lambda(eqn)) {
            nbinders++;
            eqn = binding_body(eqn);
        }
        if (is_equation(eqn)) {
            expr const & lhs = equation_lhs(eqn);
            expr const & fn  = get_app_fn(lhs);
            unsigned arity   = get_app_num_args(lhs);
            if (!is_var(fn) || var_idx(fn) >= nbinders)
                throw elaborator_exception(eqn, "ill-formed match/equations expression");
            unsigned fidx    = nbinders - var_idx(fn) - 1;
            if (fidx >= fidx2arity.size())
                fidx2arity.resize(fidx+1, optional<unsigned>());
            if (auto r = fidx2arity[fidx]) {
                if (*r != arity) {
                    throw elaborator_exception(eqn, "invalid match/equations expression, "
                                               "each case must have the same number of patterns");
                }
            } else {
                fidx2arity[fidx] = arity;
            }
        } else if (is_no_equation(eqn)) {
            /* do nothing */
        } else {
            throw elaborator_exception(curr, "ill-formed match/equations expression");
        }
    }
}

expr elaborator::visit_equations(expr const & e) {
    expr const & ref = e;
    buffer<expr> eqs;
    buffer<expr> new_eqs;
    optional<expr> new_R;
    optional<expr> new_Rwf;
    flet<list<expr_pair>> save_stack(m_inaccessible_stack, m_inaccessible_stack);
    list<expr_pair> saved_inaccessible_stack = m_inaccessible_stack;
    equations_header const & header = get_equations_header(e);
    unsigned num_fns = header.m_num_fns;
    to_equations(e, eqs);
    lean_assert(!eqs.empty());

    if (is_wf_equations(e)) {
        new_R   = visit(equations_wf_rel(e), none_expr());
        new_Rwf = visit(equations_wf_proof(e), none_expr());
        expr wf = mk_app(m_ctx, get_well_founded_name(), *new_R);
        new_Rwf = enforce_type(*new_Rwf, wf, "invalid well-founded relation proof", ref);
    }

    optional<expr> first_eq;
    for (expr const & eq : eqs) {
        expr new_eq;
        buffer<expr> fns_locals;
        fun_to_telescope(eq, fns_locals, optional<binder_info>());
        list<expr> locals = to_list(fns_locals.begin() + num_fns, fns_locals.end());
        if (first_eq) {
            // Replace first num_fns domains of eq with the ones in first_eq.
            // This is a trick/hack to ensure the fns in each equation have
            // the same elaborated type.
            new_eq   = copy_tag(eq, visit(copy_domain(num_fns, *first_eq, eq), none_expr()));
        } else {
            new_eq   = copy_tag(eq, visit(eq, none_expr()));
            first_eq = new_eq;
        }
        new_eqs.push_back(new_eq);
    }
    check_equations_arity(new_eqs);
    synthesize();
    check_inaccessible(saved_inaccessible_stack);
    expr new_e;
    if (new_R) {
        new_e = copy_tag(e, mk_equations(header, new_eqs.size(), new_eqs.data(), *new_R, *new_Rwf));
    } else {
        new_e = copy_tag(e, mk_equations(header, new_eqs.size(), new_eqs.data()));
    }
    new_e = instantiate_mvars(new_e);
    ensure_no_unassigned_metavars(new_e);
    metavar_context mctx = m_ctx.mctx();
    expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e);
    m_ctx.set_env(m_env);
    m_ctx.set_mctx(mctx);
    return r;
}

void elaborator::check_pattern_inaccessible_annotations(expr const & p) {
    if (is_app(p)) {
        buffer<expr> args;
        expr const & c = get_app_args(p, args);
        if (is_constant(c)) {
            if (optional<name> I_name = inductive::is_intro_rule(m_env, const_name(c))) {
                /* Make sure the inductive datatype parameters are marked as inaccessible */
                unsigned nparams = *inductive::get_num_params(m_env, *I_name);
                for (unsigned i = 0; i < nparams && i < args.size(); i++) {
                    if (!is_inaccessible(args[i])) {
                        throw elaborator_exception(c, "invalid pattern, in a constructor application, "
                                                   "the parameters of the inductive datatype must be marked as inaccessible");
                    }
                }
            }
            // TODO(Leo): we should add a similar check for derived constructors.
            // What about constants marked as pattern? Example: @add
            // Option: check again at elim_match. The error message will not be nice,
            // but it is better than nothing.
        }
        for (expr const & a : args) {
            check_pattern_inaccessible_annotations(a);
        }
    }
}

void elaborator::check_inaccessible_annotations(expr const & lhs) {
    buffer<expr> patterns;
    get_app_args(lhs, patterns);
    for (expr const & p : patterns) {
        check_pattern_inaccessible_annotations(p);
    }
}

expr elaborator::visit_equation(expr const & eq) {
    expr const & lhs = equation_lhs(eq);
    expr const & rhs = equation_rhs(eq);
    expr lhs_fn = get_app_fn(lhs);
    if (is_explicit_or_partial_explicit(lhs_fn))
        lhs_fn = get_explicit_or_partial_explicit_arg(lhs_fn);
    if (!is_local(lhs_fn))
        throw exception("ill-formed equation");
    expr new_lhs;
    {
        flet<bool> set(m_in_pattern, true);
        new_lhs = visit(lhs, none_expr());
        check_inaccessible_annotations(new_lhs);
        synthesize_no_tactics();
    }
    expr new_lhs_type = instantiate_mvars(infer_type(new_lhs));
    expr new_rhs      = visit(rhs, some_expr(new_lhs_type));
    new_rhs = enforce_type(new_rhs, new_lhs_type, "equation type mismatch", eq);
    return copy_tag(eq, mk_equation(new_lhs, new_rhs));
}

expr elaborator::visit_inaccessible(expr const & e, optional<expr> const & expected_type) {
    if (!m_in_pattern)
        throw elaborator_exception(e, "invalid occurrence of 'inaccessible' annotation, "
                                   "it must only occur in patterns");
    expr const & ref = e;
    expr m = mk_metavar(expected_type, ref);
    expr a = get_annotation_arg(e);
    expr new_a;
    {
        flet<bool> set(m_in_pattern, false);
        new_a = visit(a, expected_type);
    }
    m_inaccessible_stack = cons(mk_pair(m, new_a), m_inaccessible_stack);
    return copy_tag(e, mk_inaccessible(m));
}

expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
    if (is_as_is(e)) {
        return get_as_is_arg(e);
    } else if (is_anonymous_constructor(e)) {
        if (is_app_fn)
            throw elaborator_exception(e, "invalid constructor ⟨...⟩, function expected");
        return visit_anonymous_constructor(e, expected_type);
    } else if (is_prenum(e)) {
        return visit_prenum(e, expected_type);
    } else if (is_typed_expr(e)) {
        return visit_typed_expr(e);
    } else if (is_choice(e) || is_explicit(e) || is_partial_explicit(e)) {
        return visit_app_core(e, buffer<expr>(), expected_type, e);
    } else if (is_by(e)) {
        return visit_by(e, expected_type);
    } else if (is_equations(e)) {
        lean_assert(!is_app_fn); // visit_convoy is used in this case
        return visit_equations(e);
    } else if (is_equation(e)) {
        lean_assert(!is_app_fn);
        return visit_equation(e);
    } else if (is_inaccessible(e)) {
        if (is_app_fn)
            throw elaborator_exception(e, "invalid inaccessible term, function expected");
        return visit_inaccessible(e, expected_type);
    } else if (is_no_info(e)) {
        // TODO(Leo): flet<bool> let(m_no_info, true);
        return visit(get_annotation_arg(e), expected_type);
    } else if (is_notation_info(e)) {
        // flet<bool> let(m_no_info, true);
        expr r = visit(get_annotation_arg(e), expected_type);
        // save_type_data(e, r);
        return r;
    } else if (is_as_atomic(e)) {
        /* ignore annotation */
        expr new_e = visit(get_as_atomic_arg(e), none_expr());
        if (is_app_fn)
            return new_e;
        /* If the as_atomic macro is not the the function in a function application, then we need to consume
           implicit arguments. */
        return visit_default_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
    } else if (is_annotation(e)) {
        expr r = visit(get_annotation_arg(e), expected_type);
        return update_macro(e, 1, &r);
    } else {
        buffer<expr> args;
        for (unsigned i = 0; i < macro_num_args(e); i++)
            args.push_back(visit(macro_arg(e, i), none_expr()));
        return update_macro(e, args.size(), args.data());
    }
}

/* If the instance fingerprint has been set, then make sure `type` is not a local instance.
   Then, add a new local declaration to locals. */
expr elaborator::push_local(type_context::tmp_locals & locals,
                            name const & n, expr const & type, binder_info const & binfo, expr const & /* ref */) {
#if 0 // TODO(Leo): the following check is too restrictive
    if (m_ctx.lctx().get_instance_fingerprint() &&
        m_ctx.is_class(type)) {
        throw elaborator_exception(ref, "invalid occurrence of local instance, it must be a declaration parameter");
    }
#endif
    return locals.push_local(n, type, binfo);
}

/* See method above */
expr elaborator::push_let(type_context::tmp_locals & locals,
                          name const & n, expr const & type, expr const & value, expr const & /* ref */) {
#if 0 // TODO(Leo): the following check is too restrictive
    if (m_ctx.lctx().get_instance_fingerprint() &&
        m_ctx.is_class(type)) {
        throw elaborator_exception(ref, "invalid occurrence of local instance, it must be a declaration parameter");
    }
#endif
    return locals.push_let(n, type, value);
}

expr elaborator::visit_lambda(expr const & e, optional<expr> const & expected_type) {
    type_context::tmp_locals locals(m_ctx);
    expr it  = e;
    expr ex;
    bool has_expected;
    if (expected_type) {
        ex = instantiate_mvars(*expected_type);
        has_expected = true;
    } else {
        has_expected = false;
    }
    while (is_lambda(it)) {
        if (has_expected) {
            ex = try_to_pi(ex);
            if (!is_pi(ex))
                has_expected = false;
        }
        expr d     = instantiate_rev(binding_domain(it), locals);
        expr new_d = visit(d, none_expr());
        if (has_expected) {
            expr ex_d = binding_domain(ex);
            try_is_def_eq(new_d, ex_d);
        }
        new_d  = ensure_type(new_d, binding_domain(it));
        expr ref = binding_domain(it);
        expr l   = push_local(locals, binding_name(it), new_d, binding_info(it), ref);
        it = binding_body(it);
        if (has_expected) {
            lean_assert(is_pi(ex));
            ex = instantiate(binding_body(ex), l);
        }
    }
    expr b = instantiate_rev(it, locals);
    expr new_b;
    if (has_expected) {
        new_b = visit(b, some_expr(ex));
    } else {
        new_b = visit(b, none_expr());
    }
    synthesize();
    expr r = locals.mk_lambda(new_b);
    return r;
}

expr elaborator::visit_pi(expr const & e) {
    type_context::tmp_locals locals(m_ctx);
    expr it  = e;
    while (is_pi(it)) {
        expr d     = instantiate_rev(binding_domain(it), locals);
        expr new_d = visit(d, none_expr());
        new_d      = ensure_type(new_d, binding_domain(it));
        expr ref   = binding_domain(it);
        push_local(locals, binding_name(it), new_d, binding_info(it), ref);
        it = binding_body(it);
    }
    expr b     = instantiate_rev(it, locals);
    expr new_b = visit(b, none_expr());
    new_b      = ensure_type(new_b, it);
    synthesize();
    expr r = locals.mk_pi(new_b);
    return r;
}

expr elaborator::visit_let(expr const & e, optional<expr> const & expected_type) {
    expr ref = e;
    expr new_type  = visit(let_type(e), none_expr());
    synthesize_no_tactics();
    expr new_value = visit(let_value(e), some_expr(new_type));
    new_value      = enforce_type(new_value, new_type, "invalid let-expression", let_value(e));
    synthesize();
    new_type       = instantiate_mvars(new_type);
    new_value      = instantiate_mvars(new_value);
    ensure_no_unassigned_metavars(new_value);
    type_context::tmp_locals locals(m_ctx);
    push_let(locals, let_name(e), new_type, new_value, ref);
    expr body      = instantiate_rev(let_body(e), locals);
    expr new_body  = visit(body, expected_type);
    expr new_e     = locals.mk_lambda(new_body);
    return new_e;
}

expr elaborator::visit_placeholder(expr const & e, optional<expr> const & expected_type) {
    expr const & ref = e;
    return mk_metavar(expected_type, ref);
}

static bool is_have_expr(expr const & e) {
    return is_app(e) && is_have_annotation(app_fn(e)) && is_lambda(get_annotation_arg(app_fn(e)));
}

expr elaborator::strict_visit(expr const & e, optional<expr> const & expected_type) {
    expr r = visit(e, expected_type);
    synthesize();
    r = instantiate_mvars(r);
    ensure_no_unassigned_metavars(r);
    return r;
}

expr elaborator::visit_have_expr(expr const & e, optional<expr> const & expected_type) {
    lean_assert(is_have_expr(e));
    expr lambda     = get_annotation_arg(app_fn(e));
    expr type       = binding_domain(lambda);
    expr proof      = app_arg(e);
    expr new_type   = visit(type, none_expr());
    synthesize_no_tactics();
    new_type        = ensure_type(new_type, type);
    expr new_proof  = visit(proof, some_expr(new_type));
    new_proof       = enforce_type(new_proof, new_type, "invalid have-expression", proof);
    synthesize();
    ensure_no_unassigned_metavars(new_proof);
    type_context::tmp_locals locals(m_ctx);
    expr ref        = binding_domain(lambda);
    push_local(locals, binding_name(lambda), new_type, binding_info(lambda), ref);
    expr body       = instantiate_rev(binding_body(lambda), locals);
    expr new_body   = visit(body, expected_type);
    expr new_lambda = locals.mk_lambda(new_body);
    return mk_app(mk_have_annotation(new_lambda), new_proof);
}

expr elaborator::visit_suffices_expr(expr const & e, optional<expr> const & expected_type) {
    lean_assert(is_suffices_annotation(e));
    expr body = get_annotation_arg(e);
    if (!is_app(body)) throw elaborator_exception(e, "ill-formed suffices expression");
    expr fn   = app_fn(body);
    expr rest = app_arg(body);
    if (!is_lambda(fn)) throw elaborator_exception(e, "ill-formed suffices expression");
    expr new_fn;
    expr type     = binding_domain(fn);
    expr new_type = visit(type, none_expr());
    synthesize_no_tactics();
    {
        type_context::tmp_locals locals(m_ctx);
        expr ref        = binding_domain(fn);
        push_local(locals, binding_name(fn), new_type, binding_info(fn), ref);
        expr body       = instantiate_rev(binding_body(fn), locals);
        expr new_body   = visit(body, expected_type);
        synthesize();
        new_fn          = locals.mk_lambda(new_body);
    }
    expr new_rest = visit(rest, some_expr(new_type));
    return mk_suffices_annotation(mk_app(new_fn, new_rest));
}

expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
    flet<unsigned> inc_depth(m_depth, m_depth+1);
    trace_elab_detail(tout() << "[" << m_depth << "] visiting\n" << e << "\n";
                      if (expected_type) tout() << "expected type:\n" << instantiate_mvars(*expected_type) << "\n";);
    if (is_placeholder(e)) {
        return visit_placeholder(e, expected_type);
    } else if (is_have_expr(e)) {
        return visit_have_expr(e, expected_type);
    } else if (is_suffices_annotation(e)) {
        return visit_suffices_expr(e, expected_type);
    } else {
        switch (e.kind()) {
        case expr_kind::Var:        lean_unreachable();  // LCOV_EXCL_LINE
        case expr_kind::Meta:       return e;
        case expr_kind::Sort:       return visit_sort(e);
        case expr_kind::Local:      return visit_local(e, expected_type);
        case expr_kind::Constant:   return visit_constant(e, expected_type);
        case expr_kind::Macro:      return visit_macro(e, expected_type, false);
        case expr_kind::Lambda:     return visit_lambda(e, expected_type);
        case expr_kind::Pi:         return visit_pi(e);
        case expr_kind::App:        return visit_app(e, expected_type);
        case expr_kind::Let:        return visit_let(e, expected_type);
        }
        lean_unreachable(); // LCOV_EXCL_LINE
    }
}

expr elaborator::get_default_numeral_type() {
    // TODO(Leo): allow user to modify default?
    return mk_constant(get_nat_name());
}

void elaborator::synthesize_numeral_types() {
    for (expr const & A : m_numeral_types) {
        if (is_metavar(instantiate_mvars(A))) {
            if (!assign_mvar(A, get_default_numeral_type()))
                throw elaborator_exception(A, "invalid numeral, failed to force numeral to be a nat");
        }
    }
    m_numeral_types = list<expr>();
}

bool elaborator::try_synthesize_type_class_instance(expr const & mvar) {
    expr inst = instantiate_mvars(mvar);
    if (!has_expr_metavar(inst)) {
        trace_elab(tout() << "skipping type class resolution at " << pos_string_for(mvar)
                   << ", placeholder instantiated using type inference\n";);
        return true;
    }
    expr inst_type = instantiate_mvars(infer_type(inst));
    if (has_expr_metavar(inst_type))
        return false;
    metavar_decl mdecl = *m_ctx.mctx().get_metavar_decl(mvar);
    expr ref = mvar;
    if (!is_def_eq(inst, mk_instance_core(mdecl.get_context(), inst_type, ref)))
        throw elaborator_exception(mvar, "failed to assign type class instance to placeholder");
    return true;
}

void elaborator::synthesize_type_class_instances_step() {
    buffer<expr> to_keep;
    buffer<std::tuple<expr, expr, expr>> to_process;
    for (expr const & mvar : m_instances) {
        expr inst          = instantiate_mvars(mvar);
        if (!has_expr_metavar(inst)) {
            trace_elab(tout() << "skipping type class resolution at " << pos_string_for(mvar)
                       << ", placeholder instantiated using type inference\n";);
            continue;
        }
        expr inst_type = instantiate_mvars(infer_type(inst));
        if (has_expr_metavar(inst_type)) {
            to_keep.push_back(mvar);
        } else {
            to_process.emplace_back(mvar, inst, inst_type);
        }
    }
    if (to_process.empty())
        return;
    expr mvar, inst, inst_type;
    for (std::tuple<expr, expr, expr> const & curr : to_process) {
        std::tie(mvar, inst, inst_type) = curr;
        metavar_decl mdecl = *m_ctx.mctx().get_metavar_decl(mvar);
        expr ref = mvar;
        if (!is_def_eq(inst, mk_instance_core(mdecl.get_context(), inst_type, ref)))
            throw elaborator_exception(mvar, "failed to assign type class instance to placeholder");
    }
    m_instances = to_list(to_keep);
}

void elaborator::synthesize_type_class_instances() {
    while (true) {
        auto old_instances = m_instances;
        synthesize_type_class_instances_step();
        if (is_eqp(old_instances, m_instances))
            return;
    }
}

static void throw_unsolved_tactic_state(tactic_state const & ts, format const & fmt, expr const & ref) {
    format msg = fmt + line() + format("state:") + line() + ts.pp();
    throw elaborator_exception(ref, msg);
}

static void throw_unsolved_tactic_state(tactic_state const & ts, char const * msg, expr const & ref) {
    throw_unsolved_tactic_state(ts, format(msg), ref);
}

tactic_state elaborator::mk_tactic_state_for(expr const & mvar) {
    metavar_context mctx = m_ctx.mctx();
    metavar_decl mdecl   = *mctx.get_metavar_decl(mvar);
    local_context lctx   = mdecl.get_context().instantiate_mvars(mctx);
    expr type            = mctx.instantiate_mvars(mdecl.get_type());
    m_ctx.set_mctx(mctx);
    return ::lean::mk_tactic_state_for(m_env, m_opts, mctx, lctx, type);
}

void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
    expr const & ref = mvar;
    /* Build initial state */
    trace_elab(tout() << "executing tactic at " << pos_string_for(ref) << "\n";);
    tactic_state s       = mk_tactic_state_for(mvar);
    metavar_context mctx = m_ctx.mctx();
    trace_elab(tout() << "initial tactic state\n" << s.pp() << "\n";);

    /* Compile tactic into bytecode */
    name tactic_name("_tactic");
    expr tactic_type = mk_tactic_unit();
    environment new_env = m_env;
    bool use_conv_opt    = true;
    bool is_trusted      = false;
    auto cd = check(new_env, mk_definition(new_env, tactic_name, {}, tactic_type, tactic, use_conv_opt, is_trusted));
    new_env = new_env.add(cd);
    new_env = vm_compile(new_env, new_env.get(tactic_name));

    /* Invoke tactic */
    vm_state S(new_env);
    vm_obj r = S.invoke(tactic_name, to_obj(s));

    if (optional<tactic_state> new_s = is_tactic_success(r)) {
        trace_elab(tout() << "tactic at " << pos_string_for(ref) << " succeeded\n";);
        mctx     = new_s->mctx();
        expr val = mctx.instantiate_mvars(new_s->main());
        if (has_expr_metavar(val)) {
            throw_unsolved_tactic_state(*new_s, "tactic failed, result contains meta-variables", ref);
        }
        mctx.assign(mvar, val);
        m_env = new_s->env();
        m_ctx.set_env(m_env);
        m_ctx.set_mctx(mctx);
    } else if (optional<pair<format, tactic_state>> ex = is_tactic_exception(S, m_opts, r)) {
        throw_unsolved_tactic_state(ex->second, ex->first, ref);
    } else {
        lean_unreachable();
    }
}

void elaborator::synthesize_using_tactics() {
    buffer<expr_pair> to_process;
    to_buffer(m_tactics, to_process);
    m_tactics = list<expr_pair>();
    elaborate_fn fn(nested_elaborate);
    scope_elaborate_fn scope(fn);
    for (expr_pair const & p : to_process) {
        lean_assert(is_metavar(p.first));
        invoke_tactic(p.first, p.second);
    }
}

void elaborator::synthesize_no_tactics() {
    synthesize_numeral_types();
    synthesize_type_class_instances();
}

void elaborator::synthesize() {
    synthesize_numeral_types();
    synthesize_type_class_instances();
    synthesize_using_tactics();
}

void elaborator::check_inaccessible(list<expr_pair> const & old_stack) {
    buffer<expr_pair> to_process;
    while (!is_eqp(m_inaccessible_stack, old_stack)) {
        to_process.push_back(head(m_inaccessible_stack));
        m_inaccessible_stack = tail(m_inaccessible_stack);
    }
    if (to_process.empty()) return;

    unsigned i = to_process.size();
    while (i > 0) {
        --i;
        expr_pair const & p = to_process[i];
        expr const & m = p.first;
        lean_assert(is_metavar(m));
        if (!m_ctx.is_assigned(m)) {
            throw elaborator_exception(m, "invalid use of inaccessible term, it is not fixed by other arguments");
        }
        expr v = instantiate_mvars(m);
        if (has_expr_metavar(v)) {
            throw elaborator_exception(m, format("invalid use of inaccessible term, "
                                                 "it is not completely fixed by other arguments") +
                                       pp_indent(v));
        }
        if (!is_def_eq(v, p.second)) {
            auto pp_fn = mk_pp_ctx();
            throw elaborator_exception(m, format("invalid use of inaccessible term, the provided term is") +
                                       pp_indent(pp_fn, p.second) +
                                       line() + format("but is expected to be") +
                                       pp_indent(pp_fn, v));
        }
    }
}

void elaborator::unassigned_uvars_to_params(level const & l) {
    if (!has_meta(l)) return;
    for_each(l, [&](level const & l) {
            if (!has_meta(l)) return false;
            if (is_meta(l) && !m_ctx.is_assigned(l)) {
                name r = mk_tagged_fresh_name(*g_level_prefix);
                m_ctx.assign(l, mk_param_univ(r));
            }
            return true;
        });
}

void elaborator::unassigned_uvars_to_params(expr const & e) {
    if (!has_univ_metavar(e)) return;
    for_each(e, [&](expr const & e, unsigned) {
            if (!has_univ_metavar(e)) return false;
            if (is_constant(e)) {
                for (level const & l : const_levels(e))
                    unassigned_uvars_to_params(l);
            } else if (is_sort(e)) {
                unassigned_uvars_to_params(sort_level(e));
            }
            return true;
        });
}

void elaborator::ensure_no_unassigned_metavars(expr const & e) {
    if (!has_expr_metavar(e)) return;
    metavar_context mctx = m_ctx.mctx();
    for_each(e, [&](expr const & e, unsigned) {
            if (!has_expr_metavar(e)) return false;
            if (is_metavar_decl_ref(e) && !mctx.is_assigned(e)) {
                tactic_state s = mk_tactic_state_for(e);
                throw_unsolved_tactic_state(s, "don't know how to synthesize placeholder", e);
            }
            return true;
        });
}

elaborator::snapshot::snapshot(elaborator const & e) {
    m_saved_mctx               = e.m_ctx.mctx();
    m_saved_instances          = e.m_instances;
    m_saved_numeral_types      = e.m_numeral_types;
    m_saved_tactics            = e.m_tactics;
    m_saved_inaccessible_stack = e.m_inaccessible_stack;
}

void elaborator::snapshot::restore(elaborator & e) {
    e.m_ctx.set_mctx(m_saved_mctx);
    e.m_instances          = m_saved_instances;
    e.m_numeral_types      = m_saved_numeral_types;
    e.m_tactics            = m_saved_tactics;
    e.m_inaccessible_stack = m_saved_inaccessible_stack;
}

/**
    \brief Auxiliary class for creating nice names for universe
    parameters introduced by the elaborator.

    This class also transforms remaining universe metavariables
    into parameters */
struct sanitize_param_names_fn : public replace_visitor {
    type_context &  m_ctx;
    name            m_p{"l"};
    name_set        m_L; /* All parameter names in the input expression. */
    name_map<level> m_R; /* map from tagged g_level_prefix to "clean" name not in L. */
    name_map<level> m_U; /* map from universe metavariable name to "clean" name not in L. */
    unsigned        m_idx{1};
    bool            m_sanitized{false};
    buffer<name> &  m_new_param_names;

    sanitize_param_names_fn(type_context & ctx, buffer<name> & new_lp_names):
        m_ctx(ctx), m_new_param_names(new_lp_names) {}

    level mk_param() {
        while (true) {
            name new_n = m_p.append_after(m_idx);
            m_idx++;
            if (!m_L.contains(new_n)) {
                m_new_param_names.push_back(new_n);
                return mk_param_univ(new_n);
            }
        }
    }

    level sanitize(level const & l) {
        name p("l");
        return replace(l, [&](level const & l) -> optional<level> {
                if (is_param(l)) {
                    name const & n = param_id(l);
                    if (is_tagged_by(n, *g_level_prefix)) {
                        if (auto new_l = m_R.find(n)) {
                            return some_level(*new_l);
                        } else {
                            level r = mk_param();
                            m_R.insert(n, r);
                            return some_level(r);
                        }
                    }
                } else if (is_meta(l)) {
                    if (is_metavar_decl_ref(l) && m_ctx.is_assigned(l)) {
                        return some_level(sanitize(*m_ctx.get_assignment(l)));
                    } else {
                        name const & n = meta_id(l);
                        if (auto new_l = m_U.find(n)) {
                            return some_level(*new_l);
                        } else {
                            level r = mk_param();
                            m_U.insert(n, r);
                            return some_level(r);
                        }
                    }
                }
                return none_level();
            });
    }

    virtual expr visit_constant(expr const & e) override {
        return update_constant(e, map(const_levels(e), [&](level const & l) { return sanitize(l); }));
    }

    virtual expr visit_sort(expr const & e) override {
        return update_sort(e, sanitize(sort_level(e)));
    }

    void collect_params(expr const & e) {
        lean_assert(!m_sanitized);
        m_L = collect_univ_params(e, m_L);
    }

    void collect_local_context_params() {
        lean_assert(!m_sanitized);
        m_ctx.lctx().for_each([&](local_decl const & l) {
                collect_params(m_ctx.instantiate_mvars(l.get_type()));
                if (auto v = l.get_value())
                    collect_params(m_ctx.instantiate_mvars(*v));
            });
    }

    expr sanitize(expr const & e) {
        expr r = operator()(e);
        m_sanitized = true;
        return r;
    }
};

/** When the output of the elaborator may contain meta-variables, we convert the type_context level meta-variables
    into regular kernel meta-variables. */
static expr replace_with_simple_metavars(metavar_context mctx, name_map<expr> & cache, expr const & e) {
    if (!has_expr_metavar(e)) return e;
    return replace(e, [&](expr const & e, unsigned) {
            if (!is_metavar(e)) return none_expr();
            if (auto r = cache.find(mlocal_name(e))) {
                return some_expr(*r);
            } else if (auto decl = mctx.get_metavar_decl(e)) {
                expr new_type = replace_with_simple_metavars(mctx, cache, mctx.instantiate_mvars(decl->get_type()));
                expr new_mvar = mk_metavar(mlocal_name(e), new_type);
                cache.insert(mlocal_name(e), new_mvar);
                return some_expr(new_mvar);
            } else if (is_metavar_decl_ref(e)) {
                throw exception("unexpected occurrence of internal elaboration metavariable");
            }
            return none_expr();
        });
}

expr elaborator::elaborate(expr const & e) {
    expr r = visit(e,  none_expr());
    trace_elab_detail(tout() << "result before final checkpoint\n" << r << "\n";);
    synthesize();
    return r;
}

expr elaborator::elaborate_type(expr const & e) {
    expr Type  = copy_tag(e, mk_sort(mk_level_placeholder()));
    expr new_e = copy_tag(e, mk_typed_expr(Type, e));
    return elaborate(e);
}

expr_pair elaborator::elaborate_with_type(expr const & e, expr const & e_type) {
    expr const & ref = e;
    expr new_e, new_e_type;
    {
        expr Type  = visit(copy_tag(e_type, mk_sort(mk_level_placeholder())), none_expr());
        new_e_type = visit(e_type, some_expr(Type));
        new_e      = visit(e,      some_expr(new_e_type));
        synthesize();
    }
    expr inferred_type = infer_type(new_e);
    if (auto r = ensure_has_type(new_e, inferred_type, new_e_type, ref)) {
        new_e = *r;
    } else {
        auto pp_fn = mk_pp_ctx();
        throw elaborator_exception(ref,
                                   format("type mismatch, expression") + pp_indent(pp_fn, new_e) +
                                   line() + format("has type") + pp_indent(pp_fn, inferred_type) +
                                   line() + format("but is expected to have type") + pp_indent(pp_fn, new_e_type));
    }
    return mk_pair(new_e, new_e_type);
}

void elaborator::finalize(buffer<expr> & es, buffer<name> & new_lp_names, bool check_unassigned, bool to_simple_metavar) {
    sanitize_param_names_fn S(m_ctx, new_lp_names);
    name_map<expr> to_simple_mvar_cache;
    for (expr & e : es) {
        e = instantiate_mvars(e);
        if (check_unassigned)
            ensure_no_unassigned_metavars(e);
        if (!check_unassigned && to_simple_metavar) {
            e = replace_with_simple_metavars(m_ctx.mctx(), to_simple_mvar_cache, e);
        }
        unassigned_uvars_to_params(e);
        e = instantiate_mvars(e);
        S.collect_params(e);
    }
    S.collect_local_context_params();
    for (expr & e : es) {
        e = S.sanitize(e);
    }
}

pair<expr, level_param_names> elaborator::finalize(expr const & e, bool check_unassigned, bool to_simple_metavar) {
    buffer<expr> es; es.push_back(e);
    buffer<name> new_lp_names;
    finalize(es, new_lp_names, check_unassigned, to_simple_metavar);
    return mk_pair(es[0], to_list(new_lp_names));
}

pair<expr, level_param_names>
elaborate(environment & env, options const & opts,
          metavar_context & mctx, local_context const & lctx, expr const & e,
          bool check_unassigned) {
    elaborator elab(env, opts, mctx, lctx);
    expr r = elab.elaborate(e);
    auto p = elab.finalize(r, check_unassigned, true);
    mctx = elab.mctx();
    env  = elab.env();
    return p;
}

// Auxiliary procedure for #translate
static expr translate_local_name(environment const & env, local_context const & lctx, name const & local_name,
                                 expr const & src) {
    if (auto decl = lctx.get_local_decl_from_user_name(local_name)) {
        return decl->mk_ref();
    }
    if (env.find(local_name)) {
        if (is_local(src))
            return mk_constant(local_name);
        else
            return src;
    }
    throw elaborator_exception(src, format("unknown identifier '") + format(local_name) + format("'"));
}

/** \brief Translated local constants (and undefined constants) occurring in \c e into
    local constants provided by \c ctx.
    Throw exception is \c ctx does not contain the local constant.
*/
static expr translate(environment const & env, local_context const & lctx, expr const & e) {
    auto fn = [&](expr const & e) {
        if (is_placeholder(e) || is_by(e) || is_as_is(e)) {
            return some_expr(e); // ignore placeholders, nested tactics and as_is terms
        } else if (is_constant(e)) {
            expr new_e = copy_tag(e, translate_local_name(env, lctx, const_name(e), e));
            return some_expr(new_e);
        } else if (is_local(e)) {
            expr new_e = copy_tag(e, translate_local_name(env, lctx, local_pp_name(e), e));
            return some_expr(new_e);
        } else {
            return none_expr();
        }
    };
    return replace(e, fn);
}

expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
                      expr const & e, bool relaxed) {
    elaborator elab(env, opts, mctx, lctx);
    expr r = elab.elaborate(translate(env, lctx, e));
    if (!relaxed)
        elab.ensure_no_unassigned_metavars(e);
    mctx = elab.mctx();
    env  = elab.env();
    return r;
}

void initialize_elaborator() {
    g_elab_strategy = new name("elab_strategy");
    g_level_prefix = new name("_elab_u");
    register_trace_class("elaborator");
    register_trace_class("elaborator_detail");
    register_trace_class("elaborator_debug");

    register_system_attribute(
        elaborator_strategy_attribute(
            *g_elab_strategy,
            "internal attribute for the elaborator strategy for a given constant"));

    register_system_attribute(
        elaborator_strategy_proxy_attribute(
            "elab_with_expected_type",
            "instructs elaborator that the arguments of the function application (f ...) "
            "should be elaborated using information about the expected type",
            elaborator_strategy::WithExpectedType));

    register_system_attribute(
        elaborator_strategy_proxy_attribute(
            "elab_as_eliminator",
            "instructs elaborator that the arguments of the function application (f ...) "
            "should be elaborated as f were an eliminator",
            elaborator_strategy::AsEliminator));

    register_system_attribute(
        elaborator_strategy_proxy_attribute(
            "elab_simple",
            "instructs elaborator that the arguments of the function application (f ...) "
            "should be elaborated from left to right, and without propagating information from the expected type "
            "to its arguments",
            elaborator_strategy::Default));

    register_incompatible("elab_simple", "elab_with_expected_type");
    register_incompatible("elab_simple", "elab_as_eliminator");
    register_incompatible("elab_with_expected_type", "elab_as_eliminator");
}

void finalize_elaborator() {
    delete g_level_prefix;
    delete g_elab_strategy;
}
}