In singletons-2.6, Sigma
is defined as
data Sigma (s :: Type) :: (s ~> Type) -> Type
and GHC 8.8.4 tells that its kind is
> :k Sigma
Sigma :: forall s -> (s ~> *) -> *
So what is this forall
in this kind signature?
Apparently, it's different from
data Sigma :: forall s. Type -> (s ~> Type) -> Type
in which case its kind is, of course,
Sigma :: * -> (s ~> *) -> *
Also, it seems different from
data Sigma :: f s -> (s ~> *) -> *
It seems to me that the promoted kind of the type variable s
in s :: Type
is unified with the kind variable s
in (s ~> Type) -> Type
, but does it what happens? I have a feeling that I'm missing something very basic.
I tried finding any documents describing this, but I had no luck.
Now, I got some ideas from dependent haskell in GHC Wiki.
We can now pass a kind to a type constructor just like we can pass a type to a data constructor (we still need to pass a singleton instead of a type itself though).
In this declaration of
Sigma
,s
ins :: Type
is a kind variable ofType
kind-kind and this kind has to be passed explicitly when you useSigma
. And in its kind signature,forall s
meanss
is a visible kind. It means you need to pass it explicitly when you say it's visible. You can read it asSigma
is a type constructor taking a kinds
and a type of kinds ~> Type
, and returning a type of kindType
.You cannot write this type signature directly in GHC 8.8.4, but you can write it using
StandaloneKindSignatures
in GHC 8.10.1.Update (2021/9/30):
It's called Visible Dependent Quantification. You can find a good explanation about it at Visible dependent quantification in Haskell.