Buenas, no nos queda muy claro algo sobre este ejercicio. Leyendo la letra suponemos que se refieren a matrices escalonadas de nxn. Lo que no vemos bien, y por ende no vemos el tipo, es qué es lo que se supone que hace el operador addM. Suponemos que se agrega un array a una matriz pero no vemos de que forma, ya que agregandola como fila o columna la matriz dejaria de ser cuadrada.
El tipo que pensamos es:
Parameter addM: forall (A:Set) (n:nat), A -> Matrix A n -> Array A n -> Matrix A (n+1).
Muchas gracias