attached is an example where the type checker isn't "computing" in the closed type families, or at least doing a one step reduction.

this makes sense, given that type families only compute when instantiated... But if we could partially evaluate closed type families (or at least do a one step reduction), the attached example code would type check!

interestingly, depending on what order the cases for the PSum are written, the type error changes!

I guess I want an "eager matching" closed type family, that when partially instantiated will patch on the first pattern it satisfies, to complement ordered type families.

attached is a toy example where I otherwise need an unsafeCoerce to make things type check