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 |
Edited by Richard Eisenberg