Comment by josevalim

Oh, that’s exciting to hear! I would love to exchange notes and I know one of the lead researchers of set theoretic types would love to learn more about your uses too. If that sounds fun to you, you can find me on Gmail (same username).

In our case, we implement a bidirectional system where before applying x to Integer.to_string, we compute the domain of Integer.to_string (which is integer) and pass it up. If x is a dynamic type, then we refine it. So on the first call, x refines to `dynamic & integer`, then we apply it.

The second refinement fails because it becomes none, so we discard it, but it means the application on Atom.to_string will fail anyway. So yes, we check for emptiness and discard none.