strange error in `to_additive`

Stream: mathlib4

[Arien Malec]

I'm porting Algebra.PUnitInstances (mathlib4#1319) and getting very odd errors with to_additive like

application type mismatch
  HSMul.hSMul
argument has type
  HVAdd R PUnit PUnit
but function has type
  [self : HSMul R PUnit PUnit] → R → PUnit → PUnit

as if to_additive is getting confused?

[Riccardo Brasca]

This also happens in mathlib4#1238

[Floris van Doorn]

@Arien Malec there was some configuration of to_additive that was not ported over from Lean 3. Can you merge your branch with mathlib4#1330, and see if that fixes it?

[Floris van Doorn]

mathlib4#1332 fixes the issue in mathlib4#1238

[Arien Malec]

Confirmed fixed.