What does the `forall a -> b` syntax mean?

March 20, 2022

In GHCi, the kind of FUN is displayed like this:

λ> :k FUN
FUN :: forall (n :: Multiplicity) -> * -> * -> *

At first, I thought this was a roundabout way of saying

FUN :: Multiplicity -> * -> * -> *

but it turns out Template Haskell has a separate constructor for this form: ForallVisT. I can’t find any documentation on it, and I have no idea how to even begin experimenting with it in a meaningful way.

What does this syntax mean? How does forall a -> b differ from a "normal" forall a. a -> b?

>Solution :

forall a -> _ is used when the result type depends on an explicit argument.

-- type NonDep :: Type -> Type; argument is explicit
data NonDep (x :: Type) :: Type
-- type ImpDep :: forall a. Maybe a -> Type; first argument is implicit and dependent
data ImpDep (x :: Maybe a) :: Type
-- so if you want an explicit and dependent argument...
-- type ExpDep :: forall (a :: Type) -> Maybe a -> Type
data ExpDep (a :: Type) (x :: Maybe a) :: Type

It is odd that FUN‘s type has forall (m :: Multiplicity) -> and not Multiplicity -> as the following arguments (two implicit RuntimeReps and two TYPEs) do not depend on it, but such is the weirdness that surrounds GHC primitives.