[Haskell-cafe] Type constraint rewrite rules

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