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.fapplied to two parameters, - it means thatf :: Type -> Type -> Type.But then
f ais used as a list element -[f a]- and list elements must beType, which means thatf a :: Type, which means thatf :: Type -> Type.Mismatch.
fooworks because types can be partially applied. That is, iff :: Type -> Type -> Type, thenf a :: Type -> Type. And then, typetis allowed to have a parameter of kindType -> Type, so everything matches.To reiterate the above:
fooworks because typetmay have a parameter of kindType -> Type.bardoesn't work, because type[](aka "list") must have a parameter of kindType.