This issue came up again today on Zulip:

class Funny (F : Type _) (A B : outParam (Type _)) where toFun : F → A → B
instance [Funny F A B] : CoeFun F fun _ => A → B where coe := Funny.toFun
class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends Funny F A B
class Monoid (M) extends Mul M
instance [Mul A] : Mul (Id A) := ‹_›
set_option trace.Meta.synthInstance true
example [Monoid A] [Monoid B] [MulHomClass F A B] (f : F) (a : A) : f a = f a := rfl -- infinite loop

The core issue is the instance:

MulHomClass.toFunny [Mul A] [Mul B] [MulHomClass F A B] : Funny F A B

When this instance is applied to Funny F ?A ?B (which is perfectly reasonable), we get a subgoal of the form Mul ?A (which is completely evil, as it causes us to enumerate all multiplicative structures).

We have tried various things in the past to address this issue, see 3f497b8 and #1852. But there doesn't seem to be a good description of the intended behavior we want in the end, and as a result these bandaid fixes rot over time.

For example 3f497b8 changes the arguments to {inst : Mul A} {inst : Mul B} because they're outParam-instances, in the projection construction. This was silently broken by several changes: 1) #1852 which removed the outParam-marker, and 2) by multiple inheritance for structures, where the non-subobject projections are generated differently.