have EquivLike using FunLike?

Stream: mathlib4

[Antoine Chambert-Loir]

I have a question about the design of structures and classes in mathlib, especially with respect to extends.
Let's take the example of docs#AddHom and docs#AddHomClass, and their analogue docs#AddEquiv and docs#AddEquivClass.

Specifically, I don't understand why docs#AddEquiv is defined using extends AddHom, while docs#AddEquivClass is defined using an explicit rewriting of the additive property.

If one does this, one gets an error message

parent field type mismatch, field 'coe_injective'' from parent 'FunLike' has type
  Function.Injective coe : Prop
but is expected to have type
  ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g

which suggests that EquivLike should have borrowed its coe_injective' field from FunLike rather than redefining it.

[Antoine Chambert-Loir]

There is a note after the definition of EquivLike that its definition of coe_injective' makes application of congr' easier. My feeling is that this change makes all further definitions of classes more delicate (or prone to errors).

[Jireh Loreaux]

There's a thread, and even a closed mathlib 3 PR where I redefined EquivLike to extend FunLike. Ultimately, it was determined that people just didn't want this or feel it was necessary.