A GHC type checker plugin that enables you to specify rewrite rules in order to prove type equalities.

Has a nice list of alternatives in the bottom, too. Among them:

  1. ghc-typelits-natnormalize, a GHC plug-in
  2. Thoralf, another GHC plugin
  3. Liquid Haskell
  4. Ghosts of Departed Proofs, a library
  5. an approach called Hasochism