Dynamic languages defer type checking to runtime, enabling flexibility but leaving type errors undetected until execution. Static type systems catch errors early but are overly conservative, rejecting programs that would execute safely. Existing approaches either cannot simultaneously provide static safety guarantees and precise refutation of erroneous programs, or do so only at the cost of significant annotation burden and type-checking overhead.

We propose a type system with three contributions: (1) a modal type abstraction classifying terms as definitely safe, possibly crashing, or definitely crashing; (2) tabular types, which unify sufficiency and necessity analyses in a single framework, structured analogously to database tables and composed via joins; and (3) a type compression mechanism trading precision for simplicity. Together, these allow the system to refute more erroneous programs while preserving the guarantee that well-typed programs cannot go wrong.