The tl;dr I got from it: all sets of possible values in your language constitute a lattice, with entries like Int in the lattice representing the set of all values that are integers. That lattice isn’t something you can actually instantiate, but you can build small, quotient lattices of it, such as projecting all sets into the lowest entry that consists solely of types (Int|String, for example) above a given set. You can construct a few such lattices and take a direct product of them to get a useful structure to do inference on. The quotient lattice of pure types with no user defined types can be packed into a bitfield efficiently.
The tl;dr I got from it: all sets of possible values in your language constitute a lattice, with entries like Int in the lattice representing the set of all values that are integers. That lattice isn’t something you can actually instantiate, but you can build small, quotient lattices of it, such as projecting all sets into the lowest entry that consists solely of types (Int|String, for example) above a given set. You can construct a few such lattices and take a direct product of them to get a useful structure to do inference on. The quotient lattice of pure types with no user defined types can be packed into a bitfield efficiently.