The key insight that clarified things for me: refinement types are a restricted form of dependent types where the logic is restricted — you trade expressiveness for automation.

The LiquidHaskell tutorial literally says it: "Refinement Types can be thought of as a restricted class of [dependent types] where the logic is restricted, at the cost of expressiveness, but with the reward of a considerable amount of automation."

SMT solvers are magical but finite. They decide whether a formula is true (or give a counterexample) for a limited range of data types: numbers, sets, bit-vectors, arrays. Because most common program properties fall into those buckets, they cover an enormous amount of ground in practice. But "a limited range" is the operative phrase — step outside decidable theories and the solver can't help you.

In my day job (formally verifying financial settlement logic) LiquidHaskell + Z3 handles ~95% of what I need. The remaining 5% is usually: relational properties involving transitive closure, arbitrary recursive function correctness, or anything that requires knowing the value of a user-defined function at a specific point — i.e. things the SMT solver treats as fully uninterpreted and therefore knows nothing about.

Coming at this from a systems angle. I use Flux (refinement types for Rust) and F* for low-level crypto/systems code. My take:

Use refinement types when:

• Your invariants are arithmetic: buffer lengths, offsets, loop bounds, non-null, non-zero. This is 90% of C/C++/Rust safety bugs.
• You want verification to integrate invisibly into existing code. With Flux the annotations go in Rust attributes, the rest compiles normally.
• You can't ask your team to learn proof tactics. SMT automation means the tool does the heavy lifting — programmers write specs, not proofs.
• You need fast feedback loops. SMT solvers are fast. Rocq/Lean proof checking can be slow for large proof trees.

Use full dependent types when:

• You need to prove properties involving relationships between function outputs that aren't arithmetic. E.g. "the output list is a permutation of the input list."
• You need universe polymorphism or type-level computation.
• You're doing actual math formalization, not just "make the program not crash."
• You want to extract certified code from a proof (Coq's extraction, Lean's kernel).

The classic example that trips up refinement systems: proving reverse (reverse xs) == xs. In LiquidHaskell, you can express this but you have to write a proof term. At that point you're basically doing dependent types by hand inside the refinement system 😅

Let me be a bit more precise about why the SMT wall exists, because it matters for the "when to use what" question.

SMT solvers operate over ground theories — linear arithmetic (LIA/LRA), bitvectors, arrays, uninterpreted functions. The magic of liquid types is that your refinements are predicates in this decidable fragment. Checking subtyping reduces to checking validity of a formula in that fragment, and Z3 can decide it automatically.

The trouble: user-defined recursive functions are uninterpreted in the SMT backend. The solver knows len is a function, but it doesn't know len (Cons x xs) = 1 + len xs as a universally-quantified axiom — because quantifiers wreck decidability. LiquidHaskell's clever workaround is "measures" — it reflects the structure of the function into the types of constructors, keeping the SMT solver blissfully ignorant of the global definition. This works for many things but fails for equational reasoning across multiple recursive steps.

In a dependent type system like Rocq, you're in a full proof assistant. You can do induction, apply lemmas, use rewrite rules. Nothing is automatic, but nothing is out of reach either. The price is you write proofs. A non-trivial lemma might be:

Lemma rev_involutive : forall (A : Type) (l : list A),
  rev (rev l) = l.
Proof.
  intros A l. induction l as [| h t IH].
  - (* base case: nil *) reflexivity.
  - (* inductive step *)
    simpl. rewrite rev_app_distr. simpl.
    rewrite IH. reflexivity.
Qed.

That proof is trivially expressible but requires explicit induction. An SMT solver would need you to essentially give it this proof as a hint anyway at that point.

↩ FormalFelinae wrote:

user-defined recursive functions are uninterpreted in the SMT backend

Right, this is the crux. And I want to push back slightly — LiquidHaskell's Refinement Reflection feature (introduced in the 2018 "Theorem Proving for All" paper) actually does let you reflect function definitions into the refinement logic, so you CAN do some equational reasoning. The key idea is to "reflect the code implementing a user-defined function into the function's output refinement type" — meaning the function's definition becomes available as a proof term.

So you can write something like:

