Предлагаю в этой теме заняться сабжем, тем более в новой версии компилятора значительно улучшили поддержку type-level программирования.

Общая идея: приписываем к хаскеллевским типам данных фантомный тип, содержащий некоторое утверждение относительно значения. Вот так http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype#Example_with_lists, например, можно добавлять к спискам информацию о наличии/отсутсвии в них элементов. Разумеется, в реальных примерах хотелось бы иметь расширяемый некий фреймворк, позволяющий не только нести встроенную информацию о наличии/отсутсвии элементов, но и дающий пользователю возможность добавлять свои утверждения. Как мы видим, сейчас это невозможно.

Вроде бы относящаяся к теме ссылка: http://okmij.org/ftp/Computation/lightweight-dependent-typing.html (сам еще не разбирался).

Предлагаю для разогрева реализовать тип моноида, который бы нёс информацию о том, является ли элемент единицой моноида. Т.е. (ложный псевдокод):

mappend :: (Monoid a) => TaggedMonoid a Identity -> TaggedMonoid a Identity -> TaggedMonoid a Identity
mappend _ _ = Tag mempty

mappend :: TaggedMonoid a Identity -> TaggedMonoid a NonIdentity -> TaggedMonoid a NonIdentity
mappend _ b = b

mappend :: TaggedMonoid a NonIdentity -> TaggedMonoid a Identity -> TaggedMonoid a NonIdentity
mappend a _ = a

mappend :: TaggedMonoid a NonIdentity -> TaggedMonoid a NonIdentity -> TaggedMonoid a NonIdentity
mappend a b = tag $ (untag a) `mappend` (untag b)

Ссылки, код, соображения на тему пишите в эту нить. Я тоже буду время от времени.