Deriving instance on a parameter of the target type

Stream: metaprogramming / tactics

[Robin Carlier]

Is there a written example somewhere of what it would look like to write a deriving handlers that derives some instances on a parameter of the target type a declaration?

To give some context, in Mathlib we have docs#CategoryTheory.Functor.FullyFaithful as a (non-instance) structure which allows to define two instances of the Prop-classes docs#CategoryTheory.Functor.Full and docs#CategoryTheory.Functor.Faithful via declarations docs#CategoryTheory.Functor.FullyFaithful.full and docs#CategoryTheory.Functor.FullyFaithful.faithful. To learn a few new things I’d like to have a go at writing a deriving handler that would let me write

def fullyFaithfulFoo : CategoryTheory.Functor.FullyFaithful (blah : CategoryTheory.Functor _ _) where
  …
  deriving FullAndFaithful -- Automatically derives blah.Full and blah.Faithful

and avoid having to manually register the two instances manually each time (which is what we do in Mathlib currently). But from what I could read and my limited understanding of metaprogramming, all of the examples I see about deriving handlers are about deriving stuff on inductive types, so I have a bit of trouble understanding how I would go at adapting them to this kind of situation.
First: is this a good use case for a deriving handler ?
If yes, any pointers/code to learn form (even vague) to achieve this kind of stuff?

[Jovan Gerbscheid]

I don't know how deriving handlers are implemented, but I'm wondering what the advantage is of deriving over an attribute, like in @[to_additive] or @[to_fun].

[Matthew Ballard]

I think better deriving handlers would be great, especially if we find ourselves needing to implement lots of structure wrappers for some reason...

[Robin Carlier]

Jovan Gerbscheid said:

I don't know how deriving handlers are implemented, but I'm wondering what the advantage is of deriving over an attribute, like in @[to_additive] or @[to_fun].

Yes, my "backup plan" would be an attribute using addRelatedDecl, but I wanted this as a occasion to learn more about the inner workings. I think for the functionality of automatically declaring these instances, both would be pretty similar.

[Jovan Gerbscheid]

My intuition of def foo deriving Bar is that it will generate an instance of Bar foo. Your example doesn't fit into this pattern, so I would find it a bit confusing.