[Haskell-cafe] Type constraint rewrite rules

[Henning Thielemann]

Has anyone thought about rewrite rules for type constraints as 
light-weight alternative to type-checker plugins?

Rewrite rules could be

   n + 'Zero -> n

   Back (Forth a) -> a
      for closed type families Back and Forth, where Back is the inverse of Forth


Ideally the programmer would also provide a correctness proof for the 
proposed rewrite, e.g. with a function that generates a

data BackForthProof a = (Back (Forth a) ~ a) => BackForthProof