ucsd-progsys/liquidhaskell — pull request #12 by ranjitjhala (2012-11-08 04:46:52+00:00)
Title: Added support for invariant specifications in data type definitions

See tests/{pos, neg}/record0.hs for details.

The main advantage (over using abstract refinements) is that you now get automatically inserted checks at all construction (fold) and match (unfold) sites -- otherwise, you would have to write a type alias for the refined data type and then tediously specify the type alias everywhere.