On Mon, 4 May 2015, Edward Kmett wrote:
The issue with a LiquidHaskell solution in this space, aside from the fact that it is an experiment that isn't part of the compiler or the language that we have, and uses assumptions about the way numbers work that don't hold for the ones we have, is that it is terribly invasive. In order to use it everything that ever wants to work with your shiny new non-empty list type needs to be written in LiquidHaskell to prove the non-empty invariant still holds. Refinement types are notoriously hard to use. On the other-hand a type like NonEmpty satisfies that invariant trivially: There is no empty constructor.
The price of this is that it is a different data type, with different operations.
In my experience with my non-empty package I found that I can lift that restriction by using type classes like Functor, Traversable etc.
I love LiquidHaskell, but I'd be very hesitant to do anything or rather to not do anything predicated on its existence.
Although LiquidHaskell is cool, I also prefer to solve simple problems with simple tools. Non-empty lists do not need a sophisticated prover framework, it can be solved with simple Haskell 98.