* A ForAllTy (used for both types and kinds) contains a ForAllTyBinder.
Each ForAllTyBinder
Bndr a tvis
is equipped with tvis::ForAllTyFlag, which says whether or not arguments
for this binder should be visible (explicit) in source Haskell.
* A TyCon contains a list of TyConBinders. Each TyConBinder
Bndr a cvis
is equipped with cvis::TyConBndrVis, which says whether or not type
and kind arguments for this TyCon should be visible (explicit) in
source Haskell.
This table summarises the visibility rules:
| Occurrences look like this
| GHC displays type as in Haskell source code
|--------------------------------------------------------------------------------------
| Bndr a tvis :: ForAllTyBinder, in the binder of ForAllTy for a term
| tvis :: ForAllTyFlag
| tvis = Inferred: f :: forall {a}. type Arg not allowed: f
f :: forall {co}. type Arg not allowed: f
| tvis = Specified: f :: forall a. type Arg optional: f or f @Int
| tvis = Required: f :: forall k -> type Arg required: f (type Int)
|
| Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon
| cvis :: TyConBndrVis
| cvis = AnonTCB: T :: kind -> kind Required: T *
| cvis = NamedTCB Inferred: T :: forall {k}. kind Arg not allowed: T
| T :: forall {co}. kind Arg not allowed: T
| cvis = NamedTCB Specified: T :: forall k. kind Arg not allowed[1]: T
| cvis = NamedTCB Required: T :: forall k -> kind Required: T *
[1] In types, in the Specified case, it would make sense to allow
optional kind applications, thus (T @*), but we have not
yet implemented that
In term declarations ----
* Inferred. Function defn, with no signature: f1 x = x
We infer f1 :: forall {a}. a -> a, with 'a' Inferred
It's Inferred because it doesn't appear in any
user-written signature for f1
* Specified. Function defn, with signature (implicit forall):
f2 :: a -> a; f2 x = x
So f2 gets the type f2 :: forall a. a -> a, with 'a' Specified
even though 'a' is not bound in the source code by an explicit forall
* Specified. Function defn, with signature (explicit forall):
f3 :: forall a. a -> a; f3 x = x
So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified
* Required. Function defn, with signature (explicit forall):
f4 :: forall a -> a -> a; f4 (type _) x = x
So f4 gets the type f4 :: forall a -> a -> a, with 'a' Required
This is the experimental RequiredTypeArguments extension,
see GHC Proposal #281 "Visible forall in types of terms"
* Inferred. Function defn, with signature (explicit forall), marked as inferred:
f5 :: forall {a}. a -> a; f5 x = x
So f5 gets the type f5 :: forall {a}. a -> a, with 'a' Inferred
It's Inferred because the user marked it as such, even though it does appear
in the user-written signature for f5
* Inferred/Specified. Function signature with inferred kind polymorphism.
f6 :: a b -> Int
So 'f6' gets the type f6 :: forall {k} (a :: k -> Type) (b :: k). a b -> Int
Here 'k' is Inferred (it's not mentioned in the type),
but 'a' and 'b' are Specified.
* Specified. Function signature with explicit kind polymorphism
f7 :: a (b :: k) -> Int
This time 'k' is Specified, because it is mentioned explicitly,
so we get f7 :: forall (k :: Type) (a :: k -> Type) (b :: k). a b -> Int
* Similarly pattern synonyms:
Inferred - from inferred types (e.g. no pattern type signature)
- or from inferred kind polymorphism
In type declarations ----
* Inferred (k)
data T1 a b = MkT1 (a b)
Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> *
The kind variable 'k' is Inferred, since it is not mentioned
Note that 'a' and 'b' correspond to /Anon/ PiTyBinders in T1's kind,
and Anon binders don't have a visibility flag. (Or you could think
of Anon having an implicit Required flag.)
* Specified (k)
data T2 (a::k->*) b = MkT (a b)
Here T's kind is T :: forall (k:*). (k->*) -> k -> *
The kind variable 'k' is Specified, since it is mentioned in
the signature.
* Required (k)
data T k (a::k->*) b = MkT (a b)
Here T's kind is T :: forall k:* -> (k->*) -> k -> *
The kind is Required, since it bound in a positional way in T's declaration
Every use of T must be explicitly applied to a kind
* Inferred (k1), Specified (k)
data T a b (c :: k) = MkT (a b) (Proxy c)
Here T's kind is T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
So 'k' is Specified, because it appears explicitly,
but 'k1' is Inferred, because it does not
Generally, in the list of TyConBinders for a TyCon,
* Inferred arguments always come first
* Specified, Anon and Required can be mixed
e.g.
data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where ...
Here Foo's TyConBinders are
[Required 'a', Specified 'b', Anon]
and its kind prints as
Foo :: forall a -> forall b. (a -> b -> Type) -> Type
See also Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
Printing -----
We print forall types with enough syntax to tell you their visibility
flag. But this is not source Haskell, and these types may not all
be parsable.
Specified: a list of Specified binders is written between `forall` and `.`:
const :: forall a b. a -> b -> a
Inferred: like Specified, but every binder is written in braces:
f :: forall {k} (a :: k). S k a -> Int
Required: binders are put between `forall` and `->`:
T :: forall k -> *
Other points -----
* In classic Haskell, all named binders (that is, the type variables in
a polymorphic function type f :: forall a. a -> a) have been Inferred.
* Inferred variables correspond to "generalized" variables from the
Visible Type Applications paper (ESOP'16).