Hello, First of all, if you don't mind me not answering your question directly, I'd strongly suggest learning Agda or Idris before you start using dependent types in Haskell. (for example try the first two tutorials from here: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials) These are true dependently typed languages, and while GHC's extensions can get Haskell remarkably close, the result is still somewhat clunky. IMHO learning the basics in a cleaner environment is going to be much easier. Secondly, have a look at Liquid Haskell: http://ucsd-progsys.github.io/liquidhaskell-tutorial/01-intro.html Refinement types are a restricted kind of dependent types that can be solved automagically by SMT solvers. Thirdly, as for your actual question, have a look at this series of tutorials: https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dep... Best regards, Marcin Mrotek