TC for pointwise operations on `fun_like`?

Stream: maths

[Yury G. Kudryashov]

What do you think about this?

class has_pointwise_mul (F : Type*) {A B : out_param (Type*)} [fun_like F A B} [has_mul B]
  extends has_mul F :=
(mul_apply : ∀ (f g : F) (a : A), (f * g) a = f a * g a)

[Yury G. Kudryashov]

With this (and similar classes for has_one/has_scalar/has_pow/...) we can have, e.g.,

instance fun_like.semigroup (F : Type*) {A B : out_param (Type*)} [fun_like F A B] [semigroup B] [has_pointwise_mul F] :
  semigroup F :=
sorry

[Eric Wieser]

Are those instances safe? It feels like there might be a cycle hiding there

[Yury G. Kudryashov]

If we move fun_like to the end, then these instances should be safe. @Gabriel Ebner what should I tag with out_param in

variables (F : Type*) {ι : Type*} {α :  ι → Type*}

class has_pointwise_mul [Π i, has_mul (α i)] [fun_like F ι α] extends has_mul F :=
(mul_apply : ∀ (f g : F) (i : ι), (f * g) i = f i * g i)

instance fun_like.semigroup [Π i, semigroup (α i)] [fun_like F ι α] [has_pointwise_mul F] : semigroup F := sorry

to make has_pointwise_mul.to_has_mul and fun_like.semigroup safe?

[Gabriel Ebner]

out_param makes no difference as to whether an instance is safe or not, because out_param is ignored during type class search. TC instances are unsafe if they cause TC search to enumerate all instances; e.g. the first has_pointwise_mul.to_has_mul instance in this thread creates a subgoal has_mul ?B (starting from the right), and then Lean starts going through all possible ways to get a multiplication operator. So the last one seems fine in this regard, I would mark ι and α as out_param, just like in fun_like.

[Shing Tak Lam]

Are there any updates on this? It would be useful for what I'm doing in #16351. cc @Frédéric Dupuis .