From 3ebd4dde215d2845d5ddd94db7923199e7b1d89c Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 18 Mar 2021 11:52:21 -0400
Subject: [PATCH 01/16] `library/init/coe` compiles with the new
 `has_coe_to_sort`/`has_coe_to_fun`

---
 library/init/coe.lean | 37 +++++++++++++++++++++----------------
 1 file changed, 21 insertions(+), 16 deletions(-)

diff --git a/library/init/coe.lean b/library/init/coe.lean
index 604ed49d35..3b9606322d 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -42,11 +42,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 _
@@ -60,7 +62,8 @@ 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 -/
@@ -68,10 +71,11 @@ has_coe_to_fun.coe
 @[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 -/
@@ -123,19 +127,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 -/
 
@@ -152,8 +157,8 @@ instance coe_bool_to_Prop : has_coe bool Prop :=
    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⟩
+@[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

From 0ed322e686de01d035caa1579132d9fe72a674ad Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 17:11:54 +0100
Subject: [PATCH 02/16] Fix number of coercion arguments.

---
 src/frontends/lean/elaborator.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 1b4b2b18b5..6256edbf88 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/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);

From 428317f3e13d97371514f98ecd872ad547a07720 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 18 Mar 2021 13:56:52 -0400
Subject: [PATCH 03/16] Fix library/ and some tests

---
 library/init/meta/expr.lean                    | 4 ++--
 library/init/meta/widget/basic.lean            | 5 ++---
 library/init/meta/widget/tactic_component.lean | 4 ++--
 tests/lean/123-1.lean                          | 7 ++-----
 tests/lean/123-1.lean.expected.out             | 2 +-
 tests/lean/123-2.lean                          | 7 ++++---
 tests/lean/123-2.lean.expected.out             | 2 +-
 tests/lean/coe4.lean                           | 6 +++---
 tests/lean/coe5.lean                           | 5 ++---
 tests/lean/run/coe_fn_mvar.lean                | 8 ++++----
 tests/lean/run/coe_to_fn.lean                  | 7 ++-----
 tests/lean/run/coe_to_sort.lean                | 6 +++---
 12 files changed, 28 insertions(+), 35 deletions(-)

diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index d9f1002ad3..bd718cb8cb 100644
--- a/library/init/meta/expr.lean
+++ b/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 expr.has_coe_to_fun : 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.
diff --git a/library/init/meta/widget/basic.lean b/library/init/meta/widget/basic.lean
index 7a26f127e8..370dd295ca 100644
--- a/library/init/meta/widget/basic.lean
+++ b/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 component.has_coe_to_fun : has_coe_to_fun (component π α) (λ c, π → html α) :=
+⟨λ c p, html.of_component p c⟩
 
 meta def stateful {π α : Type}
      (β σ : Type)
diff --git a/library/init/meta/widget/tactic_component.lean b/library/init/meta/widget/tactic_component.lean
index 781fdd8dd7..2bf6d13cc4 100644
--- a/library/init/meta/widget/tactic_component.lean
+++ b/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 cfn : has_coe_to_fun (tc π α) (λ x, π → tactic (html α)) := ⟨to_html⟩
 
 end tc
 
-end widget
\ No newline at end of file
+end widget
diff --git a/tests/lean/123-1.lean b/tests/lean/123-1.lean
index 3d0e130af3..0298853012 100644
--- a/tests/lean/123-1.lean
+++ b/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}
 
