Type family forcing parameter to have the kind *

2
votes

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.

1
haskelltype-familiestype-kinds
Aren't things on the right side of the :: for a type family kinds? So the first one (would) say "kind t has sort k" while the second one says "type t has kind k"? – David Young
With TypeInType it's all the same. – Luka Horvat
Perhaps type family F (k :: Type) :: k -> Type is closer to what you want? – chi
@chi Wow, of course. I have no idea why I over complicated that so much. – Luka Horvat
Type families are not real 'functions'. The 2nd type family does not have type (k :: Type) -> (t :: k) -> Type. In fact, it has no type which can be currently expressed in Haskell. The first type family is invalid because (->) :: Type -> Type -> Type but you've explicitly declared t :: k and k (a fresh type variable) doesn't unify with Type. (t :: Type) -> Type would be completely valid (and is equivalent to the type in the accepted answer). – user2407038

1 Answers

3
votes

There is no need to name t in the resulting type. You can can simply use

type family F (k :: Type) :: k -> Type