> And you can do that in any language, regardless of its stance on typing.
Yes and no, because nothing prevents you from passing the wrong kind of value in an untyped language unless, well, you check for the runtime type yourself in the function and reject that. And you can only do that at runtime, at which point you'll not be able to immediately see where you're passing in invalid data accidentally unless you hit this exact branch in your code. So actually just the type tagging is quite useful already.
Also, it looks like more powerful dependently-typed languages like Idris[0] (and probably also Agda and Coq) can encode this information in the type system.