This is a single issue for issues or feature requests for to_additive, that I'll try to keep up-to-date. Feel free to comment with other suggestions

• Reorder arguments using an arbitrary permutation. This can be used to fix some to_additive connections in [Merged by Bors] - feat: Port GroupTheory.GroupAction.Prod #1056
• Improve output of to_additive?, showing the type of the generated declaration (and not the body for lemmas)
• Even more reorder features, so that we can reorder Pow.mk to SMul.mk (requires re-ordering the function arguments in a particular argument)
• to_additive (attr := scoped simp) can scope the additive version in the wrong namespace (Zulip).
• [bug] additivize lemmas generated by norm_cast (and other attributes).
• Allow specifying types where to_additive doesn't translate operations. Zulip 1 2 -- fixed by [Merged by Bors] - feat(to_additive): option to not translate operations on a type #19297
• [probably wontfix]: to_additive does not support match ... with. Zulip, also filed as to_additive doesn't support match #1428
• noncomputable definitions in a noncomputable sections won't be translated properly unless you explicitly specify noncomputable (this is feat: mark predefinitions that failed to compile as noncomputable leanprover/lean4#2610)
• The congr can generate complicated terms involving Eq.rec that to_additive has a hard time to additivize. E.g. MeasureTheory.Measure.haar.prehaar_sup_eq
• Apparently to_additive doesn't work well with private: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60.40.5Bto_additive.5D.60.20bug.3F
• to_additive doesn't copy the docstring of alias: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20and.20deprecated.20alias
• alias, deprecated, and to_additive don't get along togther #19424
• to_additive should additivize structures (warning: requires syntax for adding docstrings to constructors)
• to_additive should additivize instances created by the extends-clause for structures (i.e. put these instances into the translation dictionary). This is possible since feat: record all structure parents in StructureInfo leanprover/lean4#5853 -- fixed in [Merged by Bors] - fix(to_additive): automatically translate all instances generated by extends #19302
• Improve the to_additive heuristic so that we can support lemmas that have both a variable ring-like type (that should not be additivized) and a variable monoid-like type (that should be). This would allow writing a multiplicative version of MeasureTheory.convolution where G is multiplicative and to_additive additivizes it (without touching 𝕜) (Zulip, and there are probably more).
  Note: We now have the option dont_translate to work around limitations of the heuristic.
• (low priority) More robustly reorder universe variables
• Allow for a declaration to have multiple to_additive translations, depending on the "relevant" arguments (the types where we additivize functions). We can already specify which ones to translate using dont_translate, and this would require finding the right translation, and maybe automatically generating the names of the various additive versions.
• (hard) somehow translate from G →* Multiplicative H to Additive G →+ H
• to_dual and to_additive interaction, and potentially with a third translation attribute (or simps)
• Make guessName hashmaps into environment extesions