This simple code doesn't compile
import Data.Kind
type family F (k :: Type) :: (t :: k) -> Type
The error message is
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘(t :: k) -> Type’
I get in some sense that this actually defines a "family of type families" but I don't really understand why this limitation would exist.
type family F (k :: Type) (t :: k) :: Type
does work but it doesn't have the same semantics and can't be used the same.
There is no need to name t
in the resulting type. You can can simply use
type family F (k :: Type) :: k -> Type