[alcidesfonseca]

Liquid Types are more limited than "full dependent types" like Lean, Rocq, Agda or Idris. In Liquid Types you can refine your base types (Int, Bool), but you cannot refine all types. For instance, you cannot refine the function (a:Int | a > 0) -> {x:Int | x > a}. Functions are types, but are not refinable.

These restrictions make it possible to send the sub typing check to an SMT solver, and get the result in a reasonable amount of time.