> ... rewrite rules for type constraints ...

That's what FunDeps are, with the advantage you can stipulate multiple/multi-directional rewrites. (With a bit of effort you can support three FunDeps for `Nat` Plus.)

The more I think about it, the more it seems type-land 'solving' is not the same job as term-land 'evaluating'; and Type Families are the wrong tool for the job.

AntC