diff --git a/tests/lean/123-1.lean.expected.out b/tests/lean/123-1.lean.expected.out
index a319010ae3..b71cd15415 100644
--- a/tests/lean/123-1.lean.expected.out
+++ b/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,
diff --git a/tests/lean/123-2.lean b/tests/lean/123-2.lean
index ec11ba2d19..609ccbf1c4 100644
--- a/tests/lean/123-2.lean
+++ b/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 ring_hom'.has_coe_to_fun (α : 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 alg_hom'.has_coe_to_fun : has_coe_to_fun (alg_hom' R A B) (λ _, A → B) := ⟨λ f, f.to_fun⟩
 
 def quot.lift
   {R : Type} [comm_ring R]
diff --git a/tests/lean/123-2.lean.expected.out b/tests/lean/123-2.lean.expected.out
index 229fefbdbe..d82c4a7ff4 100644
--- a/tests/lean/123-2.lean.expected.out
+++ b/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,
diff --git a/tests/lean/coe4.lean b/tests/lean/coe4.lean
index cec6e6fc49..1b82da9d80 100644
--- a/tests/lean/coe4.lean
+++ b/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
 
diff --git a/tests/lean/coe5.lean b/tests/lean/coe5.lean
index 050b751742..9b63ab79cc 100644
--- a/tests/lean/coe5.lean
+++ b/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
 
diff --git a/tests/lean/run/coe_fn_mvar.lean b/tests/lean/run/coe_fn_mvar.lean
index 5322fdb0ec..d1c7b77b39 100644
--- a/tests/lean/run/coe_fn_mvar.lean
+++ b/tests/lean/run/coe_fn_mvar.lean
@@ -1,6 +1,6 @@
 structure hom (α β : Type*) := (f : α → β)
 
-instance {α β} : has_coe_to_fun (hom α β) := ⟨_, hom.f⟩
+instance {α β} : has_coe_to_fun (hom α β) (λ _, α → β) := ⟨hom.f⟩
 
 def frob {α β} (a : α) : hom β (α × β) := ⟨λ b, (a, b)⟩
 
@@ -15,8 +15,8 @@ structure constantFunction (α β : Type) :=
 (f : α → β)
 (h : ∀ a₁ a₂, f a₁ = f a₂)
 
-instance {α β : Type} : has_coe_to_fun (constantFunction α β) :=
-⟨_, constantFunction.f⟩
+instance {α β : Type} : has_coe_to_fun (constantFunction α β) (λ _, α → β) :=
+⟨constantFunction.f⟩
 
 def myFun {α : Type} : constantFunction α (option α) :=
 { f := fun a, none,
@@ -38,4 +38,4 @@ The single, double, and serif uparrows don't really work in Lean 3.
 #check ⇑myFun 3
 #check ⇑(myFun' _) 3
 #check ⇑(myFun' Nat) 3
--/
\ No newline at end of file
+-/
diff --git a/tests/lean/run/coe_to_fn.lean b/tests/lean/run/coe_to_fn.lean
index 2d5c02cd4e..c79b6e32f3 100644
--- a/tests/lean/run/coe_to_fn.lean
+++ b/tests/lean/run/coe_to_fn.lean
@@ -7,10 +7,7 @@ infix ` ≃ `:50 := equiv
 
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-instance: has_coe_to_fun (α ≃ β) := {
-    F := λ _, α → β,
-    coe := equiv.f,
-}
+instance: has_coe_to_fun (α ≃ β) (λ _, α → β) := ⟨equiv.f⟩
 
 @[symm] def equiv.inv : α ≃ β → β ≃ α
 | ⟨f,g⟩ := ⟨g,f⟩
@@ -23,4 +20,4 @@ def equiv.trans (f : α ≃ β) (g : β ≃ γ) : α ≃ γ :=
 
 example (f : α ≃ β) := function.bijective f
 example (f : α ≃ β) (a : α) := f a
-example (f : (α ≃ β) ≃ (β ≃ α)) (g : α ≃ β) (b : β) := f g b
\ No newline at end of file
+example (f : (α ≃ β) ≃ (β ≃ α)) (g : α ≃ β) (b : β) := f g b
diff --git a/tests/lean/run/coe_to_sort.lean b/tests/lean/run/coe_to_sort.lean
index 7ba9f22749..463f2a3d83 100644
--- a/tests/lean/run/coe_to_sort.lean
+++ b/tests/lean/run/coe_to_sort.lean
@@ -3,8 +3,8 @@ universes u
 structure pointed :=
 (carrier : Type u) (point : carrier)
 
-instance: has_coe_to_sort pointed :=
-⟨_, pointed.carrier⟩
+instance: has_coe_to_sort pointed.{u} (Type u) :=
+⟨pointed.carrier⟩
 
 example (p : pointed) := list p -- coercion works in argument position
-example (p : pointed) : p := p.point
\ No newline at end of file
+example (p : pointed) : p := p.point

From b504d928aec77b9ef8715e5b788b55214171ad6f Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 19:10:18 +0100
Subject: [PATCH 04/16] Change instance naming heuristic.

---
 src/frontends/lean/decl_util.cpp    | 11 ++++++-----
 tests/lean/run/instance_naming.lean |  3 ++-
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index ea78f07085..df0c75e5d1 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -51,14 +51,14 @@ bool 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.
@@ -106,13 +106,14 @@ 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[0];
     while (true) {
         if (is_app(arg_head)) {
             arg_head = app_fn(arg_head);
diff --git a/tests/lean/run/instance_naming.lean b/tests/lean/run/instance_naming.lean
index 3aa67ada44..bc8e113adf 100644
--- a/tests/lean/run/instance_naming.lean
+++ b/tests/lean/run/instance_naming.lean
@@ -54,7 +54,7 @@ structure boo : Type 1 :=
 (β : Type)
 [is_zoo : moo β]
 
-instance : has_coe_to_sort boo := ⟨_, boo.β⟩
+instance : has_coe_to_sort boo _ := ⟨boo.β⟩
 
 namespace boo
 -- Instance naming for variable arguments works (generating `boo.moo`)
@@ -94,3 +94,4 @@ example := lie_algebra.int.lie_algebra
 example := lie_algebra.gl.lie_algebra
 example := zoo.moo
 example := boo.moo
+example := boo.has_coe_to_sort

From f6946556cd9ad3d1bf1434f4047cfeed6891de9e Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 19:17:35 +0100
Subject: [PATCH 05/16] Fix coe pp.

---
 src/frontends/lean/pp.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 9762e048c4..837076af29 100755
--- a/src/frontends/lean/pp.cpp
+++ b/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);

From 44c0d37e636ce946660456bb6b541966c1f3aae7 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 19:25:03 +0100
Subject: [PATCH 06/16] Change instance heuristic some more.

---
 src/frontends/lean/decl_util.cpp | 76 ++++++++++++++++----------------
 1 file changed, 39 insertions(+), 37 deletions(-)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index df0c75e5d1..18eae4c062 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -111,46 +111,48 @@ optional<name> heuristic_inst_name(name const & ns, expr const & type) {
     if (!is_constant(C)) return {};
     name class_name = const_name(C);
 
-    // Look at head symbol of last argument.
-    if (!args.size()) return {};
-    expr arg_head = args[0];
-    while (true) {
-        if (is_app(arg_head)) {
-            arg_head = app_fn(arg_head);
-        } else if (is_typed_expr(arg_head)) {
-            arg_head = get_typed_expr_expr(arg_head);
-        } else if (is_explicit_or_partial_explicit(arg_head)) {
-            arg_head = get_explicit_or_partial_explicit_arg(arg_head);
-        } else if (is_annotation(arg_head)) {
-            arg_head = get_annotation_arg(arg_head);
-        } else {
-            break;
+    name arg_name;
+    // Get last viable argument head name.
+    std::reverse(args.begin(), args.end());
+    for (expr arg_head : args) {
+        if (arg_name) break;
+
+        // Look at head symbol of the argument.
+        while (true) {
+            if (is_app(arg_head)) {
+                arg_head = app_fn(arg_head);
+            } else if (is_typed_expr(arg_head)) {
+                arg_head = get_typed_expr_expr(arg_head);
+            } else if (is_explicit_or_partial_explicit(arg_head)) {
+                arg_head = get_explicit_or_partial_explicit_arg(arg_head);
+            } else if (is_annotation(arg_head)) {
+                arg_head = get_annotation_arg(arg_head);
+            } else {
+                break;
+            }
         }
-    }
 
-    // Generate name for argument.
-    name arg_name;
-    if (is_constant(arg_head)) {
-        arg_name = const_name(arg_head);
-    } else if (is_sort(arg_head) || is_sort_wo_universe(arg_head)) {
-        arg_name = "sort";
-    } else if (is_pi(arg_head)) {
-        arg_name = "pi";
-    } else if (is_field_notation(arg_head)) {
-        expr lhs = macro_arg(arg_head, 0);
-        arg_name = get_field_notation_field_name(arg_head);
-
-        // The field projection does not have the full name.
-        // If we can guess the type of the lhs, prepend it.
-        if (is_local(lhs)) {
-            expr type = get_app_fn(mlocal_type(lhs));
-            if (is_constant(type))
-                arg_name = const_name(type) + arg_name;
+        // Generate name for argument.
+        if (is_constant(arg_head)) {
+            arg_name = const_name(arg_head);
+        } else if (is_sort(arg_head) || is_sort_wo_universe(arg_head)) {
+            arg_name = "sort";
+        } else if (is_pi(arg_head)) {
+            arg_name = "pi";
+        } else if (is_field_notation(arg_head)) {
+            expr lhs = macro_arg(arg_head, 0);
+            arg_name = get_field_notation_field_name(arg_head);
+
+            // The field projection does not have the full name.
+            // If we can guess the type of the lhs, prepend it.
+            if (is_local(lhs)) {
+                expr type = get_app_fn(mlocal_type(lhs));
+                if (is_constant(type))
+                    arg_name = const_name(type) + arg_name;
+            }
+        } else if (is_local(arg_head)) {
+            // only class name
         }
-    } else if (is_local(arg_head)) {
-        // only class name
-    } else {
-        return {};
     }
 
     // Strip namespace prefix of class.

From 6b51a52bb01ffb0cd45b934dfa87a363eb3e341e Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 19:25:33 +0100
Subject: [PATCH 07/16] Fix some tests.

---
 tests/lean/coe4.lean.expected.out | 3 ++-
 tests/lean/coe5.lean.expected.out | 5 ++++-
 tests/lean/coe6.lean              | 4 ++--
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/tests/lean/coe4.lean.expected.out b/tests/lean/coe4.lean.expected.out
index 17b20e9476..33a985d7b5 100644
--- a/tests/lean/coe4.lean.expected.out
+++ b/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
diff --git a/tests/lean/coe5.lean.expected.out b/tests/lean/coe5.lean.expected.out
index 7a5d753f0d..cb60e4eaec 100644
--- a/tests/lean/coe5.lean.expected.out
+++ b/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
diff --git a/tests/lean/coe6.lean b/tests/lean/coe6.lean
index 3aa5bfb174..4408e7b94f 100644
--- a/tests/lean/coe6.lean
+++ b/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

From c711136f8c02febfb8384b81f6129d9997cc4d10 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 19:30:52 +0100
Subject: [PATCH 08/16] Revert "Change instance heuristic some more."

This reverts commit 44c0d37e636ce946660456bb6b541966c1f3aae7.
---
 src/frontends/lean/decl_util.cpp | 76 ++++++++++++++++----------------
 1 file changed, 37 insertions(+), 39 deletions(-)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 18eae4c062..df0c75e5d1 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -111,48 +111,46 @@ optional<name> heuristic_inst_name(name const & ns, expr const & type) {
     if (!is_constant(C)) return {};
     name class_name = const_name(C);
 
-    name arg_name;
-    // Get last viable argument head name.
-    std::reverse(args.begin(), args.end());
-    for (expr arg_head : args) {
-        if (arg_name) break;
-
-        // Look at head symbol of the argument.
-        while (true) {
-            if (is_app(arg_head)) {
-                arg_head = app_fn(arg_head);
-            } else if (is_typed_expr(arg_head)) {
-                arg_head = get_typed_expr_expr(arg_head);
-            } else if (is_explicit_or_partial_explicit(arg_head)) {
-                arg_head = get_explicit_or_partial_explicit_arg(arg_head);
-            } else if (is_annotation(arg_head)) {
-                arg_head = get_annotation_arg(arg_head);
-            } else {
-                break;
-            }
+    // Look at head symbol of last argument.
+    if (!args.size()) return {};
+    expr arg_head = args[0];
+    while (true) {
+        if (is_app(arg_head)) {
+            arg_head = app_fn(arg_head);
+        } else if (is_typed_expr(arg_head)) {
+            arg_head = get_typed_expr_expr(arg_head);
+        } else if (is_explicit_or_partial_explicit(arg_head)) {
+            arg_head = get_explicit_or_partial_explicit_arg(arg_head);
+        } else if (is_annotation(arg_head)) {
+            arg_head = get_annotation_arg(arg_head);
+        } else {
+            break;
         }
+    }
 
-        // Generate name for argument.
-        if (is_constant(arg_head)) {
-            arg_name = const_name(arg_head);
-        } else if (is_sort(arg_head) || is_sort_wo_universe(arg_head)) {
-            arg_name = "sort";
-        } else if (is_pi(arg_head)) {
-            arg_name = "pi";
-        } else if (is_field_notation(arg_head)) {
-            expr lhs = macro_arg(arg_head, 0);
-            arg_name = get_field_notation_field_name(arg_head);
-
-            // The field projection does not have the full name.
-            // If we can guess the type of the lhs, prepend it.
-            if (is_local(lhs)) {
-                expr type = get_app_fn(mlocal_type(lhs));
-                if (is_constant(type))
-                    arg_name = const_name(type) + arg_name;
-            }
-        } else if (is_local(arg_head)) {
-            // only class name
+    // Generate name for argument.
+    name arg_name;
+    if (is_constant(arg_head)) {
+        arg_name = const_name(arg_head);
+    } else if (is_sort(arg_head) || is_sort_wo_universe(arg_head)) {
+        arg_name = "sort";
+    } else if (is_pi(arg_head)) {
+        arg_name = "pi";
+    } else if (is_field_notation(arg_head)) {
+        expr lhs = macro_arg(arg_head, 0);
+        arg_name = get_field_notation_field_name(arg_head);
+
+        // The field projection does not have the full name.
+        // If we can guess the type of the lhs, prepend it.
+        if (is_local(lhs)) {
+            expr type = get_app_fn(mlocal_type(lhs));
+            if (is_constant(type))
+                arg_name = const_name(type) + arg_name;
         }
+    } else if (is_local(arg_head)) {
+        // only class name
+    } else {
+        return {};
     }
 
     // Strip namespace prefix of class.

From 744be0086ae8f9b9b9f5c27d927c711df5ed46fc Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 19:34:34 +0100
Subject: [PATCH 09/16] Fix some tests.

---
 tests/lean/run/algebra_attr.lean     | 4 ++--
 tests/lean/run/tc_inout1.lean        | 2 +-
 tests/lean/run/tc_right_to_left.lean | 6 +++---
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tests/lean/run/algebra_attr.lean b/tests/lean/run/algebra_attr.lean
index a6c7cd01c6..f1d005d3ee 100644
--- a/tests/lean/run/algebra_attr.lean
+++ b/tests/lean/run/algebra_attr.lean
@@ -1,10 +1,10 @@
 def f (a b : nat) := 0
 def g (a b : nat) := 1
 
-instance : is_commutative nat f :=
+instance f.is_commutative : is_commutative nat f :=
 ⟨λ a b, rfl⟩
 
-instance : is_commutative nat g :=
+instance g.is_commutative : is_commutative nat g :=
 ⟨λ a b, rfl⟩
 
 open tactic
diff --git a/tests/lean/run/tc_inout1.lean b/tests/lean/run/tc_inout1.lean
index ef3cb83f54..dab791edd6 100644
--- a/tests/lean/run/tc_inout1.lean
+++ b/tests/lean/run/tc_inout1.lean
@@ -65,7 +65,7 @@ has_mem2.mem
 
 local infix ∈ := mem2
 
-instance (α : Type u) : has_mem2 α (list α) :=
+instance list.has_mem2 (α : Type u) : has_mem2 α (list α) :=
 ⟨list.mem⟩
 
 #check λ a (s : list nat), a ∈ s
diff --git a/tests/lean/run/tc_right_to_left.lean b/tests/lean/run/tc_right_to_left.lean
index e1d3e2c1ff..b5cd16e740 100644
--- a/tests/lean/run/tc_right_to_left.lean
+++ b/tests/lean/run/tc_right_to_left.lean
@@ -4,12 +4,12 @@ class a (α : Type) (x : bool)
 class b (α : Type) (x : bool)
 class c (α : Type)
 
-instance (α) : a α tt := ⟨⟩
-instance (α) : b α tt := ⟨⟩
+instance tt.a (α) : a α tt := ⟨⟩
+instance tt.b (α) : b α tt := ⟨⟩
 instance b.to_c (α x) [a α x] [b α x] : c α := ⟨⟩
 
 -- make all type-class resolution queries for `a α ff` fail
-instance (α) [a α ff] : a α ff := ‹a α ff›
+instance ff.a (α) [a α ff] : a α ff := ‹a α ff›
 
 set_option trace.class_instances true
 example (α) : c α :=

From b8b24262d9a2db483f441f33cc75616ccd9e0473 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 Mar 2021 19:35:09 +0100
Subject: [PATCH 10/16] Fix one more test.

---
 tests/lean/run/sebastien_coe_simp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/sebastien_coe_simp.lean b/tests/lean/run/sebastien_coe_simp.lean
index ff8c24ad43..71ebc36052 100644
--- a/tests/lean/run/sebastien_coe_simp.lean
+++ b/tests/lean/run/sebastien_coe_simp.lean
@@ -3,7 +3,7 @@ variable (α : Type*)
 structure my_equiv :=
 (to_fun : α → α)
 
-instance : has_coe_to_fun (my_equiv α) := ⟨_, my_equiv.to_fun⟩
+instance : has_coe_to_fun (my_equiv α) _ := ⟨my_equiv.to_fun⟩
 
 def my_equiv1 : my_equiv α :=
 { to_fun := id }

From 65429846a070ed71590dd79b8df49e4937f89dea Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 19 Mar 2021 14:59:58 +0100
Subject: [PATCH 11/16] Tweak instance naming.

---
 src/frontends/lean/decl_util.cpp    | 6 +++++-
 src/library/constants.cpp           | 8 ++++++++
 src/library/constants.h             | 2 ++
 src/library/constants.txt           | 2 ++
 tests/lean/run/check_constants.lean | 2 ++
 5 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index df0c75e5d1..1cdbe31e8a 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/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"
@@ -113,7 +114,10 @@ optional<name> heuristic_inst_name(name const & ns, expr const & type) {
 
     // Look at head symbol of last argument.
     if (!args.size()) return {};
-    expr arg_head = args[0];
+    expr arg_head = args.back();
+    if (class_name == get_has_coe_to_fun_name() || class_name == get_has_coe_to_sort_name()) {
+        arg_head = args[0];
+    }
     while (true) {
         if (is_app(arg_head)) {
             arg_head = app_fn(arg_head);
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 51c142f3b9..82430027c4 100644
--- a/src/library/constants.cpp
+++ b/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; }
diff --git a/src/library/constants.h b/src/library/constants.h
index a5037a77a1..c3e1f9acb2 100644
--- a/src/library/constants.h
+++ b/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();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index ac0051abeb..61cd0d5232 100644
--- a/src/library/constants.txt
+++ b/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
diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean
index 3b55e55aed..6ad987cd04 100644
--- a/tests/lean/run/check_constants.lean
+++ b/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

From d2f2df87c1f48deddd3467adc743194f5207d0e5 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 19 Mar 2021 15:04:57 +0100
Subject: [PATCH 12/16] Fix tests.

---
 tests/lean/run/coe_univ_bug.lean             |  6 +++---
 tests/lean/run/dep_coe_to_fn.lean            |  5 ++---
 tests/lean/run/dep_coe_to_fn2.lean           |  5 ++---
 tests/lean/run/dep_coe_to_fn3.lean           |  5 ++---
 tests/lean/run/let_coe_sort.lean             |  4 ++--
 tests/lean/run/pred_to_subtype_coercion.lean |  4 ++--
 tests/lean/run/simp_coe.lean                 | 19 -------------------
 tests/lean/run/u_eq_max_u_v.lean             |  5 ++---
 8 files changed, 15 insertions(+), 38 deletions(-)
 delete mode 100644 tests/lean/run/simp_coe.lean

diff --git a/tests/lean/run/coe_univ_bug.lean b/tests/lean/run/coe_univ_bug.lean
index a9aa825c5e..bd2a219d40 100644
--- a/tests/lean/run/coe_univ_bug.lean
+++ b/tests/lean/run/coe_univ_bug.lean
@@ -8,10 +8,10 @@ v + 1
 
 universe variable u
 
-instance pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
-⟨Type u, (λ p : A → Prop, subtype p)⟩
+instance pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) _ :=
+⟨(λ p : A → Prop, subtype p)⟩
 
-instance coesubtype {A : Type u} {p : A → Prop} : has_coe (@coe_sort _ pred2subtype p) A :=
+instance coesubtype {A : Type u} {p : A → Prop} : has_coe (@coe_sort _ _ pred2subtype p) A :=
 ⟨λ s, subtype.val s⟩
 
 def g {n : nat} (v : below n) : nat :=
diff --git a/tests/lean/run/dep_coe_to_fn.lean b/tests/lean/run/dep_coe_to_fn.lean
index 95a69eaa36..94cb44820f 100644
--- a/tests/lean/run/dep_coe_to_fn.lean
+++ b/tests/lean/run/dep_coe_to_fn.lean
@@ -3,9 +3,8 @@ universe variables u v
 structure Func :=
 (A : Type u) (B : Type v) (fn : A → B → A)
 
-instance F_to_fn : has_coe_to_fun Func :=
-{ F   := λ f, f^.A → f^.B → f^.A,
-  coe := λ f, f^.fn }
+instance F_to_fn : has_coe_to_fun Func _ :=
+{ coe := λ f, f^.fn }
 
 variables (f : Func) (a : f^.A) (b : f^.B)
 #check (f a b)
diff --git a/tests/lean/run/dep_coe_to_fn2.lean b/tests/lean/run/dep_coe_to_fn2.lean
index 8de9de391b..10f4c35434 100644
--- a/tests/lean/run/dep_coe_to_fn2.lean
+++ b/tests/lean/run/dep_coe_to_fn2.lean
@@ -3,9 +3,8 @@ universe variables u v
 structure Func :=
 (A : Type u) (B : A → Type v) (fn : Π a, B a → B a)
 
-instance F_to_fn : has_coe_to_fun Func :=
-{ F   := λ f, Π a, f^.B a → f^.B a,
-  coe := λ f, f^.fn }
+instance F_to_fn : has_coe_to_fun Func _ :=
+{ coe := λ f, f^.fn }
 
 variables (f : Func) (a : f^.A) (b : f^.B a)
 #check (f a b)
diff --git a/tests/lean/run/dep_coe_to_fn3.lean b/tests/lean/run/dep_coe_to_fn3.lean
index 46c39be0e3..279b752a1c 100644
--- a/tests/lean/run/dep_coe_to_fn3.lean
+++ b/tests/lean/run/dep_coe_to_fn3.lean
@@ -3,9 +3,8 @@ universe variables u v
 structure Func :=
 (A : Type u) (B : A → Type v) (fn : Π a, B a → B a)
 
-instance F_to_fn : has_coe_to_fun Func :=
-{ F   := λ f, Π a, f^.B a → f^.B a,
-  coe := λ f a b, f^.fn a (f^.fn a b) }
+instance F_to_fn : has_coe_to_fun Func _:=
+{ coe := λ f a b, f^.fn a (f^.fn a b) }
 
 variables (f : Func) (a : f^.A) (b : f^.B a)
 #check (f a b)
diff --git a/tests/lean/run/let_coe_sort.lean b/tests/lean/run/let_coe_sort.lean
index 9e2fa3593d..072a6c4356 100644
--- a/tests/lean/run/let_coe_sort.lean
+++ b/tests/lean/run/let_coe_sort.lean
@@ -1,7 +1,7 @@
 inductive foo | bar
 
-instance : has_coe_to_sort foo :=
-⟨Type, λ _, unit⟩
+instance : has_coe_to_sort foo _ :=
+⟨λ _, unit⟩
 
 set_option pp.all true
 
diff --git a/tests/lean/run/pred_to_subtype_coercion.lean b/tests/lean/run/pred_to_subtype_coercion.lean
index 6d58bc18a5..b46e2d8bf8 100644
--- a/tests/lean/run/pred_to_subtype_coercion.lean
+++ b/tests/lean/run/pred_to_subtype_coercion.lean
@@ -1,8 +1,8 @@
 universe variables u
 
 attribute [instance]
-definition pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
-⟨Type u, λ p : A → Prop, subtype p⟩
+definition pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) _ :=
+⟨λ p : A → Prop, subtype p⟩
 
 definition below (n : nat) : nat → Prop :=
 λ i, i < n
diff --git a/tests/lean/run/simp_coe.lean b/tests/lean/run/simp_coe.lean
deleted file mode 100644
index b1f1326680..0000000000
--- a/tests/lean/run/simp_coe.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-example (p : Prop) (h : p) : tt → p :=
-begin
-  simp [true_implies_iff], assumption
-end
-
-local attribute [semireducible] coe_sort_bool
-
-example (p : Prop) (h : p) : tt → p :=
-begin
-  fail_if_success {simp},
-  intro, assumption
-end
-
-local attribute [reducible] coe_sort_bool
-
-example (p : Prop) (h : p) : tt → p :=
-begin
-  simp [true_implies_iff], assumption
-end
diff --git a/tests/lean/run/u_eq_max_u_v.lean b/tests/lean/run/u_eq_max_u_v.lean
index 35395e1b73..b2e2af918d 100644
--- a/tests/lean/run/u_eq_max_u_v.lean
+++ b/tests/lean/run/u_eq_max_u_v.lean
@@ -15,9 +15,8 @@ structure semigroup_morphism { α β : Type u } ( s : semigroup α ) ( t: semigr
 
 attribute [simp] semigroup_morphism.multiplicative
 
-@[reducible] instance semigroup_morphism_to_map { α β : Type u } { s : semigroup α } { t: semigroup β } : has_coe_to_fun (semigroup_morphism s t) :=
-{ F   := λ f, Π x : α, β,
-  coe := semigroup_morphism.map }
+@[reducible] instance semigroup_morphism_to_map { α β : Type u } { s : semigroup α } { t: semigroup β } : has_coe_to_fun (semigroup_morphism s t) _ :=
+{ coe := semigroup_morphism.map }
 
 @[reducible] definition semigroup_identity { α : Type u } ( s: semigroup α ) : semigroup_morphism s s := ⟨ id, ♮ ⟩
 

From da53b38807eb1217e0b7b2f559834b8adc7d045b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 19 Mar 2021 15:10:08 +0100
Subject: [PATCH 13/16] Remove unnecessary instance names.

---
 library/init/meta/expr.lean                    | 2 +-
 library/init/meta/widget/basic.lean            | 2 +-
 library/init/meta/widget/tactic_component.lean | 2 +-
 tests/lean/123-2.lean                          | 4 ++--
 tests/lean/run/algebra_attr.lean               | 4 ++--
 tests/lean/run/tc_inout1.lean                  | 2 +-
 tests/lean/run/tc_right_to_left.lean           | 6 +++---
 7 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index bd718cb8cb..df95fde8b5 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -146,7 +146,7 @@ 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 expr.has_coe_to_fun : has_coe_to_fun (expr elab) (λ e, expr elab → expr elab) :=
+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.
diff --git a/library/init/meta/widget/basic.lean b/library/init/meta/widget/basic.lean
index 370dd295ca..6c6ccec04d 100644
--- a/library/init/meta/widget/basic.lean
+++ b/library/init/meta/widget/basic.lean
@@ -253,7 +253,7 @@ meta def ignore_props : component unit α → component π α
 meta instance : has_coe (component π empty) (component π α) :=
 ⟨component.filter_map_action (λ p x, none)⟩
 
-meta instance component.has_coe_to_fun : has_coe_to_fun (component π α) (λ c, π → html α) :=
+meta instance : has_coe_to_fun (component π α) (λ c, π → html α) :=
 ⟨λ c p, html.of_component p c⟩
 
 meta def stateful {π α : Type}
diff --git a/library/init/meta/widget/tactic_component.lean b/library/init/meta/widget/tactic_component.lean
index 2bf6d13cc4..0e667311bd 100644
--- a/library/init/meta/widget/tactic_component.lean
+++ b/library/init/meta/widget/tactic_component.lean
@@ -80,7 +80,7 @@ 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
 
diff --git a/tests/lean/123-2.lean b/tests/lean/123-2.lean
index 609ccbf1c4..190e28b209 100644
--- a/tests/lean/123-2.lean
+++ b/tests/lean/123-2.lean
@@ -17,7 +17,7 @@ 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 ring_hom'.has_coe_to_fun (α : Type*) (β : Type*) [semiring α] [semiring β] :
+instance (α : Type*) (β : Type*) [semiring α] [semiring β] :
   has_coe_to_fun (ring_hom' α β) (λ _, α → β) :=
 ⟨λ f, ring_hom'.to_fun (f)⟩
 
@@ -37,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 alg_hom'.has_coe_to_fun : has_coe_to_fun (alg_hom' R A B) (λ _, 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]
diff --git a/tests/lean/run/algebra_attr.lean b/tests/lean/run/algebra_attr.lean
index f1d005d3ee..a6c7cd01c6 100644
--- a/tests/lean/run/algebra_attr.lean
+++ b/tests/lean/run/algebra_attr.lean
@@ -1,10 +1,10 @@
 def f (a b : nat) := 0
 def g (a b : nat) := 1
 
-instance f.is_commutative : is_commutative nat f :=
+instance : is_commutative nat f :=
 ⟨λ a b, rfl⟩
 
-instance g.is_commutative : is_commutative nat g :=
+instance : is_commutative nat g :=
 ⟨λ a b, rfl⟩
 
 open tactic
diff --git a/tests/lean/run/tc_inout1.lean b/tests/lean/run/tc_inout1.lean
index dab791edd6..ef3cb83f54 100644
--- a/tests/lean/run/tc_inout1.lean
+++ b/tests/lean/run/tc_inout1.lean
@@ -65,7 +65,7 @@ has_mem2.mem
 
 local infix ∈ := mem2
 
-instance list.has_mem2 (α : Type u) : has_mem2 α (list α) :=
+instance (α : Type u) : has_mem2 α (list α) :=
 ⟨list.mem⟩
 
 #check λ a (s : list nat), a ∈ s
diff --git a/tests/lean/run/tc_right_to_left.lean b/tests/lean/run/tc_right_to_left.lean
index b5cd16e740..e1d3e2c1ff 100644
--- a/tests/lean/run/tc_right_to_left.lean
+++ b/tests/lean/run/tc_right_to_left.lean
@@ -4,12 +4,12 @@ class a (α : Type) (x : bool)
 class b (α : Type) (x : bool)
 class c (α : Type)
 
-instance tt.a (α) : a α tt := ⟨⟩
-instance tt.b (α) : b α tt := ⟨⟩
+instance (α) : a α tt := ⟨⟩
+instance (α) : b α tt := ⟨⟩
 instance b.to_c (α x) [a α x] [b α x] : c α := ⟨⟩
 
 -- make all type-class resolution queries for `a α ff` fail
-instance ff.a (α) [a α ff] : a α ff := ‹a α ff›
+instance (α) [a α ff] : a α ff := ‹a α ff›
 
 set_option trace.class_instances true
 example (α) : c α :=

From deb09469aebac1d79beb05d75df54586b24fa6f8 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 19 Mar 2021 19:05:08 +0100
Subject: [PATCH 14/16] Add todo.

---
 src/frontends/lean/decl_util.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 1cdbe31e8a..51ea1a01cb 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -116,6 +116,7 @@ optional<name> heuristic_inst_name(name const & ns, expr const & type) {
     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) {

From f116eaf542a1c009fec4d581f27efbef1a64023e Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 26 Mar 2021 09:58:15 +0100
Subject: [PATCH 15/16] Synthesize tc insts before anon cstrs.

---
 src/frontends/lean/elaborator.cpp     | 4 ++++
 tests/lean/run/yury_coe_sort_bug.lean | 5 +++++
 2 files changed, 9 insertions(+)
 create mode 100644 tests/lean/run/yury_coe_sort_bug.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 6256edbf88..e8db39464d 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -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") +
diff --git a/tests/lean/run/yury_coe_sort_bug.lean b/tests/lean/run/yury_coe_sort_bug.lean
new file mode 100644
index 0000000000..7d106c6a7f
--- /dev/null
+++ b/tests/lean/run/yury_coe_sort_bug.lean
@@ -0,0 +1,5 @@
+universe u
+
+instance {α : Type u} : has_coe_to_sort (set α) (Type u) := ⟨λ s, {x // x ∈ s}⟩
+
+example : ↥({0} : set ℕ) := ⟨0, rfl⟩
\ No newline at end of file

From dcc44269840b19af2a5dab1312f43b7b65f4b5a7 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 11 Sep 2021 22:44:19 -0400
Subject: [PATCH 16/16] Fix conflict with mathlib

---
 library/init/algebra/order.lean         | 4 ++--
 library/init/meta/relation_tactics.lean | 2 --
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean
index 787a89ffe4..dbd8fe1a32 100644
--- a/library/init/algebra/order.lean
+++ b/library/init/algebra/order.lean
@@ -204,9 +204,9 @@ class linear_order (α : Type u) extends partial_order α :=
 (decidable_lt : decidable_rel ((<) : α → α → Prop) :=
     @decidable_lt_of_decidable_le _ _ decidable_le)
 (max : α → α → α := @max_default α _ _)
-(max_def : max = @max_default α _ decidable_le . tactic.reflexivity')
+(max_def : max = @max_default α _ decidable_le . tactic.interactive.reflexivity)
 (min : α → α → α := @min_default α _ _)
-(min_def : min = @min_default α _ decidable_le . tactic.reflexivity')
+(min_def : min = @min_default α _ decidable_le . tactic.interactive.reflexivity)
 
 variables [linear_order α]
 
diff --git a/library/init/meta/relation_tactics.lean b/library/init/meta/relation_tactics.lean
index 05e3e959ce..8aa5e37604 100644
--- a/library/init/meta/relation_tactics.lean
+++ b/library/init/meta/relation_tactics.lean
@@ -21,8 +21,6 @@ do tgt   ← target >>= instantiate_mvars,
 meta def reflexivity (md := semireducible) : tactic unit :=
 relation_tactic md environment.refl_for "reflexivity"
 
-meta def reflexivity' : tactic unit := reflexivity
-
 meta def symmetry (md := semireducible) : tactic unit :=
 relation_tactic md environment.symm_for "symmetry"