Opened 3 years ago

Last modified 21 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 3 years ago by goldfire

Owner: set to goldfire

comment:2 Changed 3 years 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 23 months ago by bgamari


This won't happen for 8.4.

comment:4 Changed 21 months ago by bgamari

Milestone: 8.6.1

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

comment:5 Changed 21 months ago by simonpj

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