Refinement Types refers to a type system where types can be constrained by a logical predicate in the form of a sublanguage.1 Refinement Types are weaker than Dependent Types.
Liquid Types are Refinement Types where the sublanguage is decidable. This allows the constraints to be solved with SMT solvers.