Implement KPush in types
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
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
splitTyConApp.) But I have to look closer.
This ticket serves as a reminder to do so.