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?

CodePudding user response：

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.