Yes, and in general it's pretty clear as you're doing it that that's what's happening. The ML family and Haskell type systems occupy a pretty nice place on the

Yes, and in general it's pretty clear as you're doing it that that's what's happening. The ML family and Haskell type systems occupy a pretty nice place on the spectrum of expressiveness in that there's not much you can add to them without losing the ability to infer unique types. As long as your types are on the same level of complexity as a Haskell or ML type, you can typically get away with minimal type annotations - a bit more than ML or Haskell would've required, but not a lot more. When you introduce more complex quantifiers such as the "exists" in these examples, in practice you have to start thinking about "what the compiler knows" and how to help it know the things you want it to. There are some systems such as Coq that use heuristics (and let you write your own new heuristics) to try to automatically find proofs, and interactive sessions in which you guide the system to the proof by suggesting tactics that move hypotheses toward goals or vice versa. This is one of the major factors that, in common speech, distinguishes between "typed languages" and "proof assistants" which otherwise are basically the same kind of thing. Even in proof assistants, though, you still need to be quite intentional about what lemmas need to be proven in order to move toward your ultimate goal, and often even in how you phrase your goals in order to improve the chances that the heuristics will find a proof. These are the kinds of things i mean by "helping" the system in my previous comment. They are very powerful tools if assurance of correctness is a high priority, but definitely not a free lunch. If you're ever interested in going down the rabbit hole, there's a pretty steep learning curve (though if you're comfortable with ML or Haskell you're already halfway up it) but an extensive and rewarding landscape of thought at the top. Unfortunately it's more of an academic or self-enrichment discipline than an industrial one these days, but if you look hard enough there are a few jobs where you can make use of these tools.