dangerous instances

Stream: mathlib4

[Lukas Miaskiwskyi]

In #1424, the linter is unhappy due to e.g. a dangerous instance in DistribMulActionHom.coe ; fully typed it reads as

instance DistribMulActionHom.coe.{u_1, u_2, u_3} (M : Type u_1) [inst✝ : Monoid M] (A : Type u_2) [inst✝¹ : AddMonoid A]
  [inst✝² : DistribMulAction M A] (B : Type u_3) [inst✝³ : AddMonoid B] [inst✝⁴ : DistribMulAction M B] :
  Coe (A →+[M] B) (A →+ B)

Looking around in Zulip gave me the impression that this is usually fixed by making things outParams, so writing

instance coe (M A B : outParam <| Type _) [Monoid M] [AddMonoid A]
  [AddMonoid B] [DistribMulAction M A] [DistribMulAction M B] : Coe (A →+[M] B) (A →+ B)

However, the complaint of the linter remains unchanged, being

/- The `dangerousInstance` linter reports:
SOME INSTANCES ARE DANGEROUS
During type-class search, they produce subgoals like `Group ?M`.
Try marking the dangerous arguments as implicit instead. -/
#check coe /- generates subgoals with metavariables: argument 4 inst✝⁴ : Monoid ?M -/

What is the approach here?

[Eric Wieser]

Arguably we should first add a FunLike instance in the Lean3 code before porting