This is probably a silly question but I cannot figure out the underlying rules for the following behavior:
foo :: t (f a) -> f a b -- accepted
foo = undefined
bar :: t [f a] -> f a b -- rejected
bar = undefined
It makes perfect sense that f applied to a and a b respectively in bar leads to a kind error and is thus rejected. But why is foo accepted?
It's the kind of f.
Since the return type is f a b - i.e. f applied to two parameters, - it means that f :: Type -> Type -> Type.
But then f a is used as a list element - [f a] - and list elements must be Type, which means that f a :: Type, which means that f :: Type -> Type.
Mismatch.
foo works because types can be partially applied. That is, if f :: Type -> Type -> Type, then f a :: Type -> Type. And then, type t is allowed to have a parameter of kind Type -> Type, so everything matches.
To reiterate the above:
foo works because type t may have a parameter of kind Type -> Type.bar doesn't work, because type [] (aka "list") must have a parameter of kind Type.