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,
data Sigma (s :: Type) :: (s ~> Type) -> Type
s in s :: Type is a kind variable of Type kind-kind and this kind has to be passed explicitly when you use Sigma. And in its kind signature,
Sigma :: forall s -> (s ~> *) -> *
forall s means s is a visible kind. It means you need to pass it explicitly when you say it's visible. You can read it as Sigma is a type constructor taking a kind s and a type of kind s ~> Type, and returning a type of kind Type.
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.