  Refinement types enable lightweight verification of functional programs.
Algorithms for statically inferring refinement types typically work by
reduction to solving systems of constrained Horn clauses extracted from typing
derivations. An example is Liquid type inference, which solves the extracted
constraints using predicate abstraction. However, the reduction to constraint
solving in itself already signifies an abstraction of the program semantics
that affects the precision of the overall static analysis. To better understand
this issue, we study the type inference problem in its entirety through the
lens of abstract interpretation. We propose a new refinement type system that
is parametric with the choice of the abstract domain of type refinements as
well as the degree to which it tracks context-sensitive control flow
information. We then derive an accompanying parametric inference algorithm as
an abstract interpretation of a novel data flow semantics of functional
programs. We further show that the type system is sound and complete with
respect to the constructed abstract semantics. Our theoretical development
reveals the key abstraction steps inherent in refinement type inference
algorithms. The trade-off between precision and efficiency of these abstraction
steps is controlled by the parameters of the type system. Existing refinement
type systems and their respective inference algorithms, such as Liquid types,
are captured by concrete parameter instantiations. We have implemented our
framework in a prototype tool and evaluated it for a range of new parameter
instantiations (e.g., using octagons and polyhedra for expressing type
refinements). The tool compares favorably against other existing tools. Our
evaluation indicates that our approach can be used to systematically construct
new refinement type inference algorithms that are both robust and precise.
