Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of dependent types which distinguishes them?
If it helps, I came across Refined types via the Liquid Haskell project, and dependent types via Coq and Agda. That said, I'm looking for an explanation of how the theories differ.