set tactic gives wrong type to variable

[Vierkantor]

Noticed in this Zulip thread. The following code attempts to define 6 matrices:

import data.matrix.notation

example : true :=
let X1 := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℕ), -- X1 : fin 1.succ → fin 2 → ℕ
    X2 : matrix (fin 2) (fin 2) ℕ := ![![1, 0], ![0, 0]] in -- X2 : matrix (fin 2) (fin 2) ℕ
begin
  set Y1 := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℕ), -- Y1 : fin 1.succ → fin 2 → ℕ
  set Y2 : matrix (fin 2) (fin 2) ℕ := ![![1, 0], ![0, 0]], -- Y2 : fin 1.succ → fin 2 → ℕ
  let Z1 := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℕ), -- Z1 : fin 1.succ → fin 2 → ℕ
  let Z2 : matrix (fin 2) (fin 2) ℕ := ![![1, 0], ![0, 0]], -- Z2 : matrix (fin 2) (fin 2) ℕ

  trivial
end

I'd expect that all the variables above would have type matrix (fin 2) (fin 2) ℕ, or at least that X2, Y2 and Z2 would. Instead, Y2 has type fin 1.succ → fin 2 → ℕ. This is not just confusing to the user, but also resulted in the wrong has_mul.mul instance being inferred.

[gebner]

Why would you expect Lean to infer matrix _ _ _ as the type here? The notation ![] expands to vec_empty, which literally has the type fin 0 → α. There's no matrix mentioned anywhere. How could Lean know that we want matrix here?

[Vierkantor]

Because we explicitly give the type : matrix (fin 2) (fin 2) ℕ?

[gebner]

Because we explicitly give the type : matrix (fin 2) (fin 2) ℕ?

Ah, I completely missed that part. This is definitely a bug in set then.

But I wonder if the matrix notation should have matrix type. Also (![] : matrix 0 0 ℕ) * (![] : matrix 0 0 ℕ) doesn't work (for a similar reason).

[Vierkantor]

That's true! (if you write matrix (fin 0) (fin 0) ℕ)

I think the notation should stay the same, since the type fin n -> α also represents vectors. Perhaps turning matrix from a semireducible definition into something more opaque (a structure?) and inserting explicit coercions will be a good workaround for now.