-- Reflect 'fib' into refinement logic
{-@ reflect fib @-}
fib :: Int -> Int
fib n
  | n == 0    = 0
  | n == 1    = 1
  | otherwise = fib (n-1) + fib (n-2)

-- Prove fib 2 = 1 via SMT + reflection
{-@ fib2 :: { fib 2 == 1 } @-}
fib2 = fib 1 `seq` fib 0

But — and this is important — even with reflection you still end up writing "proof terms" that guide the SMT solver. It's just that those proof terms are Haskell functions rather than Rocq tactics. You're doing a form of dependently-typed programming even within the refinement framework. The further you go, the more it resembles just... writing Agda in a trenchcoat.

That to me is the real crossover point: when your proof strategy requires writing more "proof scaffolding" than actual program code, you've passed the practical threshold of what refinement types are optimised for. Switch to a real proof assistant at that point.

I want to bring up F* explicitly because it occupies an interesting middle ground. F* started as a refinement type system but has grown to support full dependent types with effects. It's simultaneously:

• An SMT-backed verifier (like LiquidHaskell/Dafny) for the things Z3 can handle
• A proof assistant with dependent types for things that need induction/tactics
• A programming language that can extract to OCaml or C via KaRaMeL

The F* philosophy seems to be: "use SMT automation wherever possible, fall back to manual tactics when you must." This is attractive but comes with complexity costs — F* is a very large, complicated system. You're essentially wielding both hammers at once.

Dafny takes a similar "SMT-first, manual lemmas when needed" approach. The LiquidHaskell blog had a good comparison showing that in Dafny you sometimes need extra intermediate assertions to guide the verifier that LH can infer automatically from measures. Each tool has its own flavour of "where the automation ends."

My recommendation: if you're mostly doing program verification (not math formalization), F* or Dafny give you the best of both worlds at the cost of tooling complexity. If you're doing pure math, go Lean 4 or Rocq. If you want to stay in Haskell, LiquidHaskell is remarkably capable for its weight.

