feat(frontends/lean/elaborator): coercions to sort

library/init/coe.lean

@@ -17,8 +17,11 @@ of ambiguity.
 
 All coercions and lifts can be identified with the constant coe.
 
-We also have a has_coe_to_fun type class for encoding coercions from
+We use the has_coe_to_fun type class for encoding coercions from
 a type to a function space.
+
+We use the has_coe_to_sort type class for encoding coercions from
+a type to a sort.
 -/
 prelude
 import init.list init.subtype init.prod
@@ -40,6 +43,9 @@ structure has_coe_t [class] (A B : Type) :=
 structure has_coe_to_fun [class] (A : Type) :=
 (F : Type) (coe : A → F)
 
+structure has_coe_to_sort [class] (A : Type) :=
+(S : Type) (coe : A → S)
+
 definition lift {A B : Type} [has_lift A B] : A → B :=
 @has_lift.lift A B _
 
@@ -63,12 +69,17 @@ lift_t
 definition coe_fn {A : Type} [has_coe_to_fun A] : A → has_coe_to_fun.F A :=
 has_coe_to_fun.coe
 
+definition coe_sort {A : Type} [has_coe_to_sort A] : A → has_coe_to_sort.S A :=
+has_coe_to_sort.coe
+
 /- Notation -/
 
 notation `↑`:max a:max := coe a
 
 notation `⇑`:max a:max := coe_fn a
 
+notation `↥`:max a:max := coe_sort a
+
 /- Transitive closure for has_lift, has_coe, has_coe_to_fun -/
 
 definition lift_trans [instance] {A B C : Type} [has_lift A B] [has_lift_t B C] : has_lift_t A C :=
@@ -86,6 +97,9 @@ has_coe_t.mk coe_b
 definition coe_fn_trans [instance] {A B : Type} [has_lift_t A B] [has_coe_to_fun B] : has_coe_to_fun A :=
 has_coe_to_fun.mk (has_coe_to_fun.F B) (λ a, coe_fn (coe a))
 
+definition coe_sort_trans [instance] {A B : Type} [has_lift_t A B] [has_coe_to_sort B] : has_coe_to_sort A :=
+has_coe_to_sort.mk (has_coe_to_sort.S B) (λ a, coe_sort (coe a))
+
 /- Every coercion is also a lift -/
 
 definition coe_to_lift [instance] {A B : Type} [has_coe_t A B] : has_lift_t A B :=

src/frontends/lean/elaborator.cpp

@@ -353,41 +353,43 @@ expr elaborator::enforce_type(expr const & e, expr const & expected_type, char c
     }
 }
 
-void elaborator::trace_coercion_fn_failure(expr const & e_type, expr const & ref, char const * error_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 ");
             msg += format(pos_string_for(ref));
             msg += space() + format("from");
             msg += pp_indent(e_type);
-            msg += line() + format("to function space");
+            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_fun(expr const & e, expr const & _e_type, expr const & ref) {
+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, get_coe_fn_name(), 3, mask, args);
+            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_pi(new_e_type)) {
-                trace_coercion_fn_failure(e_type, ref,
-                                          "coercion was successfully generated, but resulting type is not a Pi");
-                return none_expr();
+            if ((is_fn && is_pi(new_e_type)) || (!is_fn && is_sort(new_e_type))) {
+                return some_expr(new_e);
             }
-            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");
         } catch (app_builder_exception & ex) {
-            trace_coercion_fn_failure(e_type, ref,
-                                      "failed create 'coe_fn' application using type class resolution "
-                                      "('set_option trace.app_builder true' and 'set_option trace.class_instances true' for more information)");
+            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_failure(e_type, ref,
-                                  "was not considered because type contain metavariables");
+        trace_coercion_fn_sort_failure(is_fn, e_type, ref,
+                                       "was not considered because type contain metavariables");
         return none_expr();
     }
 }
@@ -397,7 +399,7 @@ expr elaborator::ensure_function(expr const & e, expr const & ref) {
     if (is_pi(e_type)) {
         return e;
     }
-    if (auto r = mk_coercion_to_fun(e, e_type, ref)) {
+    if (auto r = mk_coercion_to_fn(e, e_type, ref)) {
         return *r;
     }
     throw elaborator_exception(ref, format("function expected at") + pp_indent(e));
@@ -417,6 +419,10 @@ expr elaborator::ensure_type(expr const & e, expr const & ref) {
         }
     }
 
+    if (auto r = mk_coercion_to_sort(e, e_type, ref)) {
+        return *r;
+    }
+
     throw elaborator_exception(ref, format("type expected at") + pp_indent(e));
 }
 

src/frontends/lean/elaborator.h

