deriving instances

Stream: mathlib4

[Joël Riou]

In mathlib4#1132, some instances which were derived in mathlib using the @[derive ...] are no longer found with the new syntax deriving .... Examples are the Category instance for the essential image, and the Full and Faithful instances for the inclusion functor.

[Matej Penciak]

It looks like this is used in a bunch of places in mathlib... I can try to define a deriving handler for categories. Is there a place in mathlib3 where @[derive...] is defined? Is it expected that it should always follow from inferInstance?

[Scott Morrison]

There is a default derive handler that just dsimps the declaration and then runs type inference. For some reason we either don't have that, or its not firing correctly.

[Scott Morrison]

(In particular, there's nothing specific about category in the derive handlers.)

[Yaël Dillies]

Also, aren't we getting a problem with the fact that derived instances get the automatic name, which we've decided on not using?