Less conservative compatibility check for closed type families
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
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |