[Merged by Bors] - feat(library/init/coe): backport has_coe_to_sort/has_coe_to_fun from Lean 4

library/init/coe.lean

@@ -46,11 +46,13 @@ class has_coe (a : Sort u) (b : Sort v) :=
 class has_coe_t (a : Sort u) (b : Sort v) :=
 (coe : a → b)
 
-class has_coe_to_fun (a : Sort u) : Sort (max u (v+1)) :=
-(F : a → Sort v) (coe : Π x, F x)
+class has_coe_to_fun (a : Sort u) (F : out_param (a → Sort v)) :
+  Sort (max u (v+1)) :=
+(coe : Π x, F x)
 
-class has_coe_to_sort (a : Sort u) : Type (max u (v+1)) :=
-(S : Sort v) (coe : a → S)
+class has_coe_to_sort (a : Sort u) (S : out_param (Sort v)) :
+  Type (max u (v+1)) :=
+(coe : a → S)
 
 def lift {a : Sort u} {b : Sort v} [has_lift a b] : a → b :=
 @has_lift.lift a b _
@@ -64,18 +66,20 @@ def coe_b {a : Sort u} {b : Sort v} [has_coe a b] : a → b :=
 def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] : a → b :=
 @has_coe_t.coe a b _
 
-def coe_fn_b {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
+def coe_fn_b {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] :
+  Π x : a, b x :=
 has_coe_to_fun.coe
 
 /-! ### User level coercion operators -/
 
 @[reducible] def coe {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
 lift_t
 
-@[reducible] def coe_fn {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
+@[reducible] def coe_fn {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] :
+  Π x : a, b x :=
 has_coe_to_fun.coe
 
-@[reducible] def coe_sort {a : Sort u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
+@[reducible] def coe_sort {a : Sort u} {b : Sort v} [has_coe_to_sort a b] : a → b :=
 has_coe_to_sort.coe
 
 /-! ### Notation -/
@@ -125,19 +129,20 @@ instance coe_option {a : Type u} : has_coe_t a (option a) :=
 class has_coe_t_aux (a : Sort u) (b : Sort v) :=
 (coe : a → b)
 
-instance coe_trans_aux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t_aux b c] [has_coe a b] : has_coe_t_aux a c :=
+instance coe_trans_aux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t_aux b c] [has_coe a b] :
+  has_coe_t_aux a c :=
 ⟨λ x : a, @has_coe_t_aux.coe b c _ (coe_b x)⟩
 
 instance coe_base_aux {a : Sort u} {b : Sort v} [has_coe a b] : has_coe_t_aux a b :=
 ⟨coe_b⟩
 
-instance coe_fn_trans {a : Sort u₁} {b : Sort u₂} [has_coe_to_fun.{u₂ u₃} b] [has_coe_t_aux a b] : has_coe_to_fun.{u₁ u₃} a :=
-{ F   := λ x, @has_coe_to_fun.F.{u₂ u₃} b _ (@has_coe_t_aux.coe a b _ x),
-  coe := λ x, coe_fn (@has_coe_t_aux.coe a b _ x) }
+instance coe_fn_trans {a : Sort u₁} {b : Sort u₂} {c : b → Sort v} [has_coe_to_fun b c]
+  [has_coe_t_aux a b] : has_coe_to_fun a (λ x, c (@has_coe_t_aux.coe a b _ x)) :=
+⟨λ x, coe_fn (@has_coe_t_aux.coe a b _ x)⟩
 
-instance coe_sort_trans {a : Sort u₁} {b : Sort u₂} [has_coe_to_sort.{u₂ u₃} b] [has_coe_t_aux a b] : has_coe_to_sort.{u₁ u₃} a :=
-{ S   := has_coe_to_sort.S.{u₂ u₃} b,
-  coe := λ x, coe_sort (@has_coe_t_aux.coe a b _ x) }
+instance coe_sort_trans {a : Sort u₁} {b : Sort u₂} {c : Sort v} [has_coe_to_sort b c] [has_coe_t_aux a b] :
+  has_coe_to_sort a c :=
+⟨λ x, coe_sort (@has_coe_t_aux.coe a b _ x)⟩
 
 /-- Every coercion is also a lift -/
 instance coe_to_lift {a : Sort u} {b : Sort v} [has_coe_t a b] : has_lift_t a b :=
@@ -151,9 +156,10 @@ instance coe_bool_to_Prop : has_coe bool Prop :=
 /-- Tactics such as the simplifier only unfold reducible constants when checking whether two terms are definitionally
    equal or a term is a proposition. The motivation is performance.
    In particular, when simplifying `p -> q`, the tactic `simp` only visits `p` if it can establish that it is a proposition.
-   Thus, we mark the following instance as `@[reducible]`, otherwise `simp` will not visit `↑p` when simplifying `↑p -> q`. -/
-@[reducible] instance coe_sort_bool : has_coe_to_sort bool :=
-⟨Prop, λ y, y = tt⟩
+   Thus, we mark the following instance as `@[reducible]`, otherwise `simp` will not visit `↑p` when simplifying `↑p -> q`.
+-/
+@[reducible] instance coe_sort_bool : has_coe_to_sort bool Prop :=
+⟨λ y, y = tt⟩
 
 instance coe_decidable_eq (x : bool) : decidable (coe x) :=
 show decidable (x = tt), from bool.decidable_eq x tt

library/init/meta/expr.lean

@@ -146,8 +146,8 @@ meta instance : has_to_string (expr elab) := ⟨expr.to_string⟩
 meta instance : has_to_format (expr elab) := ⟨λ e, e.to_string⟩
 
 /-- Coercion for letting users write (f a) instead of (expr.app f a) -/
-meta instance : has_coe_to_fun (expr elab) :=
-{ F := λ e, expr elab → expr elab, coe := λ e, expr.app e }
+meta instance : has_coe_to_fun (expr elab) (λ e, expr elab → expr elab) :=
+⟨λ e, expr.app e⟩
 
 /-- Each expression created by Lean carries a hash.
 This is calculated upon creation of the expression.

library/init/meta/widget/basic.lean

@@ -253,9 +253,8 @@ meta def ignore_props : component unit α → component π α
 meta instance : has_coe (component π empty) (component π α) :=
 ⟨component.filter_map_action (λ p x, none)⟩
 
-meta instance : has_coe_to_fun (component π α) :=
-{ F := λ c, π → html α,
-  coe := λ c p, html.of_component p c }
+meta instance : has_coe_to_fun (component π α) (λ c, π → html α) :=
+⟨λ c p, html.of_component p c⟩
 
 meta def stateful {π α : Type}
      (β σ : Type)

library/init/meta/widget/tactic_component.lean

@@ -80,8 +80,8 @@ meta def to_html : tc π α → π → tactic (html α)
 meta def to_component : tc unit α → component tactic_state α
 | c := component.map_props (λ tc, (tc,())) c
 
-meta instance cfn : has_coe_to_fun (tc π α) := ⟨λ x, π → tactic (html α), to_html⟩
+meta instance : has_coe_to_fun (tc π α) (λ x, π → tactic (html α)) := ⟨to_html⟩
 
 end tc
 
-end widget
+end widget

src/frontends/lean/decl_util.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/private.h"
 #include "library/aliases.h"
 #include "library/explicit.h"
+#include "library/constants.h"
 #include "library/reducible.h"
 #include "library/scoped_ext.h"
 #include "library/tactic/elaborate.h"
@@ -54,14 +55,14 @@ ast_id parse_univ_params(parser & p, buffer<name> & lp_names) {
 /*
 Naming instances.
 
-For `instance [...] : C t u (D x y)`, we generate the name `D.C`.
+For `instance [...] : C (D x y) t u`, we generate the name `D.C`.
 However, we remove the current namespace if it is a prefix of `C` and/or `D`.
 (Exception: if `C` *equals* the current namespace, we keep the last component of `C`.
 Otherwise, the resulting name would be the same as `D`,
 which could be a name in the current namespace.)
 The current namespace will implicitly be prepended to the resulting name.
 
-For `instance [...] : C t u α`, where `α` is a variable
+For `instance [...] : C α t u`, where `α` is a variable
 (at parse time--it might turn into a coercion later, during typechecking)
 we generate the name `C`, stripping off the current namespace if possible.
 The heuristic can fail in the presence of parameters.
@@ -109,13 +110,18 @@ optional<name> heuristic_inst_name(name const & ns, expr const & type) {
     while (is_pi(it)) it = binding_body(it);
 
     // Extract type class name.
-    expr const & C = get_app_fn(it);
+    buffer<expr> args;
+    expr const & C = get_app_args(it, args);
     if (!is_constant(C)) return {};
     name class_name = const_name(C);
 
     // Look at head symbol of last argument.
-    if (!is_app(it)) return {};
-    expr arg_head = app_arg(it);
+    if (!args.size()) return {};
+    expr arg_head = args.back();
+    if (class_name == get_has_coe_to_fun_name() || class_name == get_has_coe_to_sort_name()) {
+        // TODO(gabriel): generalize, and pick the last non-out_param argument
+        arg_head = args[0];
+    }
     while (true) {
         if (is_app(arg_head)) {
             arg_head = app_fn(arg_head);

src/frontends/lean/elaborator.cpp

@@ -769,9 +769,9 @@ optional<expr> elaborator::mk_coercion_to_fn_sort(bool is_fn, expr const & e, ex
     if (!m_coercions) return none_expr();
     expr e_type = instantiate_mvars(_e_type);
     try {
-        bool mask[3] = { true, false, true };
+        bool mask[4] = { true, false, 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 = mk_app(m_ctx, is_fn ? get_coe_fn_name() : get_coe_sort_name(), 4, 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);
@@ -2066,6 +2066,10 @@ expr elaborator::visit_anonymous_constructor(expr const & e, optional<expr> cons
     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");
+    // The expected type may be a coercion, and
+    // we need to synthesize type class instances
+    // to figure what inductive type it is.
+    synthesize();
     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") +

src/frontends/lean/pp.cpp

@@ -603,7 +603,7 @@ static bool is_coercion(expr const & e) {
 }
 
 static bool is_coercion_fn(expr const & e) {
-    return is_app_of(e, get_coe_fn_name()) && get_app_num_args(e) >= 3;
+    return is_app_of(e, get_coe_fn_name()) && get_app_num_args(e) >= 4;
 }
 
 template<class T>
@@ -628,10 +628,10 @@ auto pretty_fn<T>::pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_
     lean_assert(is_coercion_fn(e));
     buffer<expr> args;
     get_app_args(e, args);
-    if (args.size() == 3) {
-        return pp_child_at(args[2], bp, expr_address::app(args.size(), 2), ignore_hide);
+    if (args.size() == 4) {
+        return pp_child_at(args[2], bp, expr_address::app(args.size(), 3), ignore_hide);
     } else {
-        expr new_e = mk_app(args.size() - 2, args.data() + 2);
+        expr new_e = mk_app(args.size() - 3, args.data() + 3);
         // [todo] pp_child needs to know that `f` now has a different address. (see above)
         address_give_up_scope _(*this);
         return pp_child(new_e, bp, ignore_hide);

src/library/constants.cpp

@@ -74,6 +74,8 @@ name const * g_has_andthen_andthen = nullptr;
 name const * g_has_bind_and_then = nullptr;
 name const * g_has_bind_seq = nullptr;
 name const * g_has_coe_t = nullptr;
+name const * g_has_coe_to_fun = nullptr;
+name const * g_has_coe_to_sort = nullptr;
 name const * g_has_div_div = nullptr;
 name const * g_has_emptyc_emptyc = nullptr;
 name const * g_has_insert_insert = nullptr;
@@ -353,6 +355,8 @@ void initialize_constants() {
     g_has_bind_and_then = new name{"has_bind", "and_then"};
     g_has_bind_seq = new name{"has_bind", "seq"};
     g_has_coe_t = new name{"has_coe_t"};
+    g_has_coe_to_fun = new name{"has_coe_to_fun"};
+    g_has_coe_to_sort = new name{"has_coe_to_sort"};
     g_has_div_div = new name{"has_div", "div"};
     g_has_emptyc_emptyc = new name{"has_emptyc", "emptyc"};
     g_has_insert_insert = new name{"has_insert", "insert"};
@@ -633,6 +637,8 @@ void finalize_constants() {
     delete g_has_bind_and_then;
     delete g_has_bind_seq;
     delete g_has_coe_t;
+    delete g_has_coe_to_fun;
+    delete g_has_coe_to_sort;
     delete g_has_div_div;
     delete g_has_emptyc_emptyc;
     delete g_has_insert_insert;
@@ -912,6 +918,8 @@ name const & get_has_andthen_andthen_name() { return *g_has_andthen_andthen; }
 name const & get_has_bind_and_then_name() { return *g_has_bind_and_then; }
 name const & get_has_bind_seq_name() { return *g_has_bind_seq; }
 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_has_coe_to_sort_name() { return *g_has_coe_to_sort; }
 name const & get_has_div_div_name() { return *g_has_div_div; }
 name const & get_has_emptyc_emptyc_name() { return *g_has_emptyc_emptyc; }
 name const & get_has_insert_insert_name() { return *g_has_insert_insert; }

src/library/constants.h

@@ -76,6 +76,8 @@ name const & get_has_andthen_andthen_name();
 name const & get_has_bind_and_then_name();
 name const & get_has_bind_seq_name();
 name const & get_has_coe_t_name();
+name const & get_has_coe_to_fun_name();
+name const & get_has_coe_to_sort_name();
 name const & get_has_div_div_name();
 name const & get_has_emptyc_emptyc_name();
 name const & get_has_insert_insert_name();

src/library/constants.txt

@@ -69,6 +69,8 @@ has_andthen.andthen
 has_bind.and_then
 has_bind.seq
 has_coe_t
+has_coe_to_fun
+has_coe_to_sort
 has_div.div
 has_emptyc.emptyc
 has_insert.insert

tests/lean/123-1.lean

@@ -5,11 +5,8 @@ infixr ` • `:73 := has_scalar.smul
 
 structure Ring : Type.
 
-instance : has_coe_to_sort Ring :=
-{
-  S := Type,
-  coe := λ R, unit
-}
+instance : has_coe_to_sort Ring Type :=
+⟨λ R, unit⟩
 
 variables {G : Type} [has_mul G] {R : Ring}
 

tests/lean/123-1.lean.expected.out

@@ -1,4 +1,4 @@
-123-1.lean:34:18: error: don't know how to synthesize placeholder
+123-1.lean:31:18: error: don't know how to synthesize placeholder
 context:
 G : Type,
 _inst_1 : has_mul G,

tests/lean/123-2.lean

@@ -17,8 +17,9 @@ structure ring_hom' (M : Type*) (N : Type*) [semiring M] [semiring N] :=
 (map_zero' : to_fun 0 = 0)
 (map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)
 
-instance (α : Type*) (β : Type*) [semiring α] [semiring β] : has_coe_to_fun (ring_hom' α β) :=
-⟨_, λ f, ring_hom'.to_fun (f)⟩
+instance (α : Type*) (β : Type*) [semiring α] [semiring β] :
+  has_coe_to_fun (ring_hom' α β) (λ _, α → β) :=
+⟨λ f, ring_hom'.to_fun (f)⟩
 
 class algebra' (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
   extends has_scalar' R A, ring_hom' R A :=
@@ -36,7 +37,7 @@ variables {R : Type*} {A : Type*} {B : Type*}
 variables [comm_semiring R] [semiring A] [semiring B]
 variables [algebra' R A] [algebra' R B]
 
-instance : has_coe_to_fun (alg_hom' R A B) := ⟨_, λ f, f.to_fun⟩
+instance : has_coe_to_fun (alg_hom' R A B) (λ _, A → B) := ⟨λ f, f.to_fun⟩
 
 def quot.lift
   {R : Type} [comm_ring R]

tests/lean/123-2.lean.expected.out

@@ -1,4 +1,4 @@
-123-2.lean:49:17: error: don't know how to synthesize placeholder
+123-2.lean:50:17: error: don't know how to synthesize placeholder
 context:
 R : Type,
 _inst_6 : comm_ring R,

tests/lean/coe4.lean

@@ -4,9 +4,9 @@ structure Functor (A : Type u) :=
 (fn : A → A → A) (inj : ∀ x y, fn x = fn y → x = y)
 
 attribute [instance]
-definition coe_functor_to_fn (A : Type u) : has_coe_to_fun (Functor A) :=
-{ F   := λ f, A → A → A,
-  coe := Functor.fn }
+definition coe_functor_to_fn (A : Type u) :
+  has_coe_to_fun (Functor A) (λ f, A → A → A) :=
+⟨Functor.fn⟩
 
 constant f : Functor nat
 

tests/lean/coe4.lean.expected.out

@@ -1,6 +1,7 @@
 ⇑f 0 1 : ℕ
 f 0 1 : ℕ
 ⇑f 0 1 : ℕ
-@coe_fn.{1 1} (Functor.{0} nat) (coe_functor_to_fn.{0} nat) f (@has_zero.zero.{0} nat nat.has_zero)
+@coe_fn.{1 1} (Functor.{0} nat) (λ (f : Functor.{0} nat), nat → nat → nat) (coe_functor_to_fn.{0} nat) f
+  (@has_zero.zero.{0} nat nat.has_zero)
   (@has_one.one.{0} nat nat.has_one) :
   nat

tests/lean/coe5.lean

@@ -1,9 +1,8 @@
 open tactic
 
 attribute [instance]
-meta def expr_to_app : has_coe_to_fun expr :=
-{ F   := λ e, expr → expr,
-  coe := expr.app }
+meta def expr_to_app : has_coe_to_fun expr (λ e, expr → expr) :=
+⟨expr.app⟩
 
 meta constants f a b : expr
 

tests/lean/coe5.lean.expected.out

@@ -2,4 +2,7 @@
 ⇑(⇑f a) b : expr
 ⇑(⇑(⇑f a) b) a : expr
 f a b a : expr
-@coe_fn.{1 1} (expr bool.tt) expr_to_app (@coe_fn.{1 1} (expr bool.tt) expr_to_app f a) b : expr bool.tt
+@coe_fn.{1 1} (expr bool.tt) (λ (e : expr bool.tt), expr bool.tt → expr bool.tt) expr_to_app
+  (@coe_fn.{1 1} (expr bool.tt) (λ (e : expr bool.tt), expr bool.tt → expr bool.tt) expr_to_app f a)
+  b :
+  expr bool.tt

tests/lean/coe6.lean

@@ -3,8 +3,8 @@ structure Group :=
 (carrier : Type u) (mul : carrier → carrier → carrier) (one : carrier)
 
 attribute [instance]
-definition Group_to_Type : has_coe_to_sort Group :=
-{ S := Type u, coe := λ g, g^.carrier }
+definition Group_to_Type : has_coe_to_sort Group _ :=
+{ coe := λ g, g^.carrier }
 
 constant g : Group.{1}
 set_option pp.binder_types true

tests/lean/run/check_constants.lean

@@ -74,6 +74,8 @@ run_cmd script_check_id `has_andthen.andthen
 run_cmd script_check_id `has_bind.and_then
 run_cmd script_check_id `has_bind.seq
 run_cmd script_check_id `has_coe_t
+run_cmd script_check_id `has_coe_to_fun
+run_cmd script_check_id `has_coe_to_sort
 run_cmd script_check_id `has_div.div
 run_cmd script_check_id `has_emptyc.emptyc
 run_cmd script_check_id `has_insert.insert