[Haskell-cafe] Enforcing data structures invariant in the type system

[Marcin Mrotek]

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/dependent-types-in-haskell

Best regards,
Marcin Mrotek