We present an algorithm for synthesizing recursive functions that provably satisfy a given specification in the form of a refinement type. We show that refinement types can be decomposed more effectively than other kinds of specifications, which helps prune the space of candidate programs the synthesizer has to consider. Our algorithm can automatically generate refined instantiations of polymorphic types, which enables synthesis of programs with nontrivial invariants from a small set of generic components. We have evaluated our prototype implementation on a set of benchmarks and found that it meets or exceeds the state of the art in terms of scalability and conciseness of user input, and also extends the class of programs for which a verified implementation can be synthesized.