I'm not sure how a python annotation/type system could possibly do that? If numpy/pandas had different types for different cardinalities it would work today.

You just need those libraries to embrace it really, then you could theoretically have type constructors that provide well-typed NxM matrix types or whatever, allowing you to enforce that [[1,2],[3,4]] is an instance of matrix_t(2, 2).

I don't see how python could possibly make such inferences for arbitrary libraries.