So I've been thinking of a type system extension: partial type family application. If we look at the type system used by modern GHC, in it, type family application is very distinct from constructor/constraint application: it is somewhat opaque in the sense that a type family must always appear fully applied. As such, it doesn't make sense to talk about a type family's kind, if we have: type family Id (a :: *) :: * where Id x = x then saying that 'Id :: * -> *' would be wrong, because Id cannot be used interchangeably with things that are truly of kind * -> *, such as Maybe or []. The reason for the "fully applied" restriction is that if we allowed partially applied type functions, then their equality would be undecidable. Still, I think, in a lot of cases we could benefit from partially applied type functions, even without extensional equality. Writing type level list folds, filters, zips, you name it. As stated above, we can't add the proposition 'Id :: * -> *' to our type system, so, what if, instead, we added a different kind of arrow kind for type families? I like the look of (~>), so 'Id :: * ~> *'. (~>) :: * -> * -> * This rule of inference, similar to the usual, would supersede all the type family kinding rules: f :: k ~> l, x :: k ------------------- f x :: l As such, the juxtaposition operator would very clearly have two different "kinds": (k -> l) --> k --> l and (k ~> l) --> k --> l, and there is no N-ary "type family application" operator. In order for the type checker to not fall apart, we need to have at least intesional (structural) equality on (~>), which we can have because it is decidable. We could then write stuff like type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs)