feat(frontends/lean): add new option (elaborator.coercions) for disabling coercions

src/frontends/lean/elaborator.cpp

@@ -467,9 +467,12 @@ pair<expr, expr> 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);
+            list<expr> coes;
-            // try coercion to function-class
+            // try coercion to function-class IF coercions are enabled
-            list<expr> coes  = get_coercions_to_fun(env(), f_type);
+            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<expr, expr> 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<expr, constraint_seq> 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<expr> 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<expr> 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<expr, constraint_seq> elaborator::mk_delayed_coercion(
 pair<expr, constraint_seq> 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 &&
+    if (m_ctx.m_coercions) {
-        has_coercions_from(a_type, lifted_coe) && ((!lifted_coe && is_meta(expected_type)) || (lifted_coe && is_pi_meta(expected_type)))) {
+        if (use_expensive_coercions &&
-        return mk_delayed_coercion(a, a_type, expected_type, j);
+            has_coercions_from(a_type, lifted_coe) && ((!lifted_coe && is_meta(expected_type)) || (lifted_coe && is_pi_meta(expected_type)))) {
-    } 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);
-        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)) {
-    } else {
+            return mk_delayed_coercion(a, a_type, expected_type, j);
-        pair<bool, constraint_seq> 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);
+
+    pair<bool, constraint_seq> 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);
+            throw unifier_exception(j, substitution());
-            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());
-            }
         }
     }
 }
@@ -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<expr> coes;
-    list<expr> coes = get_coercions_to_sort(env(), t);
+    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 {

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<level> 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;
 }
 }

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;

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

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