Transitive closure in instance search

Stream: mathlib4

[Yury G. Kudryashov]

I started experimenting with BundledSet (see #2202). The plan is to add structures like

structure IsSubsemigroup (s : Set G) : Prop where
  mul_mem : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s

structure IsSubmonoid (s : Set G) : Prop extends IsSubsemigroup s where
  one_mem : 1 ∈ s

then use

structure BundledSet (p : Set α → Prop) where
  carrier : Set α
  prop : p carrier

In order to automatically cast, e.g., Submonoid G to Subsemigroup G, I tried to add

class Implies (p q : Set α → Prop) : Prop where
  implies : ∀ s, p s → q s

I'm trying to add transitivity instance for Implies but it fails with error message

cannot find synthesization order for instance @instImplies with type
  ∀ {α : Type u_1} {p q r : Set α → Prop} [inst : Implies p q] [h : Implies q r], Implies p r
all remaining arguments have metavariables:
  @Implies α p ?q
  @Implies α ?q r

I tried adding ImpliesTC but this doesn't help because nothing can be a semiOutParam in the transitive instance anyway.

[Yury G. Kudryashov]

Is there a workaround? Can instance search do this?

[Yury G. Kudryashov]

Or we'll need to add instances like this

instance [Implies p IsSubmonoid] : Implies p IsSubsemigroup

instead of

instance : Implies IsSubmonoid IsSubsemigroup