[greenfield1]

I doubt it. The ultimate consequence of this endeavour is that a program that takes an int as input and produces an int as output would then have the type a:A->B(a). For example, a program P that for a given n produces the n-th prime number would express this in its type signature. Another program using that as a sub-function and doing p=P(n) could never reach the state where p is not the n-th prime number, the type system would be able to express that, and the type checker would need to be able to validate it. Etc. etc.

A type checker would amount to an automatic correctness proof, which in its full generality is impossible (by halting problem), but for the practically interesting classes could be done using a theorem prover / proof assistant and the occasional hint from the programmer. That would be great to have, but none of the examples you mention is anywhere close.

[kaba0]

Dependent types are this basically, Idris, Lean, etc having it. Though proving is a huge challenge, so it is no panacea.