From 9bedbbb739514dce617689c8d1e6094bbefd1aa9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Nov 2015 11:32:05 -0800
Subject: [PATCH] refactor(library,hott): remove coercions between algebraic
 structures

They are classes, and mixing coercion with type class resolution is a
recipe for disaster (aka counterintuitive behavior).
---
 hott/algebra/category/category.hlean   |  8 +++++-
 hott/algebra/category/groupoid.hlean   |  2 +-
 hott/algebra/category/strict.hlean     |  2 +-
 hott/algebra/field.hlean               |  2 +-
 hott/algebra/group.hlean               | 16 +++++------
 hott/algebra/hott.hlean                |  8 ++++++
 hott/algebra/order.hlean               |  6 ++--
 hott/algebra/ordered_group.hlean       |  8 +++---
 hott/algebra/ordered_ring.hlean        | 34 +++++++++++------------
 hott/algebra/ring.hlean                |  4 +--
 library/algebra/field.lean             |  2 +-
 library/algebra/group.lean             | 16 +++++------
 library/algebra/group_bigops.lean      |  2 +-
 library/algebra/order.lean             |  6 ++--
 library/algebra/ordered_field.lean     |  2 +-
 library/algebra/ordered_group.lean     | 19 +++++++------
 library/algebra/ordered_ring.lean      | 38 +++++++++++++-------------
 library/algebra/ring.lean              |  4 +--
 library/data/list/sort.lean            |  4 +--
 library/theories/group_theory/hom.lean |  2 +-
 src/frontends/lean/structure_cmd.cpp   |  3 +-
 tests/lean/run/group5.lean             |  4 ---
 22 files changed, 102 insertions(+), 90 deletions(-)

diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean
index 2db10a3454..e07f82ab02 100644
--- a/hott/algebra/category/category.hlean
+++ b/hott/algebra/category/category.hlean
@@ -28,6 +28,12 @@ namespace category
   structure category [class] (ob : Type) extends parent : precategory ob :=
   mk' :: (iso_of_path_equiv : is_univalent parent)
 
+  -- Remark: category and precategory are classes. So, the structure command
+  -- does not create a coercion between them automatically.
+  -- This coercion is needed for definitions such as category_eq_of_equiv
+  -- without it, we would have to explicitly use category.to_precategory
+  attribute category.to_precategory [coercion]
+
   attribute category [multiple_instances]
 
   abbreviation iso_of_path_equiv := @category.iso_of_path_equiv
@@ -81,7 +87,7 @@ namespace category
 
   definition Category.to_Precategory [constructor] [coercion] [reducible] (C : Category)
     : Precategory :=
-  Precategory.mk (Category.carrier C) C
+  Precategory.mk (Category.carrier C) _
 
   definition category.Mk [constructor] [reducible] := Category.mk
   definition category.MK [constructor] [reducible] (C : Precategory)
diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean
index 7e5fcc47ce..50b3ff5c13 100644
--- a/hott/algebra/category/groupoid.hlean
+++ b/hott/algebra/category/groupoid.hlean
@@ -65,7 +65,7 @@ namespace category
   attribute Groupoid.struct [instance] [coercion]
 
   definition Groupoid.to_Precategory [coercion] [reducible] (C : Groupoid) : Precategory :=
-  Precategory.mk (Groupoid.carrier C) C
+  Precategory.mk (Groupoid.carrier C) _
 
   definition groupoid.Mk [reducible] := Groupoid.mk
   definition groupoid.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f)
diff --git a/hott/algebra/category/strict.hlean b/hott/algebra/category/strict.hlean
index 85ef9d12c5..a39a413cad 100644
--- a/hott/algebra/category/strict.hlean
+++ b/hott/algebra/category/strict.hlean
@@ -26,7 +26,7 @@ namespace category
 
   definition Strict_precategory.to_Precategory [coercion] [reducible]
     (C : Strict_precategory) : Precategory :=
-  Precategory.mk (Strict_precategory.carrier C) C
+  Precategory.mk (Strict_precategory.carrier C) _
 
   open functor
 
diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean
index 6bb21b7448..e0f71e61b3 100644
--- a/hott/algebra/field.hlean
+++ b/hott/algebra/field.hlean
@@ -328,7 +328,7 @@ section discrete_field
     (assume H1 : x ≠ 0,
       sum.inr (by rewrite [-one_mul, -(inv_mul_cancel H1), mul.assoc, H, mul_zero]))
 
