diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 9eb05f5fa..ad8cf5095 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -467,9 +467,12 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { erase_coercion_info(f); } else { cs = saved_cs; - f_type = m_coercion_from_tc->whnf(saved_f_type, cs); - // try coercion to function-class - list coes = get_coercions_to_fun(env(), f_type); + list coes; + // try coercion to function-class IF coercions are enabled + if (m_ctx.m_coercions) { + f_type = m_coercion_from_tc->whnf(saved_f_type, cs); + coes = get_coercions_to_fun(env(), f_type); + } if (is_nil(coes)) { throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); } else if (is_nil(tail(coes))) { @@ -513,6 +516,8 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { } bool elaborator::has_coercions_from(expr const & a_type, bool & lifted_coe) { + if (!m_ctx.m_coercions) + return false; try { expr a_cls = get_app_fn(m_coercion_from_tc->whnf(a_type).first); if (m_ctx.m_lift_coercions) { @@ -529,6 +534,8 @@ bool elaborator::has_coercions_from(expr const & a_type, bool & lifted_coe) { } bool elaborator::has_coercions_to(expr d_type) { + if (!m_ctx.m_coercions) + return false; try { d_type = m_coercion_to_tc->whnf(d_type).first; expr const & fn = get_app_fn(d_type); @@ -546,10 +553,15 @@ bool elaborator::has_coercions_to(expr d_type) { } pair elaborator::apply_coercion(expr const & a, expr a_type, expr d_type, justification const & j) { + if (!m_ctx.m_coercions) { + erase_coercion_info(a); + return to_ecs(a); + } a_type = m_coercion_from_tc->whnf(a_type).first; d_type = m_coercion_to_tc->whnf(d_type).first; constraint_seq aux_cs; - list coes = get_coercions_from_to(*m_coercion_from_tc, *m_coercion_to_tc, a_type, d_type, aux_cs, m_ctx.m_lift_coercions); + list coes = get_coercions_from_to(*m_coercion_from_tc, *m_coercion_to_tc, a_type, + d_type, aux_cs, m_ctx.m_lift_coercions); if (is_nil(coes)) { erase_coercion_info(a); return to_ecs(a); @@ -604,41 +616,45 @@ pair elaborator::mk_delayed_coercion( pair elaborator::ensure_has_type_core( expr const & a, expr const & a_type, expr const & expected_type, bool use_expensive_coercions, justification const & j) { bool lifted_coe = false; - if (use_expensive_coercions && - has_coercions_from(a_type, lifted_coe) && ((!lifted_coe && is_meta(expected_type)) || (lifted_coe && is_pi_meta(expected_type)))) { - return mk_delayed_coercion(a, a_type, expected_type, j); - } else if (use_expensive_coercions && !m_in_equation_lhs && is_meta(a_type) && has_coercions_to(expected_type)) { - return mk_delayed_coercion(a, a_type, expected_type, j); - } else { - pair dcs; - try { - dcs = m_tc->is_def_eq(a_type, expected_type, j); - } catch (exception&) { - dcs.first = false; + if (m_ctx.m_coercions) { + if (use_expensive_coercions && + has_coercions_from(a_type, lifted_coe) && ((!lifted_coe && is_meta(expected_type)) || (lifted_coe && is_pi_meta(expected_type)))) { + return mk_delayed_coercion(a, a_type, expected_type, j); + } else if (use_expensive_coercions && !m_in_equation_lhs && is_meta(a_type) && has_coercions_to(expected_type)) { + return mk_delayed_coercion(a, a_type, expected_type, j); } - if (dcs.first) { - return to_ecs(a, dcs.second); + } + + pair dcs; + try { + dcs = m_tc->is_def_eq(a_type, expected_type, j); + } catch (exception&) { + dcs.first = false; + } + if (dcs.first) { + return to_ecs(a, dcs.second); + } else { + if (!m_ctx.m_coercions) + throw unifier_exception(j, substitution()); + auto new_a_cs = apply_coercion(a, a_type, expected_type, j); + expr new_a = new_a_cs.first; + constraint_seq cs = new_a_cs.second; + bool coercion_worked = false; + if (!is_eqp(a, new_a)) { + expr new_a_type = infer_type(new_a, cs); + try { + coercion_worked = m_tc->is_def_eq(new_a_type, expected_type, j, cs); + } catch (exception&) { + coercion_worked = false; + } + } + if (coercion_worked) { + return to_ecs(new_a, cs); + } else if (has_metavar(a_type) || has_metavar(expected_type)) { + // rely on unification hints to solve this constraint + return to_ecs(a, mk_eq_cnstr(a_type, expected_type, j)); } else { - auto new_a_cs = apply_coercion(a, a_type, expected_type, j); - expr new_a = new_a_cs.first; - constraint_seq cs = new_a_cs.second; - bool coercion_worked = false; - if (!is_eqp(a, new_a)) { - expr new_a_type = infer_type(new_a, cs); - try { - coercion_worked = m_tc->is_def_eq(new_a_type, expected_type, j, cs); - } catch (exception&) { - coercion_worked = false; - } - } - if (coercion_worked) { - return to_ecs(new_a, cs); - } else if (has_metavar(a_type) || has_metavar(expected_type)) { - // rely on unification hints to solve this constraint - return to_ecs(a, mk_eq_cnstr(a_type, expected_type, j)); - } else { - throw unifier_exception(j, substitution()); - } + throw unifier_exception(j, substitution()); } } } @@ -819,8 +835,11 @@ expr elaborator::ensure_type(expr const & e, constraint_seq & cs) { } } cs = saved_cs; - t = m_coercion_from_tc->whnf(saved_t, cs); - list coes = get_coercions_to_sort(env(), t); + list coes; + if (m_ctx.m_coercions) { + t = m_coercion_from_tc->whnf(saved_t, cs); + coes = get_coercions_to_sort(env(), t); + } if (is_nil(coes)) { throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); } else { diff --git a/src/frontends/lean/elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp index 62106973e..3c8691d80 100644 --- a/src/frontends/lean/elaborator_context.cpp +++ b/src/frontends/lean/elaborator_context.cpp @@ -28,6 +28,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS true #endif +#ifndef LEAN_DEFAULT_ELABORATOR_COERCIONS +#define LEAN_DEFAULT_ELABORATOR_COERCIONS true +#endif + namespace lean { // ========================================== @@ -37,6 +41,7 @@ static name * g_elaborator_ignore_instances = nullptr; static name * g_elaborator_flycheck_goals = nullptr; static name * g_elaborator_fail_missing_field = nullptr; static name * g_elaborator_lift_coercions = nullptr; +static name * g_elaborator_coercions = nullptr; name const & get_elaborator_ignore_instances_name() { return *g_elaborator_ignore_instances; @@ -62,6 +67,10 @@ bool get_elaborator_lift_coercions(options const & opts) { return opts.get_bool(*g_elaborator_lift_coercions, LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS); } +bool get_elaborator_coercions(options const & opts) { + return opts.get_bool(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS); +} + // ========================================== elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, @@ -83,6 +92,7 @@ void elaborator_context::set_options(options const & opts) { m_flycheck_goals = get_elaborator_flycheck_goals(opts); m_fail_missing_field = get_elaborator_fail_missing_field(opts); m_lift_coercions = get_elaborator_lift_coercions(opts); + m_coercions = get_elaborator_coercions(opts); if (has_show_goal(opts, m_show_goal_line, m_show_goal_col)) { m_show_goal_at = true; @@ -131,6 +141,7 @@ void initialize_elaborator_context() { g_elaborator_flycheck_goals = new name{"elaborator", "flycheck_goals"}; g_elaborator_fail_missing_field = new name{"elaborator", "fail_if_missing_field"}; g_elaborator_lift_coercions = new name{"elaborator", "lift_coercions"}; + g_elaborator_coercions = new name{"elaborator", "coercions"}; register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(elaborator) use local declarates as class instances"); register_bool_option(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES, @@ -144,6 +155,8 @@ void initialize_elaborator_context() { register_bool_option(*g_elaborator_lift_coercions, LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS, "(elaborator) if true, the elaborator will automatically lift coercions from A to B " "into coercions from (C -> A) to (C -> B)"); + register_bool_option(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS, + "(elaborator) if true, the elaborator will automatically introduce coercions"); } void finalize_elaborator_context() { delete g_elaborator_local_instances; @@ -151,5 +164,6 @@ void finalize_elaborator_context() { delete g_elaborator_flycheck_goals; delete g_elaborator_fail_missing_field; delete g_elaborator_lift_coercions; + delete g_elaborator_coercions; } } diff --git a/src/frontends/lean/elaborator_context.h b/src/frontends/lean/elaborator_context.h index 08f9763ad..f4e4f29b8 100644 --- a/src/frontends/lean/elaborator_context.h +++ b/src/frontends/lean/elaborator_context.h @@ -27,6 +27,7 @@ class elaborator_context { bool m_flycheck_goals; bool m_fail_missing_field; bool m_lift_coercions; + bool m_coercions; friend class elaborator; bool m_show_goal_at; diff --git a/tests/lean/coe2.lean b/tests/lean/coe2.lean new file mode 100644 index 000000000..caea7063f --- /dev/null +++ b/tests/lean/coe2.lean @@ -0,0 +1,20 @@ +import data.int +open nat int + +variable f : int → int +variable a : nat + +constant bv : nat → Type₁ +attribute bv [coercion] +constant g : Π {n : nat}, bv n → bv n + +set_option pp.all true + +check f a +check fun x : a, g x + + +set_option elaborator.coercions false + +check f a -- ERROR +check fun x : a, g x -- ERROR diff --git a/tests/lean/coe2.lean.expected.out b/tests/lean/coe2.lean.expected.out new file mode 100644 index 000000000..9a3a29634 --- /dev/null +++ b/tests/lean/coe2.lean.expected.out @@ -0,0 +1,12 @@ +f (int.of_nat a) : int +λ (x : bv a), @g a x : bv a → bv a +coe2.lean:19:6: error: type mismatch at application + f a +term + a +has type + nat +but is expected to have type + int +coe2.lean:20:14: error: type expected at + a