> This can be solved by dependent typing dependant typing isn't needed for some use cases you have mentioned: > list must not be empty you can use NonEmpty h

> This can be solved by dependent typing dependant typing isn't needed for some use cases you have mentioned: > list must not be empty you can use NonEmpty https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-List-NonEmpty.html https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-L... . We are still encoding this special case and our intent in types. Cons is that we need a special support for it (special library) where with dependant types we could reason about this use case without a special library EDIT: added newlines