-  definition discrete_field.to_integral_domain [instance] [reducible] [coercion] :
+  definition discrete_field.to_integral_domain [instance] [reducible] :
     integral_domain A :=
   ⦃ integral_domain, s,
     eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄
diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index fb89364065..a438f845ca 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -53,10 +53,10 @@ theorem mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
 !comm_semigroup.mul_comm
 
 theorem mul.left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
-binary.left_comm (@mul.comm A s) (@mul.assoc A s) a b c
+binary.left_comm (@mul.comm A _) (@mul.assoc A _) a b c
 
 theorem mul.right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b :=
-binary.right_comm (@mul.comm A s) (@mul.assoc A s) a b c
+binary.right_comm (@mul.comm A _) (@mul.assoc A _) a b c
 
 structure left_cancel_semigroup [class] (A : Type) extends semigroup A :=
 (mul_left_cancel : ∀a b c, mul a b = mul a c → b = c)
@@ -95,10 +95,10 @@ theorem add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
 
 theorem add.left_comm [s : add_comm_semigroup A] (a b c : A) :
   a + (b + c) = b + (a + c) :=
-binary.left_comm (@add.comm A s) (@add.assoc A s) a b c
+binary.left_comm (@add.comm A _) (@add.assoc A _) a b c
 
 theorem add.right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
-binary.right_comm (@add.comm A s) (@add.assoc A s) a b c
+binary.right_comm (@add.comm A _) (@add.assoc A _) a b c
 
 structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_left_cancel : ∀a b c, add a b = add a c → b = c)
@@ -248,11 +248,11 @@ section group
   theorem mul_right_cancel {a b c : A} (H : a * b = c * b) : a = c :=
   by rewrite [-mul_inv_cancel_right a b, H, mul_inv_cancel_right]
 
-  definition group.to_left_cancel_semigroup [instance] [coercion] [reducible] : left_cancel_semigroup A :=
+  definition group.to_left_cancel_semigroup [instance] [reducible] : left_cancel_semigroup A :=
   ⦃ left_cancel_semigroup, s,
     mul_left_cancel := @mul_left_cancel A s ⦄
 
-  definition group.to_right_cancel_semigroup [instance] [coercion] [reducible] : right_cancel_semigroup A :=
+  definition group.to_right_cancel_semigroup [instance] [reducible] : right_cancel_semigroup A :=
   ⦃ right_cancel_semigroup, s,
     mul_right_cancel := @mul_right_cancel A s ⦄
 
@@ -363,12 +363,12 @@ section add_group
      ... = (c + b) + -b : H
      ... = c : add_neg_cancel_right
 
-  definition add_group.to_left_cancel_semigroup [instance] [coercion] [reducible] :
+  definition add_group.to_left_cancel_semigroup [instance] [reducible] :
     add_left_cancel_semigroup A :=
   ⦃ add_left_cancel_semigroup, s,
     add_left_cancel := @add_left_cancel A s ⦄
 
-  definition add_group.to_add_right_cancel_semigroup [instance] [coercion] [reducible] :
+  definition add_group.to_add_right_cancel_semigroup [instance][reducible] :
     add_right_cancel_semigroup A :=
   ⦃ add_right_cancel_semigroup, s,
     add_right_cancel := @add_right_cancel A s ⦄
diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean
index d478155b15..4e4593c363 100644
--- a/hott/algebra/hott.hlean
+++ b/hott/algebra/hott.hlean
@@ -13,6 +13,14 @@ open equiv eq equiv.ops is_trunc
 namespace algebra
   open Group has_mul has_inv
   -- we prove under which conditions two groups are equal
+
+  -- group and has_mul are classes. So, lean does not automatically generate
+  -- coercions between them anymore.
+  -- So, an application such as (@mul A G g h) in the following definition
+  -- is type incorrect if the coercion is not added (explicitly or implicitly).
+  local attribute group.to.has_mul [coercion]
+  local attribute group.to_has_inv [coercion]
+
   universe variable l
   variables {A B : Type.{l}}
   definition group_eq {G H : group A} (same_mul' : Π(g h : A), @mul A G g h = @mul A H g h)
diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean
index 1f4dd97ea4..a4208e38c3 100644
--- a/hott/algebra/order.hlean
+++ b/hott/algebra/order.hlean
@@ -142,7 +142,7 @@ section
       ne_ab eq_ab,
   show a < c, from lt_of_le_of_ne le_ac ne_ac
 
-  definition order_pair.to_strict_order [instance] [coercion] [reducible] : strict_order A :=
+  definition order_pair.to_strict_order [instance] [reducible] : strict_order A :=
   ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
 
   definition lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c :=
@@ -228,7 +228,7 @@ iff.intro
       iff.mp !strict_order_with_le.le_iff_lt_or_eq (pr1 H),
     show a < b, from sum_resolve_left H1 (pr2 H))
 
-definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] :
+definition strict_order_with_le.to_order_pair [instance] [reducible] [s : strict_order_with_le A] :
   strong_order_pair A :=
 ⦃ strong_order_pair, s,
   le_refl          := le_refl s,
@@ -263,7 +263,7 @@ section
     (assume H, H1 H)
     (assume H, sum.rec_on H (assume H', H2 H') (assume H', H3 H'))
 
-  definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible]
+  definition linear_strong_order_pair.to_linear_order_pair [instance] [reducible]
      : linear_order_pair A :=
   ⦃ linear_order_pair, s ⦄
 
diff --git a/hott/algebra/ordered_group.hlean b/hott/algebra/ordered_group.hlean
index 696cca23a3..a3ae47907d 100644
--- a/hott/algebra/ordered_group.hlean
+++ b/hott/algebra/ordered_group.hlean
@@ -213,12 +213,12 @@ definition ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {
 assert H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
 by rewrite *neg_add_cancel_left at H'; exact H'
 
-definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible]
+definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [reducible]
     [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
 ⦃ ordered_cancel_comm_monoid, s,
-  add_left_cancel       := @add.left_cancel A s,
-  add_right_cancel      := @add.right_cancel A s,
-  le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A s ⦄
+  add_left_cancel       := @add.left_cancel A _,
+  add_right_cancel      := @add.right_cancel A _,
+  le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A _ ⦄
 
 section
   variables [s : ordered_comm_group A] (a b c d e : A)
diff --git a/hott/algebra/ordered_ring.hlean b/hott/algebra/ordered_ring.hlean
index a29b62143e..a6a2f2683d 100644
--- a/hott/algebra/ordered_ring.hlean
+++ b/hott/algebra/ordered_ring.hlean
@@ -188,18 +188,18 @@ begin
   exact (iff.mp !sub_pos_iff_lt H2)
 end
 
-definition ordered_ring.to_ordered_semiring [instance] [coercion] [reducible] [s : ordered_ring A] :
+definition ordered_ring.to_ordered_semiring [instance] [reducible] [s : ordered_ring A] :
   ordered_semiring A :=
 ⦃ ordered_semiring, s,
   mul_zero                   := mul_zero,
   zero_mul                   := zero_mul,
-  add_left_cancel            := @add.left_cancel A s,
-  add_right_cancel           := @add.right_cancel A s,
-  le_of_add_le_add_left      := @le_of_add_le_add_left A s,
-  mul_le_mul_of_nonneg_left  := @ordered_ring.mul_le_mul_of_nonneg_left A s,
-  mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right A s,
-  mul_lt_mul_of_pos_left     := @ordered_ring.mul_lt_mul_of_pos_left A s,
-  mul_lt_mul_of_pos_right    := @ordered_ring.mul_lt_mul_of_pos_right A s ⦄
+  add_left_cancel            := @add.left_cancel A _,
+  add_right_cancel           := @add.right_cancel A _,
+  le_of_add_le_add_left      := @le_of_add_le_add_left A _,
+  mul_le_mul_of_nonneg_left  := @ordered_ring.mul_le_mul_of_nonneg_left A _,
+  mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right A _,
+  mul_lt_mul_of_pos_left     := @ordered_ring.mul_lt_mul_of_pos_left A _,
+  mul_lt_mul_of_pos_right    := @ordered_ring.mul_lt_mul_of_pos_right A _ ⦄
 
 section
   variable [s : ordered_ring A]
@@ -268,19 +268,19 @@ structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_
 
 -- print fields linear_ordered_semiring
 
-definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] [reducible]
+definition linear_ordered_ring.to_linear_ordered_semiring [instance] [reducible]
     [s : linear_ordered_ring A] :
   linear_ordered_semiring A :=
 ⦃ linear_ordered_semiring, s,
   mul_zero                   := mul_zero,
   zero_mul                   := zero_mul,
