I keep thinking about the parallels between type checkers and abstract interpretation.
E.g. abstract interpretation saying "this is one of two values, but I don't know which" feels very much like type checking a boolean.
Have any tools taken advantage of this?