HPow bug again

Stream: mathlib4

[Gareth Ma]

Firstly, my lean version is Lean (version 4.3.0-rc2, commit 8e5cf6466061, Release) and Mathlib is on commit 0f76a69bf023c58dfd2201fcd61d48a4e6d32452 (HEAD of origin/staging, apparently).

I think the following behaviour should've been fixed by lean4/2220 here, but it seems not. I don't know how to minimise it to not use Mathlib, so I am reporting here instead of #lean4.

import Mathlib
/- import Mathlib.Data.Matrix.Basic -/

def M : Matrix (Fin 2) (Fin 2) ℤ := !![1, 3; 2, 4]
#eval M                          -- works
#eval M ^ 2                      -- works
#eval (M ^ 2) 0 0                -- fails
#eval (M ^ 2 : Matrix _ _ _) 0 0 -- works
#eval (M ^ (2 : ℕ)) 0 0          -- works

local macro_rules | `($x ^ $y)  => `(HPow.hPow $x $y)
#eval (M ^ 2) 0 0                -- works

[Eric Wieser]

(M ^ 2 :) 0 0 is the shortest workaround here