-  add_left_cancel            := @add.left_cancel A s,
-  add_right_cancel           := @add.right_cancel A s,
-  le_of_add_le_add_left      := @le_of_add_le_add_left A s,
-  mul_le_mul_of_nonneg_left  := @mul_le_mul_of_nonneg_left A s,
-  mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A s,
-  mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left A s,
-  mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right A s,
+  add_left_cancel            := @add.left_cancel A _,
+  add_right_cancel           := @add.right_cancel A _,
+  le_of_add_le_add_left      := @le_of_add_le_add_left A _,
+  mul_le_mul_of_nonneg_left  := @mul_le_mul_of_nonneg_left A _,
+  mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A _,
+  mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left A _,
+  mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right A _,
   le_total                   := linear_ordered_ring.le_total ⦄
 
 structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A
@@ -321,7 +321,7 @@ lt.by_cases
         end))
 
 -- Linearity implies no zero divisors. Doesn't need commutativity.
-definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] [reducible]
+definition linear_ordered_comm_ring.to_integral_domain [instance] [reducible]
     [s: linear_ordered_comm_ring A] : integral_domain A :=
 ⦃ integral_domain, s,
   eq_zero_or_eq_zero_of_mul_eq_zero :=
diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean
index ee693069e5..353a217192 100644
--- a/hott/algebra/ring.hlean
+++ b/hott/algebra/ring.hlean
@@ -163,7 +163,7 @@ have H : 0 * a + 0 = 0 * a + 0 * a, from calc
         ... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib,
 show 0 * a = 0, from  (add.left_cancel H)⁻¹
 
-definition ring.to_semiring [instance] [coercion] [reducible] [s : ring A] : semiring A :=
+definition ring.to_semiring [instance] [reducible] [s : ring A] : semiring A :=
 ⦃ semiring, s,
   mul_zero := ring.mul_zero,
   zero_mul := ring.zero_mul ⦄
@@ -242,7 +242,7 @@ end
 
 structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
 
-definition comm_ring.to_comm_semiring [instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A :=
+definition comm_ring.to_comm_semiring [instance] [reducible] [s : comm_ring A] : comm_semiring A :=
 ⦃ comm_semiring, s,
   mul_zero := mul_zero,
   zero_mul := zero_mul ⦄
diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index 69729d157f..b2c9cc1687 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -328,7 +328,7 @@ section discrete_field
     (suppose x ≠ 0,
       or.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
 
-  definition discrete_field.to_integral_domain [trans_instance] [reducible] [coercion] :
+  definition discrete_field.to_integral_domain [trans_instance] [reducible] :
     integral_domain A :=
   ⦃ integral_domain, s,
     eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index c0f7bc5f66..4beec39038 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -31,10 +31,10 @@ theorem mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
 !comm_semigroup.mul_comm
 
 theorem mul.left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
-binary.left_comm (@mul.comm A s) (@mul.assoc A s) a b c
+binary.left_comm (@mul.comm A _) (@mul.assoc A _) a b c
 
 theorem mul.right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b :=
-binary.right_comm (@mul.comm A s) (@mul.assoc A s) a b c
+binary.right_comm (@mul.comm A _) (@mul.assoc A _) a b c
 
 structure left_cancel_semigroup [class] (A : Type) extends semigroup A :=
 (mul_left_cancel : ∀a b c, mul a b = mul a c → b = c)
@@ -70,10 +70,10 @@ theorem add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
 
 theorem add.left_comm [s : add_comm_semigroup A] (a b c : A) :
   a + (b + c) = b + (a + c) :=
-binary.left_comm (@add.comm A s) (@add.assoc A s) a b c
+binary.left_comm (@add.comm A _) (@add.assoc A _) a b c
 
 theorem add.right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
-binary.right_comm (@add.comm A s) (@add.assoc A s) a b c
+binary.right_comm (@add.comm A _) (@add.assoc A _) a b c
 
 structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_left_cancel : ∀a b c, add a b = add a c → b = c)
@@ -309,12 +309,12 @@ section group
       ... = x ∘c b : Py
       ... = a : Px)
 
