bundling additive groups and multiplicative groups

Stream: lean4

[Edward Ayers]

I'm porting to_additive for mathlib4. The to_additive algorithm is complicated, and it seems like it is doing a lot because add_group and group are essentially part of completely separate class hierarchies and just coincidentally prove the same thing with different symbols.
I was wondering what the motivation was for having different classes in the first place. If I was coming to the problem for the first time I would attempt a bundled approach:

class Group {α : Type} (p : α → α → α) (i : α → α) (e : α) where
    ... axioms

class MulGroup α extends HasMul α, HasInv α, HasOne α :=
  Group α (. * .) (. ⁻¹) 1

class AddGroup α extends HasAdd α, HasNeg α, HasZero α :=
  Group α (. + .) (- .) 0

-- define syntax for ∙ ~ e somewhere here
variable [Group α ∙ ~ e] (x y : α)

lemma inv_mul_mul_inv : ~(x ∙ y) = ~y ∙ ~x := by
    ... proof

example [AddGroup β] (a b c : β) : c + -(x + y) = c + (- y + - x) := by
    rw [inv_mul_mul_inv]

The main problem seems to me that you need higher order unification to spot that inv_mul_mul_inv would apply to the example. I wonder whether it would be possible to get around this with heuristics, most of the time you are matching ∙ on + or * or maybe ∘. Are there any other reasons why the above bundling approach was not used?
I was wondering because it might be that the reasons are less compelling in Lean 4 and the design might be worth a revisit.

I know that Lean very rarely has bundled classes, but I think I missed the memo explaining why bundling is a bad idea.

[Leonardo de Moura]

The following link should be relevant for this discussion https://github.com/leanprover/lean/wiki/Refactoring-structures#encoding-the-algebraic-hierarchy-1

[Leonardo de Moura]

@Edward Ayers The plan in the link above never moved forward. I think the general consensus was that it would take a lot of energy to refactor the library, and it was not clear whether we would hit performance problems or other unforeseen issues.

[Edward Ayers]

I see thanks :blush: