A question about types, answered yes, no with a value, or unknown.

The analysis answers questions about types so that it can narrow, and a wrong answer in the safe direction costs only precision: Feel.Type.Union.subtype?/2 says false both when a type is not within another and when it could not show that it is. That is the right direction for the optimizer and the wrong one for a verdict on a model, where "this table has a gap" and "this table might have a gap" have to be told apart.

• :yes is a proof: the analysis showed it (subtype?/2 is true, an intersection is none).
• {:no, value} is a counterexample: a value that the exact check (Feel.Type.Union.contains?/2) says is in the one type and not in the other. It does not depend on the analysis having been exact.
• :unknown is neither: no proof, and no value was found (the search was cut, or the types are of a kind that Feel.Type.Witness makes no value of: a time, a date and time, a range, a function).

A table whose rules cover the inputs is :yes; one that leaves an input out is {:no, input} with that input; a large or an odd one may be :unknown.

iex> alias Feel.Type.Verdict
iex> Verdict.subtype([:number], [:number, :null])
:yes
iex> {:no, nil} = Verdict.subtype([:number, :null], [:number])
iex> Verdict.disjoint([:number], [:string])
:yes
iex> {:no, "a"} = Verdict.disjoint([{:string, ["a", "b"]}], [{:string, ["a"]}])
iex> {:no, _value} = Verdict.empty([:number])
iex> Verdict.empty([])
:yes