6.4.14. Visible type application¶

TypeApplications
¶ Since: 8.0.1 Allow the use of type application syntax.
The TypeApplications
extension allows you to use
visible type application in expressions. Here is an
example: show (read @Int "5")
. The @Int
is the visible type application; it specifies the value of the type variable
in read
‘s type.
A visible type application is preceded with an @
sign. (To disambiguate the syntax, the @
must be
preceded with a nonidentifier letter, usually a space. For example,
read@Int 5
would not parse.) It can be used whenever
the full polymorphic type of the function is known. If the function
is an identifier (the common case), its type is considered known only when
the identifier has been given a type signature. If the identifier does
not have a type signature, visible type application cannot be used.
GHC also permits visible kind application, where users can declare the kind arguments to be instantiated in kindpolymorphic cases. Its usage parallels visible type application in the term level, as specified above.
6.4.14.1. Inferred vs. specified type variables¶
GHC tracks a distinction between what we call inferred and specified type variables. Only specified type variables are available for instantiation with visible type application. An example illustrates this well:
f :: (Eq b, Eq a) => a > b > Bool
f x y = (x == x) && (y == y)
g x y = (x == x) && (y == y)
The functions f
and g
have the same body, but only f
is given
a type signature. When GHC is figuring out how to process a visible type application,
it must know what variable to instantiate. It thus must be able to provide
an ordering to the type variables in a function’s type.
If the user has supplied a type signature, as in f
, then this is easy:
we just take the ordering from the type signature, going left to right and
using the first occurrence of a variable to choose its position within the
ordering. Thus, the variables in f
will be b
, then a
.
In contrast, there is no reliable way to do this for g
; we will not know
whether Eq a
or Eq b
will be listed first in the constraint in g
‘s
type. In order to have visible type application be robust between releases of
GHC, we thus forbid its use with g
.
We say that the type variables in f
are specified, while those in
g
are inferred. The general rule is this: if the user has written
a type variable in the source program, it is specified; if not, it is
inferred.
This rule applies in datatype declarations, too. For example, if we have
data Proxy a = Proxy
(and PolyKinds
is enabled), then
a
will be assigned kind k
, where k
is a fresh kind variable.
Because k
was not written by the user, it will be unavailable for
type application in the type of the constructor Proxy
; only the a
will be available.
When fprintexplicitforalls
is enabled, inferred variables
are printed in braces. Thus, the type of the data constructor Proxy
from the previous example would be forall {k} (a :: k). Proxy a
.
We can observe this behavior in a GHCi session:
> :set XTypeApplications fprintexplicitforalls
> let myLength1 :: Foldable f => f a > Int; myLength1 = length
> :type +v myLength1
myLength1 :: forall (f :: * > *) a. Foldable f => f a > Int
> let myLength2 = length
> :type +v myLength2
myLength2 :: forall {a} {t :: * > *}. Foldable t => t a > Int
> :type +v myLength2 @[]
<interactive>:1:1: error:
• Cannot apply expression of type ‘t0 a0 > Int’
to a visible type argument ‘[]’
• In the expression: myLength2 @[]
Notice that since myLength1
was defined with an explicit type signature,
:type +v
reports that all of its type variables are available
for type application. On the other hand, myLength2
was not given a type
signature. As a result, all of its type variables are surrounded with braces,
and trying to use visible type application with myLength2
fails.
Also note the use of :type +v
in the GHCi session above instead
of :type
. This is because :type
gives you the type
that would be inferred for a variable assigned to the expression provided
(that is, the type of x
in let x = <expr>
). As we saw above with
myLength2
, this type will have no variables available to visible type
application. On the other hand, :type +v
gives you the actual
type of the expression provided. To illustrate this:
> :type myLength1
myLength1 :: forall {a} {f :: * > *}. Foldable f => f a > Int
> :type myLength2
myLength2 :: forall {a} {t :: * > *}. Foldable t => t a > Int
Using :type
might lead one to conclude that none of the type
variables in myLength1
‘s type signature are available for type
application. This isn’t true, however! Be sure to use :type +v
if you want the most accurate information with respect to visible type
application properties.
6.4.14.2. Ordering of specified variables¶
In the simple case of the previous section, we can say that specified variables appear in lefttoright order. However, not all cases are so simple. Here are the rules in the subtler cases:
If an identifier’s type has a
forall
, then the order of type variables as written in theforall
is retained.If any of the variables depend on other variables (that is, if some of the variables are kind variables), the variables are reordered so that kind variables come before type variables, preserving the lefttoright order as much as possible. That is, GHC performs a stable topological sort on the variables. Example:
h :: Proxy (a :: (j, k)) > Proxy (b :: Proxy a) > ()  as if h :: forall j k a b. ...
In this example,
a
depends onj
andk
, andb
depends ona
. Even thougha
appears lexically beforej
andk
,j
andk
are quantified first, becausea
depends onj
andk
. Note further thatj
andk
are not reordered with respect to each other, even though doing so would not violate dependency conditions.A “stable topological sort” here, we mean that we perform this algorithm (which we call ScopedSort):
 Work lefttoright through the input list of type variables, with a cursor.
 If variable
v
at the cursor is depended on by any earlier variablew
, movev
immediately before the leftmost suchw
.
Class methods’ type arguments include the class type variables, followed by any variables an individual method is polymorphic in. So,
class Monad m where return :: a > m a
means thatreturn
‘s type arguments arem, a
.With the
RankNTypes
extension (Lexically scoped type variables), it is possible to declare type arguments somewhere other than the beginning of a type. For example, we can havepair :: forall a. a > forall b. b > (a, b)
and then saypair @Bool True @Char
which would have typeChar > (Bool, Char)
.Partial type signatures (Partial Type Signatures) work nicely with visible type application. If you want to specify only the second type argument to
wurble
, then you can saywurble @_ @Int
. The first argument is a wildcard, just like in a partial type signature. However, if used in a visible type application/visible kind application, it is not necessary to specifyPartialTypeSignatures
and your code will not generate a warning informing you of the omitted type.
The section in this manual on kind polymorphism describes how variables in type and class declarations are ordered (Inferring the order of variables in a type/class declaration).