`forall {..}` in GHC 9

Question

This is valid syntax in GHC 9. What do the {..} mean (as distinct from (..) which GHC 8.10 requires here)?

ign :: forall {f :: Type -> Type} {p}. Applicative f => p -> f ()
ign _ = pure ()

Answer 1

See 6.4.14.1. Inferred vs. specified type variables:

Since the 9.0.1 release, GHC permits labelling the user-written type or kind variables as inferred, in contrast to the default of specified. By writing the type variable binder in braces as {tyvar} or {tyvar :: kind}, the new variable will be classified as inferred, not specified.

• .. is a specified type
• {..} is an inferred type

forall a. and forall {a}. are invisible quantifiers that GHC will instantiate automatically by unification.

const :: forall a b. a -> b -> a
const a _ = a

This means const True EQ instantiates a (@Bool) and b (@Ordering) without the users help.

If the user wants to explicitly instantiate them they can "override their visibility", using visible type applications. That's why they are specified types. (although "specifiable" might be a more accurate terminology)

>> :set -XTypeApplications
>> :t const @Bool @Ordering True EQ
const @Bool @Ordering True EQ :: Bool

If for some reason we only want to specify b (without summoning the "snail squad": @_, umm "partial type signatures") we can make a an inferred type. Then the first type is dropped

const2 :: forall {a} b. a -> b -> a
const2 a _ = a

>> :t const2 @Ordering True EQ
const2 @Ordering True EQ :: Bool

For your example it means ghc must infer the type of f and p. You cannot write ign @IO @Int.

---

This becomes more useful when you have kind polymorphism. If you define

-- MkApply @Type @[] @Int :: [Int] -> Apply @Type [] Int
-- MkApply @_    @[] @Int :: [Int] -> Apply @Type [] Int
type    Apply :: forall (k :: Type). (k -> Type) -> (k -> Type)
newtype Apply f a where
  MkApply :: forall (k :: Type) (f :: k -> Type) (a :: k). f a -> Apply @k f a

you must specify the kind k when instantiating MkApply @Type @[] @Int but this kind is implied by both [] and Int. You might prefer marking k as inferred in MkApply so you can write MkApply @[] @Int

-- MkApply @[] @Int :: [Int] -> Apply @Type [] Int
type    Apply :: forall (k :: Type). (k -> Type) -> (k -> Type)
newtype Apply f a where
  MkApply :: forall {k :: Type} (f :: k -> Type) (a :: k). f a -> Apply @k f a