Types express properties of programs; typechecking is specification checking. But the specifications expressed by conventional type systems are imprecise. Type refinements enable programmers to express more precise properties, while keeping typechecking decidable.

I present a system that unifies and extends past work on datasort and index refinements. Intersection and union types permit a powerful type system that requires no user input besides type annotations. Instead of seeing type annotations as a burden or just as a shield against undecidability, I see them as a desirable form of machine-checked documentation. Accordingly, I embrace the technique of bidirectional typechecking for everything from dimension types to first-class polymorphism.

My implementation of this type system, for a subset of Standard ML, found several bugs in the SML/NJ data structure libraries.