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
• #25238 (closed) (I think)

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