<div dir="ltr">> ... <span style="color:rgb(0,0,0);white-space:pre-wrap">rewrite rules for type constraints ...</span><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">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.)</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">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.</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">AntC</span></div></div>