I haven't used it but something like that exists https://github.com/gelisam/typelevel-rewrite-rules Rowan Goemans On 1/22/23 22:16, Henning Thielemann wrote:

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 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.