Lean not seeing Fin m -> Fin n -> F as a Matrix Type

Stream: new members

[Vivek Rajesh Joshi]

What do I do to fix this error?

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Fin.Tuple.Reflection

variable (F : Type) [Field F] [DecidableEq F]

inductive RowEchelonForm : (m n : Nat) → Type where
| nil : RowEchelonForm m 0
| pad : RowEchelonForm m n → RowEchelonForm m n.succ
| extend : RowEchelonForm m n → (Fin n → F) → RowEchelonForm m n.succ

def RowEchelonForm.toMatrix (R : RowEchelonForm F m n) : Matrix (Fin m) (Fin n) F :=
  match R with
  | nil => fun _ => ![]
  | pad R0 => FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix
  | extend R0 v => Matrix.vecCons (Matrix.vecCons 1 v) (FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix)

Error:

type mismatch
  Matrix.vecCons (Matrix.vecCons 1 v) (FinVec.map (fun r ↦ Matrix.vecCons 0 r) (toMatrix R0))
has type
  Fin m.succ → Fin n✝.succ → F : Type
but is expected to have type
  Matrix (Fin m) (Fin n✝.succ) F : Type

[Yaël Dillies]

Matrix (Fin m) (Fin n✝.succ) F is Fin m → Fin n✝.succ → Frather than Fin m.succ → Fin n✝.succ → F

[Vivek Rajesh Joshi]

Ah, should have seen that. Thanks!

[Eric Wieser]

Note you should prefer to use Matrix.of to explicitly cast between the types

[Eric Wieser]

That would also have given you a better message here