Proposition types complement subtyping

The way wombat2 works, both at compile time and runtime, is that actions are taken to move an expression's known type down the hierarchy. When we get to a type restricted to a single value then we have evaluated the expression. When we get down to a type restricted to the empty set of values, then expression evaluation has failed.

A natural question is: why do we have types representing propositions, such as:  x <% y. Why not just simple boolean expressions.

Suppose we have a type Dog, and it's a subtype of Animal. We have a value x of type Animal, and we have some proposition about it: say hasTail(x). Moving down the subtyping hierarchy can't invalidate a witness of this, or a witness of its negation. But if we can't decide until we've moved to a more specific subtype then the proposition and its negation both stay empty. Propositions can be evaluated at the right level of generality.