The reason I have been against the idea so far is that an integer type is easily accomplished using the FFI and user code. Here is one example (not quite what you're asking for, but hopefully instructive): https://github.com/darinmorrison/purescript-int64
Personally, it surprises me that with all the years of extensions to ECMAScript, nobody has added 1) sized integer types like word32, word64, and so on, and 2) transparent bignums, similar to int/long in Python.
I mean there are several compilers from langs with strong type systems, such as F#->JS with FunScript, and in those, usually the source lang has integers...
For the cases you mention the checks would simply be: integer * integer = integer, integer + integer = integer. Problems only arise when real/floating point numbers are introduced and how to handle integer division.
If your claim is that no compiler in existence can make these kinds of checks at compile time, that's not true. Any dependently-typed language can do this (Idris, Coq, Agda, ATS). In fact, even a language with refinement types can do this, like Liquid Haskell.
And a number of languages do these checks at runtime: Ada and Nimrod are two that come to mind.