> 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?

I'd suggest you attempt to do so. If you mean that, with the benefit of hindsight, you could go back and replace the string with an enum or set of flags, sure, but no, the signature of the function in question is, and due to historical baggage, must stay

def open(path: _PathType, mode: str) -> Union[IO[Text], IO[bytes]]: ...

It's just that the set of values `mode` can take on is restricted to a list of ~30 valid strings, which importantly can affect the output type and swap it from Text to bytes. Python already has sum types, and they, uhh, can't solve this problem, as you should know.

> Dependent typing is still about types

Well kind of, in the sense that Literal[4] or Nat::2 is a type, yes. In the sense that Literal[4] is a subclass of int, yes. But it's very different, and much more powerful, because most type systems force you to deal with types as sets of values, and you can't introspect into the sets at all. Dependent types let you introspect and care about particular values, and so you don't have to deal with the types as opaque things. You can care about values, and you aren't restricted to working with only types. But yes the values are still types.

> 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?

Yes, but implementing peano numerals in java or rust's type system isn't the same as having literal-dependent types, in which you can dispatch based on the actual values present in the language. PEANO_FOUR isn't the same as `4`, and short of a massive amount of codegeneration, you're not gonna have PEANO_FIFTEEN in java generics. Or I mean, if you want to do that, be my guest, but I'll just use `4`.

Or to put it another way: yes, Java's type system is technically turing complete. That doesn't mean that it is pleasant to write programs that execute only during java compilation. Support for literal dependent types makes that more pleasant (and in some cases possible, I'm not actually clear on how you'd write a java function that compiles if passed `4`, and fails to compile otherwise, bridging the gap between PEANO_FOUR and `4` isn't, I don't believe, possible in java. You can no longer use java's own integer class in your code, you have to use your new peano integer class). Native support for dependent types inverts that.

> I suppose that you do understand it well that leaving the choice on typechecking to external tools is something rather atrocious, do you?

This depends. There's a gradient: I run probably 20-30 static analysis tools on my code, from linters to typecheckers to autoformatters. Things that check for malformed TODO comments and all kinds of other fun things. They all prevent various classes of errors. I think not investing in typechecking for large programs is bad, but I also think there's a huge value in gradual typing. Being able to explore interactively in a repl is something that would be painful in java or C++, but is quite pleasant in python. Being able to then convert that code to be production ready by adding types and type-checking, without rewriting in a totally new language, is also quite pleasant. Leaving a user without the choice is also atrocious for many styles of development. That python is able to work for more than one is imo, a feature more than a bug.