I hear different opinions about whether type checking is "an" instance of abstract interpretation (AI) or "the" instance (which IMHO is a useful question since we might consolidate our efforts on one method if possible).

This article does a very good job of laying out typical examples motivating AI as a concept.

But the process of attributing points in the AI lattice to expressions does look a lot like type inference (and the AI lattice itself does look a lot like a type hierarchy).

Does this point to a slightly different approach we should take to type systems? For example, suppose the type of '1' was not 'int' but rather '1' (a type runtime equivalent to unit, but carrying its information at compile-time), and that 'add' is overloaded on input types so that it can either directly compute its result (also then statically knowable) or emit instructions to dynamically compute its result if its arguments are only dynamically known.

Is that the meta lesson here? Should we be using more detailed/nuanced type systems?