-  definition group.to_left_cancel_semigroup [trans_instance] [coercion] [reducible] :
+  definition group.to_left_cancel_semigroup [trans_instance] [reducible] :
     left_cancel_semigroup A :=
   ⦃ left_cancel_semigroup, s,
     mul_left_cancel := @mul_left_cancel A s ⦄
 
-  definition group.to_right_cancel_semigroup [trans_instance] [coercion] [reducible] :
+  definition group.to_right_cancel_semigroup [trans_instance] [reducible] :
     right_cancel_semigroup A :=
   ⦃ right_cancel_semigroup, s,
     mul_right_cancel := @mul_right_cancel A s ⦄
@@ -437,12 +437,12 @@ section add_group
      ... = (c + b) + -b : H
      ... = c : add_neg_cancel_right
 
-  definition add_group.to_left_cancel_semigroup [trans_instance] [coercion] [reducible] :
+  definition add_group.to_left_cancel_semigroup [trans_instance] [reducible] :
     add_left_cancel_semigroup A :=
   ⦃ add_left_cancel_semigroup, s,
     add_left_cancel := @add_left_cancel A s ⦄
 
-  definition add_group.to_add_right_cancel_semigroup [trans_instance] [coercion] [reducible] :
+  definition add_group.to_add_right_cancel_semigroup [trans_instance] [reducible] :
     add_right_cancel_semigroup A :=
   ⦃ add_right_cancel_semigroup, s,
     add_right_cancel := @add_right_cancel A s ⦄
diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean
index 7303917b63..41f0222359 100644
--- a/library/algebra/group_bigops.lean
+++ b/library/algebra/group_bigops.lean
@@ -107,7 +107,7 @@ namespace finset
   include cmB
 
   theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) :=
-  right_commutative_compose_right (@has_mul.mul B cmB) f (@mul.right_comm B cmB)
+  right_commutative_compose_right (@has_mul.mul B _) f (@mul.right_comm B _)
 
   theorem Prodl_eq_Prodl_of_perm (f : A → B) {l₁ l₂ : list A} :
     perm l₁ l₂ → Prodl l₁ f = Prodl l₂ f :=
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 2804d9bc8f..d5bd3b91ee 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -111,7 +111,7 @@ section
   private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
     lt_of_lt_of_le lt_ab (le_of_lt lt_bc)
 
-  definition order_pair.to_strict_order [trans_instance] [coercion] [reducible] : strict_order A :=
+  definition order_pair.to_strict_order [trans_instance] [reducible] : strict_order A :=
   ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
 
   theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
@@ -181,7 +181,7 @@ have ne_ac : a ≠ c, from
   show false, from ne_of_lt' lt_bc eq_bc,
 show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
 
-definition strong_order_pair.to_order_pair [trans_instance] [coercion] [reducible]
+definition strong_order_pair.to_order_pair [trans_instance] [reducible]
     [s : strong_order_pair A] : order_pair A :=
 ⦃ order_pair, s,
   lt_irrefl := lt_irrefl',
@@ -196,7 +196,7 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak
 structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A,
     linear_weak_order A
 
-definition linear_strong_order_pair.to_linear_order_pair [trans_instance] [coercion] [reducible]
+definition linear_strong_order_pair.to_linear_order_pair [trans_instance] [reducible]
     [s : linear_strong_order_pair A] : linear_order_pair A :=
 ⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄
 
diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index aff691b6cb..66f4fb0844 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -384,7 +384,7 @@ section discrete_linear_ordered_field
       (assume H' : ¬ y < x,
         decidable.inl (le.antisymm (le_of_not_gt H') (le_of_not_gt H))))
 
-  definition discrete_linear_ordered_field.to_discrete_field [trans_instance] [reducible] [coercion]
+  definition discrete_linear_ordered_field.to_discrete_field [trans_instance] [reducible]
      :  discrete_field A :=
      ⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄
 
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 170654fcec..c900ebea22 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -210,13 +210,14 @@ theorem ordered_comm_group.lt_of_add_lt_add_left [s : ordered_comm_group A] {a b
 assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _,
 by rewrite *neg_add_cancel_left at H'; exact H'
 
-definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [coercion] [reducible]
+set_option pp.all true
+definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [reducible]
     [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
 ⦃ ordered_cancel_comm_monoid, s,
-  add_left_cancel       := @add.left_cancel A s,
-  add_right_cancel      := @add.right_cancel A s,
-  le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A s,
-  lt_of_add_lt_add_left := @ordered_comm_group.lt_of_add_lt_add_left A s⦄
+  add_left_cancel       := @add.left_cancel A _,
+  add_right_cancel      := @add.right_cancel A _,
+  le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A _,
+  lt_of_add_lt_add_left := @ordered_comm_group.lt_of_add_lt_add_left A _⦄
 
 section
   variables [s : ordered_comm_group A] (a b c d e : A)
@@ -582,12 +583,12 @@ structure decidable_linear_ordered_comm_group [class] (A : Type)
     (add_lt_add_left : ∀ a b, lt a b → ∀ c, lt (add c a) (add c b))
 
 definition decidable_linear_ordered_comm_group.to_ordered_comm_group
-      [trans_instance] [reducible] [coercion]
+      [trans_instance] [reducible]
    (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A :=
 ⦃ ordered_comm_group, s,
-  le_of_lt := @le_of_lt A s,
-  lt_of_le_of_lt := @lt_of_le_of_lt A s,
-  lt_of_lt_of_le := @lt_of_lt_of_le A s ⦄
+  le_of_lt := @le_of_lt A _,
+  lt_of_le_of_lt := @lt_of_le_of_lt A _,
+  lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄
 
 section
   variables [s : decidable_linear_ordered_comm_group A]
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index 9a234fc0b7..431b8bc0b7 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -235,20 +235,20 @@ begin
   exact (iff.mp !sub_pos_iff_lt H2)
 end
 
-definition ordered_ring.to_ordered_semiring [trans_instance] [coercion] [reducible]
+definition ordered_ring.to_ordered_semiring [trans_instance] [reducible]
     [s : ordered_ring A] :
   ordered_semiring A :=
 ⦃ ordered_semiring, s,
   mul_zero                   := mul_zero,
   zero_mul                   := zero_mul,
-  add_left_cancel            := @add.left_cancel A s,
-  add_right_cancel           := @add.right_cancel A s,
-  le_of_add_le_add_left      := @le_of_add_le_add_left A s,
-  mul_le_mul_of_nonneg_left  := @ordered_ring.mul_le_mul_of_nonneg_left A s,
-  mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right A s,
-  mul_lt_mul_of_pos_left     := @ordered_ring.mul_lt_mul_of_pos_left A s,
-  mul_lt_mul_of_pos_right    := @ordered_ring.mul_lt_mul_of_pos_right A s,
-  lt_of_add_lt_add_left      := @lt_of_add_lt_add_left A s⦄
+  add_left_cancel            := @add.left_cancel A _,
+  add_right_cancel           := @add.right_cancel A _,
+  le_of_add_le_add_left      := @le_of_add_le_add_left A _,
+  mul_le_mul_of_nonneg_left  := @ordered_ring.mul_le_mul_of_nonneg_left A _,
+  mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right A _,
+  mul_lt_mul_of_pos_left     := @ordered_ring.mul_lt_mul_of_pos_left A _,
+  mul_lt_mul_of_pos_right    := @ordered_ring.mul_lt_mul_of_pos_right A _,
+  lt_of_add_lt_add_left      := @lt_of_add_lt_add_left A _⦄
 
 section
   variable [s : ordered_ring A]
@@ -317,21 +317,21 @@ structure linear_ordered_ring [class] (A : Type)
     extends ordered_ring A, linear_strong_order_pair A :=
   (zero_lt_one : lt zero one)
 
-definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [coercion] [reducible]
+definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [reducible]
     [s : linear_ordered_ring A] :
   linear_ordered_semiring A :=
 ⦃ linear_ordered_semiring, s,
   mul_zero                   := mul_zero,
   zero_mul                   := zero_mul,
-  add_left_cancel            := @add.left_cancel A s,
-  add_right_cancel           := @add.right_cancel A s,
-  le_of_add_le_add_left      := @le_of_add_le_add_left A s,
-  mul_le_mul_of_nonneg_left  := @mul_le_mul_of_nonneg_left A s,
-  mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A s,
-  mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left A s,
-  mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right A s,
+  add_left_cancel            := @add.left_cancel A _,
+  add_right_cancel           := @add.right_cancel A _,
+  le_of_add_le_add_left      := @le_of_add_le_add_left A _,
+  mul_le_mul_of_nonneg_left  := @mul_le_mul_of_nonneg_left A _,
+  mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A _,
+  mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left A _,
+  mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right A _,
   le_total                   := linear_ordered_ring.le_total,
-  lt_of_add_lt_add_left      := @lt_of_add_lt_add_left A s ⦄
+  lt_of_add_lt_add_left      := @lt_of_add_lt_add_left A _ ⦄
 
 structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A
 
@@ -371,7 +371,7 @@ lt.by_cases
         end))
 
 -- Linearity implies no zero divisors. Doesn't need commutativity.
-definition linear_ordered_comm_ring.to_integral_domain [trans_instance] [coercion] [reducible]
+definition linear_ordered_comm_ring.to_integral_domain [trans_instance] [reducible]
     [s: linear_ordered_comm_ring A] : integral_domain A :=
 ⦃ integral_domain, s,
   eq_zero_or_eq_zero_of_mul_eq_zero :=
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index a7335a884f..a1fec765ae 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -174,7 +174,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc
         ... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib,
 show 0 * a = 0, from  (add.left_cancel this)⁻¹
 
-definition ring.to_semiring [trans_instance] [coercion] [reducible] [s : ring A] : semiring A :=
+definition ring.to_semiring [trans_instance] [reducible] [s : ring A] : semiring A :=
 ⦃ semiring, s,
   mul_zero := ring.mul_zero,
   zero_mul := ring.zero_mul ⦄
@@ -259,7 +259,7 @@ end
 
 structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
 
-definition comm_ring.to_comm_semiring [trans_instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A :=
+definition comm_ring.to_comm_semiring [trans_instance] [reducible] [s : comm_ring A] : comm_semiring A :=
 ⦃ comm_semiring, s,
   mul_zero := mul_zero,
   zero_mul := zero_mul ⦄
diff --git a/library/data/list/sort.lean b/library/data/list/sort.lean
index 8ea633969e..c41838c026 100644
--- a/library/data/list/sort.lean
+++ b/library/data/list/sort.lean
@@ -179,9 +179,9 @@ section
 open algebra
 omit decR
 lemma strongly_sorted_sort [ord : decidable_linear_order A] (l : list A) : strongly_sorted le (sort le l) :=
-strongly_sorted_sort_core le.total (@le.trans A ord) le.refl l
+strongly_sorted_sort_core le.total (@le.trans A _) le.refl l
 
 lemma sort_eq_of_perm {l₁ l₂ : list A} [ord : decidable_linear_order A] (h : l₁ ~ l₂) : sort le l₁ = sort le l₂ :=
-sort_eq_of_perm_core le.total (@le.trans A ord) le.refl (@le.antisymm A ord) h
+sort_eq_of_perm_core le.total (@le.trans A _) le.refl (@le.antisymm A _) h
 end
 end list
diff --git a/library/theories/group_theory/hom.lean b/library/theories/group_theory/hom.lean
index 109a0b3033..4eba4563ee 100644
--- a/library/theories/group_theory/hom.lean
+++ b/library/theories/group_theory/hom.lean
@@ -52,7 +52,7 @@ variables {A B : Type}
 variable [s1 : group A]
 
 definition id_is_iso [instance] : @is_hom_class A A s1 s1 (@id A) :=
-is_iso_class.mk (take a b, rfl) injective_id
+is_hom_class.mk (take a b, rfl)
 
 variable [s2 : group B]
 include s1
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 7562714804..e5e98ea149 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -818,7 +818,8 @@ struct structure_cmd_fn {
             save_def_info(coercion_name);
             add_alias(coercion_name);
             if (!m_private_parents[i]) {
-                m_env = add_coercion(m_env, m_p.ios(), coercion_name);
+                if (!m_modifiers.is_class() || !is_class(m_env, parent_name))
+                    m_env = add_coercion(m_env, m_p.ios(), coercion_name);
                 if (m_modifiers.is_class() && is_class(m_env, parent_name)) {
                     // if both are classes, then we also mark coercion_name as an instance
                     m_env = add_trans_instance(m_env, coercion_name);
diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean
index 92788f18a5..b45e06a887 100644
--- a/tests/lean/run/group5.lean
+++ b/tests/lean/run/group5.lean
@@ -139,8 +139,4 @@ calc
   a * 1 * b * c = a * b * c   : {!mul_right_id}
             ... = a * (b * c) : !mul_assoc
 
-theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
-calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : !mul_assoc
 end examples