explicit `↑` in coercions + infix operators = unfolding timeout

Minimized from an issue originally reported on Zulip. Explicit coercion arrows seem to badly interact with the infix% term elaborator, causing nonassignable metavariables to be created which cause unification to go on a wild goose chase of definition unfolding:

def dontUnfoldMe (x : Int) : Nat → List Bool → Nat
  | 0, _ => 0
  | n+1, l => dontUnfoldMe x n (true::l) + dontUnfoldMe x n (false::l)

theorem dontUnfoldMe_eq (x) : ∀ n l, dontUnfoldMe x n l = 0
  | 0, _ => rfl
  | n+1, l => by rw [dontUnfoldMe, dontUnfoldMe_eq x n, dontUnfoldMe_eq x n]

example (a : Int) (n : Nat) : dontUnfoldMe (a * n) 14 [] = 0 :=
  dontUnfoldMe_eq (a * n) 14 [] -- fast
example (a : Int) (n : Nat) : dontUnfoldMe (a * n) 14 [] = 0 :=
  dontUnfoldMe_eq (a * ↑n) 14 [] -- slow

Here dontUnfoldMe is written such that it exponentially blows up if you unfold it. The Meta.isDefEq trace looks like this:

  [] 💥 dontUnfoldMe (a * ?m.1656) 14 [] =?= dontUnfoldMe (a * Int.ofNat n) 14 [] ▼
    [] ❌ a * ?m.1656 =?= a * Int.ofNat n ▼
      [] ✅ a =?= a 
      [] ❌ ?m.1656 =?= Int.ofNat n ▼
        [] ?m.1656 [nonassignable] =?= Int.ofNat n [nonassignable] 
      [] ❌ instHMul.1 a ?m.1656 =?= instHMul.1 a (Int.ofNat n) ▼
        [] ❌ Mul.mul a ?m.1656 =?= Mul.mul a (Int.ofNat n) ▼
          [] ✅ a =?= a 
          [] ❌ ?m.1656 =?= Int.ofNat n ▼
            [] ?m.1656 [nonassignable] =?= Int.ofNat n [nonassignable] 
          [] ❌ Int.instMulInt.1 a ?m.1656 =?= Int.instMulInt.1 a (Int.ofNat n) ▼
            [] ❌ Int.mul a ?m.1656 =?= Int.mul a (Int.ofNat n) ▶
    [] 💥 dontUnfoldMe (a * ?m.1656) 13 [true] +
          dontUnfoldMe (a * ?m.1656) 13
            [false] =?= dontUnfoldMe (a * Int.ofNat n) 13 [true] + dontUnfoldMe (a * Int.ofNat n) 13 [false] ▶

Start with the minimized examples contrasting a * n and a * ↑n, then inspect the infix% term elaborator and the Meta.isDefEq trace shown in the report. Done means the explicit-coercion case no longer creates the nonassignable metavariable path that triggers exponential unfolding and a timeout.