I realize this is just one example, but you might be interested to know that I've done some work making this kind of invariant enforceable via static types (though in practice, you need a combination of features that aren't found in many mainstream language besides Haskell afaik).
See the README here for motivation and some examples (in Haskell, but hopefully the idea is still clear): https://github.com/matt-noonan/justified-containers
Or the tutorial module here: https://hackage.haskell.org/package/justified-containers-0.3...
Or this paper, if you really want to go off the deep end: http://kataskeue.com/gdp.pdf
This post had some interesting tidbits about technical challenges, but I didn't fully grasp everything on first read: http://blog.ezyang.com/2016/04/hindley-milner-with-top-level...
I really like tome's observation in the other comment: universally-quantified types have a direct encoding in System F as type abstractions, but there is no such direct encoding for existentially-quantified types.
So is it similar to or different from assertions?
Suppose you have an XML format, <library> that has books and authors[1]. The elements look something like this: <book author-id="0000"/>, <author id="0000" name="Plath"/>. Obviously, you want to make sure that book's author-id attribute will always refer to an author that actually exists. This is something a (Java-style) static type system can't do: it doesn't know at compile-time what the contents of a variable will be. But spec can do this because it is a runtime check[2]: you'd just write a function that ensures all author-ids refer to extant authors and register it with spec, telling it that this must be true for valid <library>s.
As for your example, I don't think that is a use-case that spec was intended to handle. You could write a spec to ensure that an object has certain properties/methods, but I'm not spec would be too useful for a function invocation on that object.
[1]: For a worked out example of this in spec, see a blog post I wrote: https://lgessler.com/posts/2018-07-12-choosing-the-right-too...
[2]: It sounds expensive, but there's a compiler flag that lets you turn off all spec checks, so you can have them only run in dev builds if you like.