Notation `g^n` incurs two slow CoeTs

Stream: mathlib4

[Yongyi Chen]

MWE:

import Mathlib
set_option trace.Meta.synthInstance true
/-
The two offending CoeT calls:
[Meta.synthInstance] [0.506649s] ❌ CoeT ℤ x G ▶
[Meta.synthInstance] [0.508005s] ❌ CoeT G x ℤ ▶
-/
example [Group G] (g : G) (n : ℕ) (h : n = 0) : g ^ n = 1 := by
  sorry

[Patrick Massot]

Elaborations of powers will change very soon so it is probably not worth investigating this.

[Yongyi Chen]

It's conceivable that Lean will still try the two failed CoeT's, though.