`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 ()

Delaware

It looks like it's an inferred type variable that can not be applied using ign @MyF @MyP: downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/… – Intention

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

Collative

Broadly speaking, I think kind variables should be inferred when possible. This is the opposite of the default, which is unfortunate. For example, GHC.Generics.Generic1 takes a specified kind argument, so to1 and from1 do as well. Horrible user experience. – Fulmar

I agree with that, it blocked me from making Category kind polymorphic with a specified kind (type Category :: forall ob. Cat ob -> Constraint). This would have changed the quantification of ob in the methods from inferred to specified so you had to write id @Type @(->) @Int :: Int -> Int. There was no way to specify {ob} as inferred in the methods if it is specified in the kind. I don't like this state of affairs, when I added Generically1 I had to use GADT syntax and quantify all the variables in the Generically1 :: forall {k} f a. f a -> Generically1 @k f a constructor as well – Collative

I'm not sure it's unreasonable for the class specification to match the method specification. I do think it's unreasonable to have to write from1 @_ @Identity or whatever – Fulmar

I'm not sure what the best default is but there was no way to override it for the methods! I don't know if this has changed; there was a proposal for a top-level method signature where you could write id :: forall {ob :: Type} (cat :: Cat ob) (a :: ob) :: Category @ob cat => cat a a. I don't like duplicating the signature outside of the class declaration but at least it allows finetuning it! – Collative

Ah, now I understand you. You want to specify an uninferable kind argument for the class, but avoid specifying that same, now inferable, argument to the method. Makes sense. – Fulmar

Yes and a similar thing might happen with visibility (in the future). sizeOf :: forall a. Sizeable a => a -> Int doesn't actually use the a argument so it can be supplied with sizeOf (undefined :: A). If the argument is removed we can specify it with type application sizeOf :: forall a. Sizeable a => Int but it makes more sense to use visible quantification: forall a -> Sizeable a => Int. But even with forall-> how would you visibly quantify over a method? The type argument of a class is already implicitly quantified outside of the scope of a method. Idk. – Collative

It makes me wonder if forall {a} -> .. would be allowed? Presumably not – Collative