[trizinix]

Richard A. Eisenberg has a nice comparison of Dependent Haskell with Idris and Liquid Haskell in his PhD. thesis[1]. There is a difference between refinement types and dependent types. In Liquid Haskell you basically state some predicates and then let the SMT solver figure out whether they are true. With Dependent Types you have to do all the legwork, but they are also more powerful.

[1] https://github.com/goldfirere/thesis

[johncolanduoni]

It's also important to note that you can embed SMT-driven refinement types into a fully dependently typed language; that's what F* does. I wonder how feasible doing something similar in Idris via the elaborator reflection and type provider faculties is. I remember Brady did something following a similar principle in one of the elaborator reflection papers with automated proofs of termination, but without calling into an external SMT solver.

[hood_syntax]

Thank you for the recommendation