Narrowing

Inside a rule body, a guard that establishes a fact about a value refines that value’s type for the rest of the body. After x.field is not unknown, subsequent atoms read x.field as present; after a type test x: Employee succeeds, x carries Employee thereafter. This is occurrence typing — the type at a use site reflects what has been proven about the value on the path that reaches it.

The discipline is sound because narrowing predicates are upward-closed in information: once established at a state, a narrowing survives every state that carries more information. Gaining facts can extend what is known; it can never retract a narrowing already in force. The mechanization proves exactly this — every narrowing predicate holds monotonically as the state grows — which is what lets the type system trust a narrowed type through the rest of a body.