Rewrite rules for constraints

[amigalemming]

I would like to write a rule like:

type SimplifyUnary (n::Nat) = IsUnary (ToUnary n) ~ (()::Constraint)

where IsUnary is a type class.
Currently the rule seems to have no effect. If it had, would it work at all? I mean, GHC might be missing the IsUnary class method dictionary.

[gelisam]

Currently the rule seems to have no effect.

It has no effect in code like IsUnary (ToUnary 4) => Int because typelevel-rewrite-rules only rewrites the types which occur inside equality constraints: in (A a ~ B a, C a) => D a, it only touches A a and B a, not C a.

[gelisam]

If it had, would it work at all? I mean, GHC might be missing the IsUnary class method dictionary.

When typechecker plugins remove constraints, they do need to insert a dictionary to compensate. See e.g. my tutorial on implementing "magic typeclasses".

Because typelevel-rewrite-rules only touches a ~ b constraints, I always use a dictionary which basically does unsafeCoerce: https://github.com/gelisam/typelevel-rewrite-rules/blob/main/src/TypeLevel/Rewrite.hs#L179