> For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that.

Numpy arrays have been checkable by dtype for a little while now, and I think recent versions also support shape constraints.