chore: clean up "dangerous instance" porting notes (#18041)

Most of these notes are about issues in Lean 3 that are no longer issues in Lean 4, so they can be easily removed. A few need some more explanation.
leanprover-community · Oct 24, 2024 · 8fd75ac · 8fd75ac
1 parent 9715344
commit 8fd75ac
Show file tree

Hide file tree

Showing 11 changed files with 4 additions and 30 deletions.
diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean
@@ -44,8 +44,6 @@ class AlgEquivClass (F : Type*) (R A B : outParam Type*) [CommSemiring R] [Semir
   /-- An equivalence of algebras commutes with the action of scalars. -/
   commutes : ∀ (f : F) (r : R), f (algebraMap R A r) = algebraMap R B r
 
--- Porting note: Removed nolint dangerousInstance from AlgEquivClass.toRingEquivClass
-
 namespace AlgEquivClass
 
 -- See note [lower instance priority]
@@ -141,7 +139,6 @@ protected theorem coe_coe {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R
 theorem coe_fun_injective : @Function.Injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) fun e => (e : A₁ → A₂) :=
   DFunLike.coe_injective
 
--- Porting note: Made to CoeOut instance from Coe, not dangerous anymore
 instance hasCoeToRingEquiv : CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂) :=
   ⟨AlgEquiv.toRingEquiv⟩
 

diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean
@@ -45,9 +45,6 @@ class AlgHomClass (F : Type*) (R A B : outParam Type*)
   [FunLike F A B] extends RingHomClass F A B : Prop where
   commutes : ∀ (f : F) (r : R), f (algebraMap R A r) = algebraMap R B r
 
--- Porting note: `dangerousInstance` linter has become smarter about `outParam`s
--- attribute [nolint dangerousInstance] AlgHomClass.toRingHomClass
-
 -- For now, don't replace `AlgHom.commutes` and `AlgHomClass.commutes` with the more generic lemma.
 -- The file `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` slows down by
 -- 15% if we would do so (see benchmark on PR #18040).

diff --git a/Mathlib/Algebra/Algebra/NonUnitalHom.lean b/Mathlib/Algebra/Algebra/NonUnitalHom.lean
@@ -80,12 +80,8 @@ abbrev NonUnitalAlgHomClass (F : Type*) (R A B : outParam Type*)
     [DistribMulAction R A] [DistribMulAction R B] [FunLike F A B] :=
   NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B
 
--- Porting note: commented out, not dangerous
--- attribute [nolint dangerousInstance] NonUnitalAlgHomClass.toMulHomClass
-
 namespace NonUnitalAlgHomClass
 
--- Porting note: Made following instance non-dangerous through [...] -> [...] replacement
 -- See note [lower instance priority]
 instance (priority := 100) toNonUnitalRingHomClass
   {F R S A B : Type*} {_ : Monoid R} {_ : Monoid S} {φ : outParam (R →* S)}

diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@@ -1190,7 +1190,6 @@ end Group
 
 section VSub
 
--- Porting note: Reordered [VSub α β] and [DecidableEq α] to make vsub less dangerous. Bad?
 variable [VSub α β] [DecidableEq α] {s s₁ s₂ t t₁ t₂ : Finset β} {u : Finset α} {a : α} {b c : β}
 
 /-- The pointwise subtraction of two finsets `s` and `t`: `s -ᵥ t = {x -ᵥ y | x ∈ s, y ∈ t}`. -/

diff --git a/Mathlib/Algebra/Module/LinearMap/Defs.lean b/Mathlib/Algebra/Module/LinearMap/Defs.lean
@@ -110,10 +110,6 @@ class SemilinearMapClass (F : Type*) {R S : outParam Type*} [Semiring R] [Semiri
 
 end
 
--- Porting note: `dangerousInstance` linter has become smarter about `outParam`s
--- `σ` becomes a metavariable but that's fine because it's an `outParam`
--- attribute [nolint dangerousInstance] SemilinearMapClass.toAddHomClass
-
 -- `map_smulₛₗ` should be `@[simp]` but doesn't fire due to `lean4#3701`.
 -- attribute [simp] map_smulₛₗ
 
@@ -139,7 +135,6 @@ variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMon
 variable [Module R M] [Module R M₂] [Module S M₃]
 variable {σ : R →+* S}
 
--- Porting note: the `dangerousInstance` linter has become smarter about `outParam`s
 instance (priority := 100) instAddMonoidHomClass [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
     AddMonoidHomClass F M M₃ :=
   { SemilinearMapClass.toAddHomClass with

diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean
@@ -329,7 +329,7 @@ class RingHomClass (F : Type*) (α β : outParam Type*)
 
 variable [FunLike F α β]
 
--- Porting note: marked `{}` rather than `[]` to prevent dangerous instances
+-- See note [implicit instance arguments].
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} [RingHomClass F α β]
 
 /-- Turn an element of a type `F` satisfying `RingHomClass F α β` into an actual

diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean
@@ -61,9 +61,6 @@ class SeminormClass (F : Type*) (𝕜 E : outParam Type*) [SeminormedRing 𝕜]
 
 export SeminormClass (map_smul_eq_mul)
 
--- Porting note: dangerous instances no longer exist
--- attribute [nolint dangerousInstance] SeminormClass.toAddGroupSeminormClass
-
 section Of
 
 /-- Alternative constructor for a `Seminorm` on an `AddCommGroup E` that is a module over a

diff --git a/Mathlib/CategoryTheory/Comma/Arrow.lean b/Mathlib/CategoryTheory/Comma/Arrow.lean
@@ -88,7 +88,6 @@ theorem mk_injective (A B : T) :
 theorem mk_inj (A B : T) {f g : A ⟶ B} : Arrow.mk f = Arrow.mk g ↔ f = g :=
   (mk_injective A B).eq_iff
 
-/- Porting note: was marked as dangerous instance so changed from `Coe` to `CoeOut` -/
 instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where
   coe := mk
 

diff --git a/Mathlib/GroupTheory/GroupAction/Hom.lean b/Mathlib/GroupTheory/GroupAction/Hom.lean
@@ -356,9 +356,6 @@ abbrev DistribMulActionHomClass (F : Type*) (M : outParam Type*)
     [DistribMulAction M A] [DistribMulAction M B] [FunLike F A B] :=
     DistribMulActionSemiHomClass F (MonoidHom.id M) A B
 
-/- porting note: Removed a @[nolint dangerousInstance] for
-DistribMulActionHomClass.toAddMonoidHomClass not dangerous due to `outParam`s -/
-
 namespace DistribMulActionHom
 
 /- Porting note (#11215): TODO decide whether the next two instances should be removed
@@ -601,9 +598,6 @@ abbrev MulSemiringActionHomClass
     [DistribMulAction M R] [DistribMulAction M S] [FunLike F R S] :=
   MulSemiringActionSemiHomClass F (MonoidHom.id M) R S
 
-/- porting note: Removed a @[nolint dangerousInstance] for MulSemiringActionHomClass.toRingHomClass
- not dangerous due to outParam -/
-
 namespace MulSemiringActionHom
 
 /- Porting note (#11215): TODO decide whether the next two instances should be removed

diff --git a/Mathlib/LinearAlgebra/Ray.lean b/Mathlib/LinearAlgebra/Ray.lean
@@ -188,9 +188,9 @@ set_option linter.unusedVariables false in
 def RayVector (R M : Type*) [Zero M] :=
   { v : M // v ≠ 0 }
 
--- Porting note: Made Coe into CoeOut so it's not dangerous anymore
 instance RayVector.coe [Zero M] : CoeOut (RayVector R M) M where
   coe := Subtype.val
+
 instance {R M : Type*} [Zero M] [Nontrivial M] : Nonempty (RayVector R M) :=
   let ⟨x, hx⟩ := exists_ne (0 : M)
   ⟨⟨x, hx⟩⟩

diff --git a/Mathlib/Order/Heyting/Hom.lean b/Mathlib/Order/Heyting/Hom.lean
@@ -99,8 +99,8 @@ section Hom
 
 variable [FunLike F α β]
 
-/- Porting note: `[HeytingAlgebra α, β]` -> `{ _ : HeytingAlgebra α, β}` as a dangerous instance fix
-similar for Coheyting & Biheyting instances -/
+/-! This section passes in some instances implicitly. See note [implicit instance arguments] -/
+
 -- See note [lower instance priority]
 instance (priority := 100) HeytingHomClass.toBoundedLatticeHomClass [HeytingAlgebra α]
     { _ : HeytingAlgebra β} [HeytingHomClass F α β] : BoundedLatticeHomClass F α β :=