I haven't had too many problems of this kind, but it does start becoming very painful if you work with GHC.TypeLits. It becomes very annoying using unsafeCoerce

I haven't had too many problems of this kind, but it does start becoming very painful if you work with GHC.TypeLits. It becomes very annoying using unsafeCoerce to "prove" to GHC that (a-1)+1 ~ a and other such trivialites. I realise solving these in the general case require the type checker to be equipped with a fully fledged SMT solver, but what I find really annoying is when GHC.TypeLits lacks the mechanism to solve simple contraints that you can get for free by lifting a simple inductive Nat type. For instance GHC doesn't know that + is injective, so can't deduce that given a ~ m+1 and a ~ n+1, m ~ n.