That was, of course, just an example. I'm also assuming that any "real" type system implemented this way would do this with something like typeclasses or higher kinds or something else.
The larger point is that baked-in type system see the word "int" as a type, but what that's hiding is the higher abstraction: that what we're really doing is specifying a function which should be run when determining the validity of the program.
But that was exactly my point: what IS this "higher abstraction" to which you allude? What are you actually advocating here? Typeclasses? Sequent calculus? Something else? Details matter.
I'm advocating something that typeclasses, sequent calculus, contracts, etc. could be built on. Sure, the language may have some standard libraries that would do much the same things that these do in other languages, but those libraries could be improved, removed, or replaced by the programmer.
What exactly is the point of a type system? I think there are really two big ones: program verification and metadata tagging. To simplify, the former is why Haskellers love types, and the latter seems to be the main reason that F#'s type providers exist (and why C# programmers love creating lots of little types rather than using typeless object literals a la Ruby).
Intellisense is an incredibly seductive thing, and many programmers in the enterprise world would argue that any language that can't show you that little "box" after you press Ctrl+Space is dead on arrival.
But both of those things are a subset of the things you COULD do if the phases of compilation were in your control. Maybe you want a function that says "throw an error at compile time if someone uses this deprecated parameter on this API call", or maybe you'd like to have a function where if you call it with a hard-coded URL, the program fails at compile time if the URL can't be reached.
These are obviously a bit silly, but the point is that, to many of us, WHENEVER a compiler is doing something with our AST, that should be fully exposed and not a black box. Another example: why is Idris[1] its own language? Why isn't it just a Haskell library? Granted that also gets into programmable syntax and editor support thereof, but that's part of my larger point as well.
One reason why Idris is its own language is that you can't just lie dependent types atop a language---that's the whole point, the types interact with the values and the values the types. This blurs the boundary between compiler phases.
Sometimes you get type erasure, but for really interesting programs to arise (the kind that I'm sure Idris is aiming at, though I don't know for certain) you really want to operate in that blurry divide.
Why int? What about adding floats? complex numbers? rationals? quaternions? matrices? dimensional quantities? etc. etc. etc.