>Much like java and javac are different tools, python and pytype/mypy are different tools

I get where you're heading. The `java` one is for JVM bytecode interpretation and the `javac` is for actual Java. Ok. Cool. I suppose that you do understand it well that leaving the choice on typechecking to external tools is something rather atrocious, do you?

>All of the python _I write_

The factory that produces the hammers for us carpenters provides just hammerheads alone and leaves us to choose and get the grips, so oftentimes fellow woodworkers use them without any grip whatsoever, some make flails and flail the nails, and I just go buy the soft grip from a third-party vendor. What's the problem here?

>[throws a Wikipedia link with the term definition at me, goes on showing me what must be done by a sum type]

You sure do consider me stupid, right? Anyway, what dependent types _usually_ do is they limit a category (think set) to some sub-category. Your example indeed describes dependent types but the problem with it is that it isn't a good place for dependent types. It can be expressed by sum types and I don't see any reason not to do so. By the way, do you have the sum types in Python nowadays?

>has generic types, not dependent types

(1) Look. Have you heard it anywhere that once you get powerful-enough generics, you can at least emulate dependent typing to some extent if not outright get it? Consider this: Java can express Peano numbers at the type level, along with Rust, C# and whatever there is with even remotely working generics. Do you know what that means to us here? Yes. We can express anything number-related at the type level, thus getting one little step closer to dependent typing. The most modest example of what you can do with that is a list with length limited on a type level, which qualifies pretty ok for dependent typing.

>not the _type_

Dependent typing is still about types, and if you work with these on a type level, you will deal with types. The type isn't inferred here but the value is limited by the type in question, so please don't say this, otherwise it will not constitute a sane type system. Imagine the types that just constatate the fact once it happened instead of setting an invariant (ah yes).

>with some massaging

Zero massaging[0] but ok. I hope that, knowing about [0], you've already guessed that there's an implementation of matrix multiplication with actual dependent types[1].

Actually, if you want, I could implement type-level floats for you but I'm not sure if they have any good use case and I'm pretty sure that some operations will compile for a little while: type families operating on numbers are usually defined in terms of recursion. Not sure if we're going to flex type systems at each other at this point, there's a clear winner even if we're not bringing the said to the table: static typing in Python isn't provided out of the box, and while your little example makes me check it out and appeals to me, it's still a third-party tool and that's not how it must be. I will not mention anything about types describing here. If that's not enforced by type system, it's pretty bad but there's no point in discussing that already, enough's been said.

>plainly cannot

Refer to (1).

[0]: http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-Ty...

[1]: https://hackage.haskell.org/package/linear-code-0.1.0/docs/M...

Edit 1: one more link.

Edit 2: a suggestion and some out-of-place conclusion.