@@ -104,8 +104,16 @@ class elaborator {
     void trace_coercion_failure(expr const & e_type, expr const & type, expr const & ref, char const * error_msg);
     optional<expr> mk_coercion(expr const & e, expr const & e_type, expr const & type, expr const & ref);
 
-    void trace_coercion_fn_failure(expr const & e_type, expr const & ref, char const * error_msg);
-    optional<expr> mk_coercion_to_fun(expr const & e, expr const & _e_type, expr const & ref);
+    void trace_coercion_fn_sort_failure(bool is_fn, expr const & e_type, expr const & ref, char const * error_msg);
+    optional<expr> mk_coercion_to_fn_sort(bool is_fn, expr const & e, expr const & _e_type, expr const & ref);
+
+    optional<expr> mk_coercion_to_fn(expr const & e, expr const & e_type, expr const & ref) {
+        return mk_coercion_to_fn_sort(true, e, e_type, ref);
+    }
+
+    optional<expr> mk_coercion_to_sort(expr const & e, expr const & e_type, expr const & ref) {
+        return mk_coercion_to_fn_sort(false, e, e_type, ref);
+    }
 
     expr ensure_type(expr const & e, expr const & ref);
     expr ensure_function(expr const & e, expr const & ref);

src/library/constants.cpp

@@ -31,6 +31,7 @@ name const * g_classical_prop_decidable = nullptr;
 name const * g_classical_type_decidable_eq = nullptr;
 name const * g_coe = nullptr;
 name const * g_coe_fn = nullptr;
+name const * g_coe_sort = nullptr;
 name const * g_coe_to_lift = nullptr;
 name const * g_combinator_K = nullptr;
 name const * g_comm_ring = nullptr;
@@ -90,7 +91,6 @@ name const * g_has_to_string = nullptr;
 name const * g_has_zero = nullptr;
 name const * g_has_zero_zero = nullptr;
 name const * g_has_coe_t = nullptr;
-name const * g_has_coe_to_fun = nullptr;
 name const * g_heq = nullptr;
 name const * g_heq_refl = nullptr;
 name const * g_heq_symm = nullptr;
@@ -354,6 +354,7 @@ void initialize_constants() {
     g_classical_type_decidable_eq = new name{"classical", "type_decidable_eq"};
     g_coe = new name{"coe"};
     g_coe_fn = new name{"coe_fn"};
+    g_coe_sort = new name{"coe_sort"};
     g_coe_to_lift = new name{"coe_to_lift"};
     g_combinator_K = new name{"combinator", "K"};
     g_comm_ring = new name{"comm_ring"};
@@ -413,7 +414,6 @@ void initialize_constants() {
     g_has_zero = new name{"has_zero"};
     g_has_zero_zero = new name{"has_zero", "zero"};
     g_has_coe_t = new name{"has_coe_t"};
-    g_has_coe_to_fun = new name{"has_coe_to_fun"};
     g_heq = new name{"heq"};
     g_heq_refl = new name{"heq", "refl"};
     g_heq_symm = new name{"heq", "symm"};
@@ -678,6 +678,7 @@ void finalize_constants() {
     delete g_classical_type_decidable_eq;
     delete g_coe;
     delete g_coe_fn;
+    delete g_coe_sort;
     delete g_coe_to_lift;
     delete g_combinator_K;
     delete g_comm_ring;
@@ -737,7 +738,6 @@ void finalize_constants() {
     delete g_has_zero;
     delete g_has_zero_zero;
     delete g_has_coe_t;
-    delete g_has_coe_to_fun;
     delete g_heq;
     delete g_heq_refl;
     delete g_heq_symm;
@@ -1001,6 +1001,7 @@ name const & get_classical_prop_decidable_name() { return *g_classical_prop_deci
 name const & get_classical_type_decidable_eq_name() { return *g_classical_type_decidable_eq; }
 name const & get_coe_name() { return *g_coe; }
 name const & get_coe_fn_name() { return *g_coe_fn; }
+name const & get_coe_sort_name() { return *g_coe_sort; }
 name const & get_coe_to_lift_name() { return *g_coe_to_lift; }
 name const & get_combinator_K_name() { return *g_combinator_K; }
 name const & get_comm_ring_name() { return *g_comm_ring; }
@@ -1060,7 +1061,6 @@ name const & get_has_to_string_name() { return *g_has_to_string; }
 name const & get_has_zero_name() { return *g_has_zero; }
 name const & get_has_zero_zero_name() { return *g_has_zero_zero; }
 name const & get_has_coe_t_name() { return *g_has_coe_t; }
-name const & get_has_coe_to_fun_name() { return *g_has_coe_to_fun; }
 name const & get_heq_name() { return *g_heq; }
 name const & get_heq_refl_name() { return *g_heq_refl; }
 name const & get_heq_symm_name() { return *g_heq_symm; }

src/library/constants.h

@@ -33,6 +33,7 @@ name const & get_classical_prop_decidable_name();
 name const & get_classical_type_decidable_eq_name();
 name const & get_coe_name();
 name const & get_coe_fn_name();
+name const & get_coe_sort_name();
 name const & get_coe_to_lift_name();
 name const & get_combinator_K_name();
 name const & get_comm_ring_name();
@@ -92,7 +93,6 @@ name const & get_has_to_string_name();
 name const & get_has_zero_name();
 name const & get_has_zero_zero_name();
 name const & get_has_coe_t_name();
-name const & get_has_coe_to_fun_name();
 name const & get_heq_name();
 name const & get_heq_refl_name();
 name const & get_heq_symm_name();

src/library/constants.txt

@@ -26,6 +26,7 @@ classical.prop_decidable
 classical.type_decidable_eq
 coe
 coe_fn
+coe_sort
 coe_to_lift
 combinator.K
 comm_ring
@@ -85,7 +86,6 @@ has_to_string
 has_zero
 has_zero.zero
 has_coe_t
-has_coe_to_fun
 heq
 heq.refl
 heq.symm

tests/lean/coe6.lean

@@ -0,0 +1,10 @@
+structure Group :=
+(carrier : Type) (mul : carrier → carrier → carrier) (one : carrier)
+
+definition Group_to_Type [instance] : has_coe_to_sort Group :=
+has_coe_to_sort.mk Type Group.carrier
+
+constant g : Group.{1}
+set_option pp.binder_types true
+
+#elab λ a b : g, Group.mul g a b

tests/lean/coe6.lean.expected.out

@@ -0,0 +1 @@
+λ (a b : ↥g), Group.mul g a b : ↥g → ↥g → Group.carrier g