It's a continuum of how much checking/proving you want to do. Assuming that all Monoid instances obey the monoid laws is a pretty reasonable thing to do even i

It's a continuum of how much checking/proving you want to do. Assuming that all Monoid instances obey the monoid laws is a pretty reasonable thing to do even if you haven't proven every single instance yourself. It's the same as assuming that a Set<T> in e.g. Java actually obeys the set abstraction: has no duplicates, ordering is not guaranteed, etc. In practice the laws associated with type classes are a bit better specified in Haskell via either terse (algebraic) documentation or default implementations of associated functions. It would perhaps be nice if libraries which export type classes came with test functions that could be used to test your instances using some sort of QuickCheck-like approach. Though I've personally found that Haskell is sufficient at least my purposes, Idris currently seems the most "practical" of the dependently typed languages, but it's quite young and doesn't really have any ecosystem to speak of AFAICT.