diff --git a/library/init/coe.lean b/library/init/coe.lean
index e047928ba6..511fcd02b9 100644
--- a/library/init/coe.lean
+++ b/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,7 +66,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 -/
@@ -72,10 +75,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 -/
@@ -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
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index fde77fd0a4..85f7b3aa6c 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 : 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..6c6ccec04d 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 : 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..0e667311bd 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 : 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/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index db4e994c00..1ab602070b 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"
@@ -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);
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index f7cf8850c2..1cac978b7f 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);
@@ -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/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);
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/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..190e28b209 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 (α : 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]
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/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 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/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
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
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
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/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
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/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 }
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, ♮ ⟩
 
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