fix(*): lower instance priority (#1724)

* fix(*): lower instance priority

use lower instance priority for instances that always apply
also do this for automatically generated instances using the `extend` keyword
also add a comment to most places where we short-circuit type-class inference. This can lead to greatly increased search times (see issue #1561), so we might want to delete some/all of them.

* put default_priority option inside section

Default priority also applies to all instances, not just automatically-generates ones
the scope of set_option is limited to a section

* two more low priorities

* fix some broken proofs

* fix proof

* more fixes

* more fixes

* increase max_depth a bit

* update notes

* fix linter issues

Author: fpvandoorn

src/algebra/category/CommRing/basic.lean

@@ -39,14 +39,14 @@ def of (R : Type u) [semiring R] : SemiRing := bundled.of R
 
 local attribute [reducible] SemiRing
 
-instance : has_coe_to_sort SemiRing := infer_instance
+instance : has_coe_to_sort SemiRing := infer_instance -- short-circuit type class inference
 
 instance (R : SemiRing) : semiring R := R.str
 
 instance bundled_hom : bundled_hom @ring_hom :=
 ⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
 
-instance : concrete_category SemiRing := infer_instance
+instance : concrete_category SemiRing := infer_instance -- short-circuit type class inference
 
 instance has_forget_to_Mon : has_forget₂ SemiRing Mon :=
 bundled_hom.mk_has_forget₂ @semiring.to_monoid (λ R₁ R₂, ring_hom.to_monoid_hom) (λ _ _ _, rfl)
@@ -68,13 +68,13 @@ def of (R : Type u) [ring R] : Ring := bundled.of R
 
 local attribute [reducible] Ring
 
-instance : has_coe_to_sort Ring := infer_instance
+instance : has_coe_to_sort Ring := infer_instance -- short-circuit type class inference
 
 instance (R : Ring) : ring R := R.str
 
-instance : concrete_category Ring := infer_instance
+instance : concrete_category Ring := infer_instance -- short-circuit type class inference
 
-instance has_forget_to_SemiRing : has_forget₂ Ring SemiRing := infer_instance
+instance has_forget_to_SemiRing : has_forget₂ Ring SemiRing := infer_instance  -- short-circuit type class inference
 instance has_forget_to_AddCommGroup : has_forget₂ Ring AddCommGroup :=
 -- can't use bundled_hom.mk_has_forget₂, since AddCommGroup is an induced category
 { forget₂ :=
@@ -93,13 +93,13 @@ def of (R : Type u) [comm_semiring R] : CommSemiRing := bundled.of R
 
 local attribute [reducible] CommSemiRing
 
-instance : has_coe_to_sort CommSemiRing := infer_instance
+instance : has_coe_to_sort CommSemiRing := infer_instance -- short-circuit type class inference
 
 instance (R : CommSemiRing) : comm_semiring R := R.str
 
-instance : concrete_category CommSemiRing := infer_instance
+instance : concrete_category CommSemiRing := infer_instance -- short-circuit type class inference
 
-instance has_forget_to_SemiRing : has_forget₂ CommSemiRing SemiRing := infer_instance
+instance has_forget_to_SemiRing : has_forget₂ CommSemiRing SemiRing := infer_instance -- short-circuit type class inference
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 instance has_forget_to_CommMon : has_forget₂ CommSemiRing CommMon :=
@@ -119,13 +119,13 @@ def of (R : Type u) [comm_ring R] : CommRing := bundled.of R
 
 local attribute [reducible] CommRing
 
-instance : has_coe_to_sort CommRing := infer_instance
+instance : has_coe_to_sort CommRing := infer_instance -- short-circuit type class inference
 
 instance (R : CommRing) : comm_ring R := R.str
 
-instance : concrete_category CommRing := infer_instance
+instance : concrete_category CommRing := infer_instance -- short-circuit type class inference
 
-instance has_forget_to_Ring : has_forget₂ CommRing Ring := infer_instance
+instance has_forget_to_Ring : has_forget₂ CommRing Ring := infer_instance -- short-circuit type class inference
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 instance has_forget_to_CommSemiRing : has_forget₂ CommRing CommSemiRing :=

src/algebra/category/Group.lean

@@ -39,7 +39,7 @@ namespace Group
 local attribute [reducible] Group
 
 @[to_additive]
-instance : has_coe_to_sort Group := infer_instance
+instance : has_coe_to_sort Group := infer_instance -- short-circuit type class inference
 
 @[to_additive add_group]
 instance (G : Group) : group G := G.str
@@ -48,10 +48,10 @@ instance (G : Group) : group G := G.str
 instance : has_one Group := ⟨Group.of punit⟩
 
 @[to_additive]
-instance : concrete_category Group := infer_instance
+instance : concrete_category Group := infer_instance -- short-circuit type class inference
 
 @[to_additive has_forget_to_AddMon]
-instance has_forget_to_Mon : has_forget₂ Group Mon := infer_instance
+instance has_forget_to_Mon : has_forget₂ Group Mon := infer_instance -- short-circuit type class inference
 
 end Group
 
@@ -68,17 +68,17 @@ namespace CommGroup
 local attribute [reducible] CommGroup
 
 @[to_additive]
-instance : has_coe_to_sort CommGroup := infer_instance
+instance : has_coe_to_sort CommGroup := infer_instance -- short-circuit type class inference
 
 @[to_additive add_comm_group]
 instance (G : CommGroup) : comm_group G := G.str
 
 @[to_additive] instance : has_one CommGroup := ⟨CommGroup.of punit⟩
 
-@[to_additive] instance : concrete_category CommGroup := infer_instance
+@[to_additive] instance : concrete_category CommGroup := infer_instance -- short-circuit type class inference
 
 @[to_additive has_forget_to_AddGroup]
-instance has_forget_to_Group : has_forget₂ CommGroup Group := infer_instance
+instance has_forget_to_Group : has_forget₂ CommGroup Group := infer_instance -- short-circuit type class inference
 
 @[to_additive has_forget_to_AddCommMon]
 instance has_forget_to_CommMon : has_forget₂ CommGroup CommMon :=

src/algebra/category/Mon/basic.lean

@@ -58,7 +58,7 @@ def of (M : Type u) [monoid M] : Mon := bundled.of M
 local attribute [reducible] Mon
 
 @[to_additive]
-instance : has_coe_to_sort Mon := infer_instance
+instance : has_coe_to_sort Mon := infer_instance -- short-circuit type class inference
 
 @[to_additive add_monoid]
 instance (M : Mon) : monoid M := M.str
@@ -68,7 +68,7 @@ instance bundled_hom : bundled_hom @monoid_hom :=
 ⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
 
 @[to_additive]
-instance : concrete_category Mon := infer_instance
+instance : concrete_category Mon := infer_instance -- short-circuit type class inference
 
 end Mon
 
@@ -85,16 +85,16 @@ def of (M : Type u) [comm_monoid M] : CommMon := bundled.of M
 local attribute [reducible] CommMon
 
 @[to_additive]
-instance : has_coe_to_sort CommMon := infer_instance
+instance : has_coe_to_sort CommMon := infer_instance -- short-circuit type class inference
 
 @[to_additive add_comm_monoid]
 instance (M : CommMon) : comm_monoid M := M.str
 
 @[to_additive]
-instance : concrete_category CommMon := infer_instance
+instance : concrete_category CommMon := infer_instance -- short-circuit type class inference
 
 @[to_additive has_forget_to_AddMon]
-instance has_forget_to_Mon : has_forget₂ CommMon Mon := infer_instance
+instance has_forget_to_Mon : has_forget₂ CommMon Mon := infer_instance -- short-circuit type class inference
 
 end CommMon
 

src/algebra/char_zero.lean

@@ -34,6 +34,7 @@ theorem ordered_cancel_comm_monoid.char_zero_of_inj_zero {α : Type*}
   (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
 char_zero_of_inj_zero (@add_left_cancel _ _) H
 
+@[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_semiring.to_char_zero {α : Type*}
   [linear_ordered_semiring α] : char_zero α :=
 ordered_cancel_comm_monoid.char_zero_of_inj_zero $

src/algebra/euclidean_domain.lean

@@ -10,6 +10,8 @@ import data.int.basic
 
 universe u
 
+section prio
+set_option default_priority 100 -- see Note [default priority]
 class euclidean_domain (α : Type u) extends nonzero_comm_ring α :=
 (quotient : α → α → α)
 (quotient_zero : ∀ a, quotient a 0 = 0)
@@ -28,15 +30,18 @@ class euclidean_domain (α : Type u) extends nonzero_comm_ring α :=
   function from weak to strong. I've currently divided the lemmas into
   strong and weak depending on whether they require `val_le_mul_left` or not. -/
 (mul_left_not_lt : ∀ a {b}, b ≠ 0 → ¬r (a * b) a)
+end prio
 
 namespace euclidean_domain
 variable {α : Type u}
 variables [euclidean_domain α]
 
 local infix ` ≺ `:50 := euclidean_domain.r
 
+@[priority 100] -- see Note [lower instance priority]
 instance : has_div α := ⟨quotient⟩
 
+@[priority 100] -- see Note [lower instance priority]
 instance : has_mod α := ⟨remainder⟩
 
 theorem div_add_mod (a b : α) : b * (a / b) + a % b = a :=
@@ -235,6 +240,7 @@ by have := @xgcd_aux_P _ _ _ a b a b 1 0 0 1
   (by rw [P, mul_one, mul_zero, add_zero]) (by rw [P, mul_one, mul_zero, zero_add]);
 rwa [xgcd_aux_val, xgcd_val] at this
 
+@[priority 100] -- see Note [lower instance priority]
 instance (α : Type*) [e : euclidean_domain α] : integral_domain α :=
 by haveI := classical.dec_eq α; exact
 { eq_zero_or_eq_zero_of_mul_eq_zero :=
@@ -331,6 +337,7 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
     by rw [← mul_one a.nat_abs, int.nat_abs_mul];
     exact mul_le_mul_of_nonneg_left (int.nat_abs_pos_of_ne_zero b0) (nat.zero_le _) }
 
+@[priority 100] -- see Note [lower instance priority]
 instance discrete_field.to_euclidean_domain {K : Type u} [discrete_field K] : euclidean_domain K :=
 { quotient := (/),
   remainder := λ a b, if b = 0 then a else 0,

src/algebra/field.lean

@@ -9,10 +9,12 @@ open set
 universe u
 variables {α : Type u}
 
--- Default priority sufficient as core version has custom-set lower priority (100)
 /-- Core version `division_ring_has_div` erratically requires two instances of `division_ring` -/
+-- priority 900 sufficient as core version has custom-set lower priority (100)
+@[priority 900] -- see Note [lower instance priority]
 instance division_ring_has_div' [division_ring α] : has_div α := ⟨algebra.div⟩
 
+@[priority 100] -- see Note [lower instance priority]
 instance division_ring.to_domain [s : division_ring α] : domain α :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b h,
     classical.by_contradiction $ λ hn,
@@ -122,6 +124,7 @@ lemma div_eq_iff_mul_eq (hb : b ≠ 0) : a / b = c ↔ c * b = a :=
 
 end division_ring
 
+@[priority 100] -- see Note [lower instance priority]
 instance field.to_integral_domain [F : field α] : integral_domain α :=
 { ..F, ..division_ring.to_domain }
 

src/algebra/gcd_domain.lean

@@ -13,12 +13,17 @@ variables {α : Type*}
 
 set_option old_structure_cmd true
 
+
+
+section prio
+set_option default_priority 100 -- see Note [default priority]
 /-- Normalization domain: multiplying with `norm_unit` gives a normal form for associated elements. -/
 class normalization_domain (α : Type*) extends integral_domain α :=
 (norm_unit : α → units α)
 (norm_unit_zero      : norm_unit 0 = 1)
 (norm_unit_mul       : ∀{a b}, a ≠ 0 → b ≠ 0 → norm_unit (a * b) = norm_unit a * norm_unit b)
 (norm_unit_coe_units : ∀(u : units α), norm_unit u = u⁻¹)
+end prio
 
 export normalization_domain (norm_unit norm_unit_zero norm_unit_mul norm_unit_coe_units)
 
@@ -127,6 +132,8 @@ quotient.induction_on a normalize_idem
 
 end associates
 
+section prio
+set_option default_priority 100 -- see Note [default priority]
 /-- GCD domain: an integral domain with normalization and `gcd` (greatest common divisor) and
 `lcm` (least common multiple) operations. In this setting `gcd` and `lcm` form a bounded lattice on
 the associated elements where `gcd` is the infimum, `lcm` is the supremum, `1` is bottom, and
@@ -142,6 +149,7 @@ class gcd_domain (α : Type*) extends normalization_domain α :=
 (gcd_mul_lcm    : ∀a b, gcd a b * lcm a b = normalize (a * b))
 (lcm_zero_left  : ∀a, lcm 0 a = 0)
 (lcm_zero_right : ∀a, lcm a 0 = 0)
+end prio
 
 export gcd_domain (gcd lcm gcd_dvd_left gcd_dvd_right dvd_gcd  lcm_zero_left lcm_zero_right)
 

src/algebra/group/hom.lean

@@ -47,6 +47,15 @@ When they can be inferred from the type it is faster to use this method than to
 is_group_hom, is_monoid_hom, monoid_hom
 
 -/
+
+/- Note [low priority instance on morphisms]:
+  We have instances stating that the composition or the product of two morphisms is again a morphism.
+  Type class inference will "succeed" in applying these instances when they shouldn't apply (for
+  example when the goal is just `⊢ is_mul_hom f` the instances `is_mul_hom.comp` or `is_mul_hom.mul`
+  might still succeed). This can cause type class inference to loop.
+  To avoid this, we make the priority of these instances very low. We should think about not making
+  these declarations instances in the first place.
+-/
 universes u v
 variables {α : Type u} {β : Type v}
 
@@ -67,13 +76,15 @@ variables [has_mul α] [has_mul β] {γ : Type*} [has_mul γ]
 instance id : is_mul_hom (id : α → α) := {map_mul := λ _ _, rfl}
 
 /-- The composition of maps which preserve multiplication, also preserves multiplication. -/
-@[to_additive "The composition of addition preserving maps also preserves addition"]
+-- see Note [low priority instance on morphisms]
+@[priority 10, to_additive "The composition of addition preserving maps also preserves addition"]
 instance comp (f : α → β) (g : β → γ) [is_mul_hom f] [hg : is_mul_hom g] : is_mul_hom (g ∘ f) :=
 { map_mul := λ x y, by simp only [function.comp, map_mul f, map_mul g] }
 
 /-- A product of maps which preserve multiplication,
 preserves multiplication when the target is commutative. -/
-@[instance, to_additive]
+-- see Note [low priority instance on morphisms]
+@[instance, priority 10, to_additive]
 lemma mul {α β} [semigroup α] [comm_semigroup β]
   (f g : α → β) [is_mul_hom f] [is_mul_hom g] :
   is_mul_hom (λa, f a * g a) :=
@@ -88,6 +99,8 @@ lemma inv {α β} [has_mul α] [comm_group β] (f : α → β) [is_mul_hom f] :
 
 end is_mul_hom
 
+section prio
+set_option default_priority 100 -- see Note [default priority]
 /-- Predicate for add_monoid homomorphisms (deprecated -- use the bundled `monoid_hom` version). -/
 class is_add_monoid_hom [add_monoid α] [add_monoid β] (f : α → β) extends is_add_hom f : Prop :=
 (map_zero : f 0 = 0)
@@ -96,6 +109,7 @@ class is_add_monoid_hom [add_monoid α] [add_monoid β] (f : α → β) extends
 @[to_additive is_add_monoid_hom]
 class is_monoid_hom [monoid α] [monoid β] (f : α → β) extends is_mul_hom f : Prop :=
 (map_one : f 1 = 1)
+end prio
 
 namespace is_monoid_hom
 variables [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
@@ -121,7 +135,7 @@ variables [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
 instance id : is_monoid_hom (@id α) := { map_one := rfl }
 
 /-- The composite of two monoid homomorphisms is a monoid homomorphism. -/
-@[to_additive]
+@[priority 10, to_additive] -- see Note [low priority instance on morphisms]
 instance comp {γ} [monoid γ] (g : β → γ) [is_monoid_hom g] :
   is_monoid_hom (g ∘ f) :=
 { map_one := show g _ = 1, by rw [map_one f, map_one g] }
@@ -142,12 +156,15 @@ instance is_add_monoid_hom_mul_right {γ : Type*} [semiring γ] (x : γ) :
 
 end is_add_monoid_hom
 
+section prio
+set_option default_priority 100 -- see Note [default priority]
 /-- Predicate for additive group homomorphism (deprecated -- use bundled `monoid_hom`). -/
 class is_add_group_hom [add_group α] [add_group β] (f : α → β) extends is_add_hom f : Prop
 
 /-- Predicate for group homomorphisms (deprecated -- use bundled `monoid_hom`). -/
 @[to_additive is_add_group_hom]
 class is_group_hom [group α] [group β] (f : α → β) extends is_mul_hom f : Prop
+end prio
 
 /-- Construct `is_group_hom` from its only hypothesis. The default constructor tries to get
 `is_mul_hom` from class instances, and this makes some proofs fail. -/
@@ -161,7 +178,7 @@ variables [group α] [group β] (f : α → β) [is_group_hom f]
 open is_mul_hom (map_mul)
 
 /-- A group homomorphism is a monoid homomorphism. -/
-@[to_additive to_is_add_monoid_hom]
+@[priority 100, to_additive to_is_add_monoid_hom] -- see Note [lower instance priority]
 instance to_is_monoid_hom : is_monoid_hom f :=
 is_monoid_hom.of_mul f
 
@@ -179,7 +196,7 @@ eq_inv_of_mul_eq_one $ by rw [← map_mul f, inv_mul_self, map_one f]
 instance id : is_group_hom (@id α) := { }
 
 /-- The composition of two group homomomorphisms is a group homomorphism. -/
-@[to_additive]
+@[priority 10, to_additive] -- see Note [low priority instance on morphisms]
 instance comp {γ} [group γ] (g : β → γ) [is_group_hom g] : is_group_hom (g ∘ f) := { }
 
 /-- A group homomorphism is injective iff its kernel is trivial. -/
@@ -192,7 +209,7 @@ lemma injective_iff (f : α → β) [is_group_hom f] :
     simpa using inv_eq_of_mul_eq_one (h _ hxy)⟩
 
 /-- The product of group homomorphisms is a group homomorphism if the target is commutative. -/
-@[instance, to_additive]
+@[instance, priority 10, to_additive] -- see Note [low priority instance on morphisms]
 lemma mul {α β} [group α] [comm_group β]
   (f g : α → β) [is_group_hom f] [is_group_hom g] :
   is_group_hom (λa, f a * g a) :=

src/algebra/lie_algebra.lean

@@ -79,6 +79,8 @@ end
 
 end ring_commutator
 
+section prio
+set_option default_priority 100 -- see Note [default priority]
 /--
 A Lie ring is an additive group with compatible product, known as the bracket, satisfying the
 Jacobi identity. The bracket is not associative unless it is identically zero.
@@ -88,6 +90,7 @@ class lie_ring (L : Type v) [add_comm_group L] extends has_bracket L :=
 (lie_add : ∀ (x y z : L), ⁅z, x + y⁆ = ⁅z, x⁆ + ⁅z, y⁆)
 (lie_self : ∀ (x : L), ⁅x, x⁆ = 0)
 (jacobi : ∀ (x y z : L), ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0)
+end prio
 
 section lie_ring
 
@@ -150,13 +153,16 @@ def lie_ring.of_associative_ring (A : Type v) [ring A] : lie_ring A :=
 
 end lie_ring
 
+section prio
+set_option default_priority 100 -- see Note [default priority]
 /--
 A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi
 identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.
 -/
 class lie_algebra (R : Type u) (L : Type v)
   [comm_ring R] [add_comm_group L] extends module R L, lie_ring L :=
 (lie_smul : ∀ (t : R) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆)
+end prio
 
 @[simp] lemma lie_smul  (R : Type u) (L : Type v) [comm_ring R] [add_comm_group L] [lie_algebra R L]
   (t : R) (x y : L) : ⁅x, t • y⁆ = t • ⁅x, y⁆ :=