chore: scope dangerous instances for monoid objects (#37883)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

@@ -40,7 +40,11 @@ variable {R : Type u} [CommRing R]
 
 namespace MonModuleEquivalenceAlgebra
 
-instance MonObj.toRing (A : ModuleCat.{u} R) [MonObj A] : Ring A :=
+/-- The ring structure on a monoid object.
+This instance is dangerous as it doesn't round trip from a ring to a monoid object and then back
+to a ring, since the `npow` field is lost in the middle. Therefore, it is scoped. -/
+@[implicit_reducible]
+def MonObj.toRing (A : ModuleCat.{u} R) [MonObj A] : Ring A :=
   { (inferInstance : AddCommGroup A) with
     one := η[A] (1 : R)
     mul := fun x y => μ[A] (x ⊗ₜ y)
@@ -65,7 +69,12 @@ instance MonObj.toRing (A : ModuleCat.{u} R) [MonObj A] : Ring A :=
     mul_zero := fun x => show μ[A] _ = 0 by
       rw [TensorProduct.tmul_zero, map_zero] }
 
-instance Algebra_of_Mon_ (A : ModuleCat.{u} R) [MonObj A] : Algebra R A where
+scoped[ModuleCat.MonModuleEquivalenceAlgebra] attribute [instance] MonObj.toRing
+
+/-- The algebra structure on a monoid object.
+This instance is dangerous as it doesn't round trip from a ring to a monoid object and then back
+to a ring, since the `npow` field is lost in the middle. Therefore, it is scoped. -/
+scoped instance Algebra_of_Mon_ (A : ModuleCat.{u} R) [MonObj A] : Algebra R A where
   algebraMap :=
   { η[A].hom with
     map_zero' := η[A].hom.map_zero