Type/data family instances in kind checking
See
- Artem's blog post about this stuff; it's very helpful.
- This wiki page, written in response to this ticket
- This later wiki page, also written in response to this ticket
In TcEnv.hs there is a note AFamDataCon: not promoting data family constructors. It states that we can't use a promoted data family instance constructor because we would have to interleave the checking of instances and data types. But with the fix of #11348 (closed), we now do exactly this. In the example from the note
data family T a
data instance T Int = MkT
data Proxy (a :: k)
data S = MkS (Proxy 'MkT)-ddump-rn-trace shows these groups
rnTycl dependency analysis made groups
[[data family T a_apG]
[]
[data instance T Int = MkT],
[data Proxy (a_apF :: k_apE)]
[]
[],
[data S = MkS (Proxy MkT)]
[]
[]]That's to say, the instance T Int will in fact be checked before S. So let's remove this restriction.
See also (NB: "closed" means "closed because #12088 takes precendence")
- #11348 (closed)
- #16693
- #16410 (closed)
- #16448 (closed)
- #19527
- #19611 (closed)
- #20875 (closed)
- #20885 (closed)
- #21172 (closed)
- #22257
- #23496
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #11348 (closed) |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |