The example of dimension checking is handy, especially in fields where the same name for an idea has multiple incompatible instantiations or when there's an arbitrary choice that some subfield uses and some other makes differently (left vs right multiplication as a convention, left vs right handed coordinates as a convention, tensor ordering, ...). Sometimes better names help, but often they're just a lot of visual noise for the tiny bit of additional information they portray. Usually I use strings as type annotations for that purpose (compactly describing common constraints like the shape's shape, which dimensions are in common, ...) to communicate to other developers, but I could see a use case for some actual tooling, especially to the extent that somebody could build on top of the library and tailor it to some problem domain.
Seems you refer to a domain specific language in the annotations. This is exactly what https://github.com/AndreaCensi/contracts does (it's an amazing project but has a very large code base). However, I wanted to achieve something similar in pure python and as compact as possible – so there are compromises (like no real symbolic calculus)
def foobar(a: '(i>1, j)', b: '(j, k)') -> '(k,)':