  A long-standing shortcoming of statically typed functional languages is that
type checking does not rule out pattern-matching failures (run-time match
exceptions). Refinement types distinguish different values of datatypes; if a
program annotated with refinements passes type checking, pattern-matching
failures become impossible. Unfortunately, refinement is a monolithic property
of a type, exacerbating the difficulty of adding refinement types to nontrivial
programs.
  Gradual typing has explored how to incrementally move between static typing
and dynamic typing. We develop a type system of gradual sums that combines
refinement with imprecision. Then, we develop a bidirectional version of the
type system, which rules out excessive imprecision, and give a type-directed
translation to a target language with explicit casts. We prove that the static
sublanguage cannot have match failures, that a well-typed program remains
well-typed if its type annotations are made less precise, and that making
annotations less precise causes target programs to fail later. Several of these
results correspond to criteria for gradual typing given by Siek et al. (2015).
