A refinement type attaches a logical predicate to a base type: {x : Int | x > 0} is the positives, {a : Array | len a > 0} is the non-empty arrays. The type checker discharges the predicates — often to an SMT solver — so head can require a non-empty list and a caller who cannot prove it gets a type error. Refinement types are a sweet spot: far more expressive than plain types, far more automatable than full dependent types. They let you state and enforce “this is always in range” without writing a proof by hand.
The refinement {x | x > 0} over a sample array. The demo counts how many values inhabit the refined type: live demo
“Int is Int; ranges are a runtime concern.” — a refinement makes “positive” part of the type, so the check happens once, at compile time, and every use downstream is free. The predicate rides in the type instead of littering the code with guards. cited
A refinement is a proof obligation the type carries: state x > 0 and the solver must discharge it at every use. Verification becomes typechecking — without hand-written proofs. Constable · Liquid Types
On the canonical compiler, over [5, -2, 3, 0, 7] the refinement {x | x > 0} has 3 inhabitants (5, 3, 7):