Comment by Tuna-Fish

> Can the typechecker ensure that your matrices have compatible dimensions to be multiplied together?

In any dependently typed language, absolutely yes.