Opened 16 months ago

Last modified 5 months ago

#13650 new task

Implement KPush in types

Reported by: goldfire Owned by: goldfire
Priority: high Milestone:
Component: Compiler Version:
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


A recent commit contributed a Note that explains why we need the dreaded KPush rule to be implemented in splitTyConApp. Without KPush there, it's possible that we can have two types t1 and t2 such that t1 `eqType` t2 and yet they respond differently to splitTyConApp: t1 = (T |> co1) (a |> co2) and t2 = T a. Both t1 and t2 are well-kinded and can have the same kind. But one is a TyConApp and one is an AppTy. (Actually, looking at this, perhaps the magic will be in mkAppTy, not splitTyConApp.) But I have to look closer.

This ticket serves as a reminder to do so.

Change History (5)

comment:1 Changed 16 months ago by goldfire

Owner: set to goldfire

comment:2 Changed 15 months ago by goldfire

One wrinkle (at least until #11715 is fixed): which eqType do we wish to respect here? eqType or tcEqType? I think it might be best to wait until after #11715. Or it's possible that it doesn't matter which eqType we're thinking of.

comment:3 Changed 7 months ago by bgamari


This won't happen for 8.4.

comment:4 Changed 5 months ago by bgamari

Milestone: 8.6.1

Removing milestone as there is no one actively working on this.

comment:5 Changed 5 months ago by simonpj

Keywords: TypeInType added
Note: See TracTickets for help on using tickets.