Let me share a concrete war story. We were verifying a Rust implementation of a sorted merge (think merge sort's merge step) using Flux. The refinement type approach worked beautifully for:

• Proving no out-of-bounds accesses (array length tracking)
• Proving the output length equals the sum of input lengths
• Proving termination (decreasing index arguments)

But when we wanted to prove "the output is sorted AND is a permutation of the concatenated input" — the sorted part was fine (it's an inductive numeric invariant), but "is a permutation" requires you to express multiset equality. That's not in the decidable SMT fragment for Flux's current logic. We ended up having to either:

1. Trust the permutation property through testing (gave up on proving it), or
2. Port that specific invariant to F* where we could write a manual inductive proof

We went with option 2 for the critical security-sensitive sort. The F* proof was about 150 lines for what was a 30-line Rust function. That's the tax of full dependent types — but for a crypto implementation where permutation correctness actually matters for security, it was worth it.

This is my heuristic: use refinement types for safety properties, use dependent types for liveness / functional correctness properties involving complex relational invariants.

There's a conceptual point that I think is worth making explicit: refinement types and dependent types differ fundamentally in their approach to proof relevance.

In a full dependent type system (Rocq, Agda, Lean), types are propositions and proofs are values — the Curry-Howard correspondence goes all the way down. A proof that n > 0 is an actual runtime value (even if erased). Dependent pairs (Σ-types) carry both a value and its proof. This proof-relevance is what enables:

• Inductive reasoning: you recurse on the structure of proofs
• Proof extraction: certified programs with correctness guarantees baked in
• Homotopy type theory: proof-relevant equality (path types)

In a refinement type system, the predicates are checked externally by the SMT solver — the proofs are not runtime values and aren't accessible inside your program. This is actually a feature: it means zero proof overhead at runtime. But it means you can't recurse on proof structure or use proof terms to guide type-level computation.

One interesting perspective: refinement types can be viewed as encoding dependent pairs where the predicate and proof are offloaded to the SMT oracle. Compiling refinement types into dependent types is actually an active research direction — the idea being to translate { n : Int | n > 0 } into a genuine Σ-type and preserve the operational semantics.

For practical day-to-day work though: if your team is PL researchers → Lean/Rocq. If your team is software engineers who want correctness → LiquidHaskell/Dafny/Flux. The ergonomics difference is enormous.

↩ RefinementRawr wrote:

what's the sharpest example of something that looks like it should be in the refinement fragment but isn't?

Classic one: list length after reverse. You'd think this is trivial arithmetic — len (reverse xs) == len xs. The length is just a number! But to prove it in a refinement system, you need to unfold the definition of reverse, which requires induction over the structure of the list. The SMT solver sees reverse as an uninterpreted function — it knows nothing about how its output length relates to its input. So this "arithmetic" fact is actually outside the decidable fragment.

LiquidHaskell handles it with Refinement Reflection + a manual proof term, but that's the point: you've crossed into writing actual proofs. Compare to Agda where length-reverse is a two-liner with cong and the standard library's ++-length lemma.

Another good one: map preserves length. len (map f xs) == len xs. Same story — trivially true by induction, but the SMT solver can't figure it out without a quantified axiom about how map behaves, and quantifiers = bye bye decidability.

The pattern: any property that requires knowing the behavior of a recursive function across all inputs, not just at specific call sites, is outside what SMT can handle without quantifiers. Refinement systems paper over this with measures and reflection but the limits are real.

I want to add something about the practical usability gap that often gets overlooked in these theory-heavy discussions.

With LiquidHaskell, you can drop into an existing Haskell codebase, add some annotations in comments ({-@ ... @-}), and start getting verification value immediately. The LiquidHaskell tutorial notes that since annotations appear in comments, you can introduce them into existing Haskell code without disrupting anything — the Liquid checker is entirely optional and doesn't affect GHC compilation.

With Lean 4 or Rocq, you're committing to a dedicated proof engineering workflow. Everything needs to be in the proof assistant's language. You can extract code, yes, but the integration story with existing codebases is very different — you're typically writing your verified code from scratch in the DT language, not annotating existing code.

For industry adoption, this is a massive practical advantage for refinement types. The counter-argument is that if you're building safety-critical certified software, starting fresh in Lean is a feature not a bug — your verified code IS the source of truth.

But most teams verifying "normal" software? Incremental annotation via refinements wins every time. You don't have to boil the ocean.

One more dimension: decidability and verification time.

Refinement type checking is decidable (for the pure SMT fragment). You run the checker, it terminates with SAFE or UNSAFE, usually in seconds. With full DT proof assistants, proof-checking is decidable (type-checking in CIC is decidable), but the proof development time is very much not bounded — you're writing proofs by hand and they can get arbitrarily complex.

There's also a nasty middle ground in tools like F* where you're mixing SMT automation with manual tactics. Sometimes a proof that "should" be automatic takes 30 seconds of Z3 timeout grinding, or worse, flaps (succeeds on some machine states, fails on others due to SMT nondeterminism). This is a genuine pain in real projects — your CI can fail intermittently because Z3 took a different path through its search space. With full dependent types, proof checking is deterministic: either your proof term typechecks or it doesn't.

tldr: SMT = fast when it works, nondeterministic when it doesn't. Manual DT proofs = slow to write, deterministic to check. Choose your poison 🐱

Great summary of the whole thread so far. Let me crystallize with what I think is the fundamental theoretical reason for the tradeoff:

Refinement types = decidable checking × restricted expressiveness
Dependent types = undecidable checking × arbitrary expressiveness

This isn't a flaw — it's a fundamental result. To get decidable verification, you must restrict the language of specifications. Rice's theorem lurks: any non-trivial semantic property of programs is undecidable in general. Both approaches dodge this, differently:

• Refinements restrict specs to a decidable fragment (SMT theories) and automate checking within that fragment
• Dependent types make the human write a proof witness — the type-checker only needs to verify that witness (which is decidable for CIC), not synthesize it

So the real question is never "which is more powerful?" (DT wins trivially). It's "can I express what I need to express in the refinement fragment?" If yes — use it, it's automated and ergonomic. If no — pick up Lean/Rocq/Agda and write the proof yourself.

And honestly? For most production software, the answer is "yes, the refinement fragment is enough." The bugs that kill prod systems are arithmetic bugs, null dereferences, buffer overflows, integer overflows — all first-class citizens in the refinement world. Full DT is mostly needed when you're building compilers, crypto, or formal math libraries.