[Haskell-cafe] Type constraint rewrite rules

Henning Thielemann lemming at henning-thielemann.de
Sun Jan 22 21:16:51 UTC 2023

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

More information about the Haskell-Cafe mailing list