XGitUrl: http://git.haskell.org/ghc.git/blobdiff_plain/5edb18a962cbfee0ff869b1a77ebf2cd79dd8ef5..ae7d1ff62f61e2ded772d4c58cda3c130bbdcf78:/docs/users_guide/glasgow_exts.rst
diff git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 4125c33..eae0283 100644
 a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ 148,24 +148,25 @@ stores a pointer. GHC currently does not support this variety of ``Just``
nodes (nor for any other datatype). Accordingly, the *kind* of an unboxed
type is different from the kind of a boxed type.
The Haskell Report describes that ``*`` is the kind of ordinary datatypes,
such as ``Int``. Furthermore, type constructors can have kinds with arrows;
for example, ``Maybe`` has kind ``* > *``. Unboxed types have a kind that
specifies their runtime representation. For example, the type ``Int#`` has
kind ``TYPE 'IntRep`` and ``Double#`` has kind ``TYPE 'DoubleRep``. These
kinds say that the runtime representation of an ``Int#`` is a machine integer,
and the runtime representation of a ``Double#`` is a machine doubleprecision
floating point. In contrast, the kind ``*`` is actually just a synonym
for ``TYPE 'PtrRepLifted``. More details of the ``TYPE`` mechanisms appear in
the `section on runtime representation polymorphism <#runtimerep>`__.

Given that ``Int#``'s kind is not ``*``, it then it follows that
``Maybe Int#`` is disallowed. Similarly, because type variables tend
to be of kind ``*`` (for example, in ``(.) :: (b > c) > (a > b) > a > c``,
all the type variables have kind ``*``), polymorphism tends not to work
over primitive types. Stepping back, this makes some sense, because
a polymorphic function needs to manipulate the pointers to its data,
and most primitive types are unboxed.
+The Haskell Report describes that ``*`` (spelled ``Type`` and imported from
+``Data.Kind`` in the GHC dialect of Haskell) is the kind of ordinary datatypes,
+such as ``Int``. Furthermore, type constructors can have kinds with arrows; for
+example, ``Maybe`` has kind ``Type > Type``. Unboxed types have a kind that
+specifies their runtime representation. For example, the type ``Int#`` has kind
+``TYPE 'IntRep`` and ``Double#`` has kind ``TYPE 'DoubleRep``. These kinds say
+that the runtime representation of an ``Int#`` is a machine integer, and the
+runtime representation of a ``Double#`` is a machine doubleprecision floating
+point. In contrast, the kind ``Type`` is actually just a synonym for ``TYPE
+'LiftedRep``. More details of the ``TYPE`` mechanisms appear in the `section
+on runtime representation polymorphism <#runtimerep>`__.
+
+Given that ``Int#``'s kind is not ``Type``, it then it follows that ``Maybe
+Int#`` is disallowed. Similarly, because type variables tend to be of kind
+``Type`` (for example, in ``(.) :: (b > c) > (a > b) > a > c``, all the
+type variables have kind ``Type``), polymorphism tends not to work over
+primitive types. Stepping back, this makes some sense, because a polymorphic
+function needs to manipulate the pointers to its data, and most primitive types
+are unboxed.
There are some restrictions on the use of primitive types:
@@ 284,21 +285,21 @@ for an unboxed sum type with N alternatives is ::
(# t_1  t_2  ...  t_N #)
where `t_1` ... `t_N` are types (which can be unlifted, including unboxed tuple
and sums).
+where ``t_1`` ... ``t_N`` are types (which can be unlifted, including unboxed
+tuples and sums).
Unboxed tuples can be used for multiarity alternatives. For example: ::
(# (# Int, String #)  Bool #)
Term level syntax is similar. Leading and preceding bars (``) indicate which
alternative it is. Here is two terms of the type shown above: ::
+The term level syntax is similar. Leading and preceding bars (``) indicate which
+alternative it is. Here are two terms of the type shown above: ::
(# (# 1, "foo" #)  #)  first alternative
(#  True #)  second alternative
Pattern syntax reflects the term syntax: ::
+The pattern syntax reflects the term syntax: ::
case x of
(# (# i, str #)  #) > ...
@@ 307,45 +308,56 @@ Pattern syntax reflects the term syntax: ::
Unboxed sums are "unboxed" in the sense that, instead of allocating sums in the
heap and representing values as pointers, unboxed sums are represented as their
components, just like unboxed tuples. These "components" depend on alternatives
of a sum type. Code generator tries to generate as compact layout as possible.
In the best case, size of an unboxed sum is size of its biggest alternative +
one word (for tag). The algorithm for generating memory layout for a sum type
works like this:
+of a sum type. Like unboxed tuples, unboxed sums are lazy in their lifted
+components.
+
+The code generator tries to generate as compact layout as possible for each
+unboxed sum. In the best case, size of an unboxed sum is size of its biggest
+alternative plus one word (for a tag). The algorithm for generating the memory
+layout for a sum type works like this:
 All types are classified as one of these classes: 32bit word, 64bit word,
32bit float, 64bit float, pointer.
 For each alternative of the sum type, a layout that consists of these fields
 is generated. For example, if an alternative has `Int`, `Float#` and `String`
 fields, the layout will have an 32bit word, 32bit float and pointer fields.
+ is generated. For example, if an alternative has ``Int``, ``Float#`` and
+ ``String`` fields, the layout will have an 32bit word, 32bit float and
+ pointer fields.
 Layout fields are then overlapped so that the final layout will be as compact
 as possible. E.g. say two alternatives have these fields: ::
+ as possible. For example, suppose we have the unboxed sum: ::
 Word32, String, Float#
 Float#, Float#, Maybe Int
+ (# (# Word32#, String, Float# #)
+  (# Float#, Float#, Maybe Int #) #)
 Final layout will be something like ::
+ The final layout will be something like ::
Int32, Float32, Float32, Word32, Pointer
 First `Int32` is for the tag. It has two `Float32` fields because floating
 point types can't overlap with other types, because of limitations of the code
 generator that we're hoping to overcome in the future, and second alternative
 needs two `Float32` fields. `Word32` field is for the `Word32` in the first
 alternative. `Pointer` field is shared between `String` and `Maybe Int` values
 of the alternatives.

 In the case of enumeration types (like `Bool`), the unboxed sum layout only
 has an `Int32` field (i.e. the whole thing is represented by an integer).
+ The first ``Int32`` is for the tag. There are two ``Float32`` fields because
+ floating point types can't overlap with other types, because of limitations of
+ the code generator that we're hoping to overcome in the future. The second
+ alternative needs two ``Float32`` fields: The ``Word32`` field is for the
+ ``Word32#`` in the first alternative. The ``Pointer`` field is shared between
+ ``String`` and ``Maybe Int`` values of the alternatives.
In the example above, a value of this type is thus represented as 5 values. As
an another example, this is the layout for unboxed version of `Maybe a` type: ::
+ As another example, this is the layout for the unboxed version of ``Maybe a``
+ type, ``(# (# #)  a #)``: ::
Int32, Pointer
The `Pointer` field is not used when tag says that it's `Nothing`. Otherwise
`Pointer` points to the value in `Just`.
+ The ``Pointer`` field is not used when tag says that it's ``Nothing``.
+ Otherwise ``Pointer`` points to the value in ``Just``. As mentioned
+ above, this type is lazy in its lifted field. Therefore, the type ::
+
+ data Maybe' a = Maybe' (# (# #)  a #)
+
+ is *precisely* isomorphic to the type ``Maybe a``, although its memory
+ representation is different.
+
+ In the degenerate case where all the alternatives have zero width, such
+ as the ``Bool``like ``(# (# #)  (# #) #)``, the unboxed sum layout only
+ has an ``Int32`` tag field (i.e., the whole thing is represented by an integer).
.. _syntaxextns:
@@ 514,11 +526,8 @@ instance, the binary integer literal ``0b11001001`` will be desugared into
Hexadecimal floating point literals

.. ghcflag:: XHexFloatLiterals
+.. extension:: HexFloatLiterals
:shortdesc: Enable support for :ref:`hexadecimal floating point literals `.
 :type: dynamic
 :reverse: XNoHexFloatLIterals
 :category:
:since: 8.4.1
@@ 531,7 +540,7 @@ corresponds closely to the underlying bitencoding of the number.
In this notation floating point numbers are written using hexadecimal digits,
and so the digits are interpreted using base 16, rather then the usual 10.
This means that digits left of the decimal point correspond to positive
powers of 16, while the ones to the right correspond to negaitve ones.
+powers of 16, while the ones to the right correspond to negative ones.
You may also write an explicit exponent, which is similar to the exponent
in decimal notation with the following differences:
@@ 553,6 +562,94 @@ by one bit left (negative) or right (positive). Here are some examples:
+.. _numericunderscores:
+
+Numeric underscores
+
+
+.. extension:: NumericUnderscores
+ :shortdesc: Enable support for :ref:`numeric underscores `.
+
+ :since: 8.6.1
+
+ Allow the use of underscores in numeric literals.
+
+GHC allows for numeric literals to be given in decimal, octal, hexadecimal,
+binary, or float notation.
+
+The language extension :extension:`NumericUnderscores` adds support for expressing
+underscores in numeric literals.
+For instance, the numeric literal ``1_000_000`` will be parsed into
+``1000000`` when :extension:`NumericUnderscores` is enabled.
+That is, underscores in numeric literals are ignored when
+:extension:`NumericUnderscores` is enabled.
+See also :ghcticket:`14473`.
+
+For example:
+
+.. codeblock:: none
+
+  decimal
+ million = 1_000_000
+ billion = 1_000_000_000
+ lightspeed = 299_792_458
+ version = 8_04_1
+ date = 2017_12_31
+
+  hexadecimal
+ red_mask = 0xff_00_00
+ size1G = 0x3fff_ffff
+
+  binary
+ bit8th = 0b01_0000_0000
+ packbits = 0b1_11_01_0000_0_111
+ bigbits = 0b1100_1011__1110_1111__0101_0011
+
+  float
+ pi = 3.141_592_653_589_793
+ faraday = 96_485.332_89
+ avogadro = 6.022_140_857e+23
+
+  function
+ isUnderMillion = (< 1_000_000)
+
+ clip64M x
+  x > 0x3ff_ffff = 0x3ff_ffff
+  otherwise = x
+
+ test8bit x = (0b01_0000_0000 .&. x) /= 0
+
+About validity:
+
+.. codeblock:: none
+
+ x0 = 1_000_000  valid
+ x1 = 1__000000  valid
+ x2 = 1000000_  invalid
+ x3 = _1000000  invalid
+
+ e0 = 0.0001  valid
+ e1 = 0.000_1  valid
+ e2 = 0_.0001  invalid
+ e3 = _0.0001  invalid
+ e4 = 0._0001  invalid
+ e5 = 0.0001_  invalid
+
+ f0 = 1e+23  valid
+ f1 = 1_e+23  valid
+ f2 = 1__e+23  valid
+ f3 = 1e_+23  invalid
+
+ g0 = 1e+23  valid
+ g1 = 1e+_23  invalid
+ g2 = 1e+23_  invalid
+
+ h0 = 0xffff  valid
+ h1 = 0xff_ff  valid
+ h2 = 0x_ffff  valid
+ h3 = 0x__ffff  valid
+ h4 = _0xffff  invalid
+
.. _patternguards:
Pattern guards
@@ 646,7 +743,7 @@ follows:
view pattern expression are in scope. For example: ::
example :: Maybe ((String > Integer,Integer), String) > Bool
 example Just ((f,_), f > 4) = True
+ example (Just ((f,_), f > 4)) = True
Additionally, in function definitions, variables bound by matching
earlier curried arguments may be used in view pattern expressions
@@ 1136,7 +1233,6 @@ Parallel List Comprehensions
.. extension:: ParallelListComp
:shortdesc: Enable parallel list comprehensions.
 Implied by :extension:`ParallelArrays`.
:since: 6.8.1
@@ 1500,14 +1596,13 @@ New monadic failure desugaring mechanism
when desugaring refutable patterns in ``do`` blocks.
The ``XMonadFailDesugaring`` extension switches the desugaring of
``do``blocks to use ``MonadFail.fail`` instead of ``Monad.fail``. This will
eventually be the default behaviour in a future GHC release, under the
+``do``blocks to use ``MonadFail.fail`` instead of ``Monad.fail``.
+
+This extension is enabled by default since GHC 8.6.1, under the
`MonadFail Proposal (MFP)
`__.
This extension is temporary, and will be deprecated in a future release. It is
included so that library authors have a hard check for whether their code
will work with future GHC versions.
+This extension is temporary, and will be deprecated in a future release.
.. _rebindablesyntax:
@@ 1547,9 +1642,12 @@ not the Prelude versions:
 An integer literal ``368`` means "``fromInteger (368::Integer)``",
rather than "``Prelude.fromInteger (368::Integer)``".
 Fractional literals are handed in just the same way, except that the
+ Fractional literals are handled in just the same way, except that the
translation is ``fromRational (3.68::Rational)``.
+ String literals are also handled the same way, except that the
+ translation is ``fromString ("368"::String)``.
+
 The equality test in an overloaded numeric pattern uses whatever
``(==)`` is in scope.
@@ 2011,6 +2109,104 @@ data constructor in an import or export list with the keyword
``pattern``, to allow the import or export of a data constructor without
its parent type constructor (see :ref:`patsynimpexp`).
+.. _blockarguments:
+
+More liberal syntax for function arguments
+
+
+.. extension:: BlockArguments
+ :shortdesc: Allow ``do`` blocks and other constructs as function arguments.
+
+ :since: 8.6.1
+
+ Allow ``do`` expressions, lambda expressions, etc. to be directly used as
+ a function argument.
+
+In Haskell 2010, certain kinds of expressions can be used without parentheses
+as an argument to an operator, but not as an argument to a function.
+They include ``do``, lambda, ``if``, ``case``, and ``let``
+expressions. Some GHC extensions also define language constructs of this type:
+``mdo`` (:ref:`recursivedonotation`), ``\case`` (:ref:`lambdacase`), and
+``proc`` (:ref:`arrownotation`).
+
+The :extension:`BlockArguments` extension allows these constructs to be directly
+used as a function argument. For example::
+
+ when (x > 0) do
+ print x
+ exitFailure
+
+will be parsed as::
+
+ when (x > 0) (do
+ print x
+ exitFailure)
+
+and
+
+::
+
+ withForeignPtr fptr \ptr > c_memcpy buf ptr size
+
+will be parsed as::
+
+ withForeignPtr fptr (\ptr > c_memcpy buf ptr size)
+
+Changes to the grammar
+~~~~~~~~~~~~~~~~~~~~~~
+
+The Haskell report `defines
+`_
+the ``lexp`` nonterminal thus (``*`` indicates a rule of interest)::
+
+ lexp â \ apat1 â¦ apatn > exp (lambda abstraction, n â¥ 1) *
+  let decls in exp (let expression) *
+  if exp [;] then exp [;] else exp (conditional) *
+  case exp of { alts } (case expression) *
+  do { stmts } (do expression) *
+  fexp
+
+ fexp â [fexp] aexp (function application)
+
+ aexp â qvar (variable)
+  gcon (general constructor)
+  literal
+  ( exp ) (parenthesized expression)
+  qcon { fbind1 â¦ fbindn } (labeled construction)
+  aexp { fbind1 â¦ fbindn } (labelled update)
+  â¦
+
+The :extension:`BlockArguments` extension moves these production rules under
+``aexp``::
+
+ lexp â fexp
+
+ fexp â [fexp] aexp (function application)
+
+ aexp â qvar (variable)
+  gcon (general constructor)
+  literal
+  ( exp ) (parenthesized expression)
+  qcon { fbind1 â¦ fbindn } (labeled construction)
+  aexp { fbind1 â¦ fbindn } (labelled update)
+  \ apat1 â¦ apatn > exp (lambda abstraction, n â¥ 1) *
+  let decls in exp (let expression) *
+  if exp [;] then exp [;] else exp (conditional) *
+  case exp of { alts } (case expression) *
+  do { stmts } (do expression) *
+  â¦
+
+Now the ``lexp`` nonterminal is redundant and can be dropped from the grammar.
+
+Note that this change relies on an existing metarule to resolve ambiguities:
+
+ The grammar is ambiguous regarding the extent of lambda abstractions, let
+ expressions, and conditionals. The ambiguity is resolved by the metarule
+ that each of these constructs extends as far to the right as possible.
+
+For example, ``f \a > a b`` will be parsed as ``f (\a > a b)``, not as ``f
+(\a > a) b``.
+
.. _syntaxstolen:
Summary of stolen syntax
@@ 2040,9 +2236,10 @@ The following syntax is stolen:
.. index::
single: forall
 Stolen (in types) by: :extension:`ExplicitForAll`, and hence by
 :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
 :extension:`RankNTypes`, :extension:`ExistentialQuantification`
+ Stolen (in types) by default (see :ref:`infelicitieslexical`). ``forall`` is
+ a reserved keyword and never a type variable, in accordance with `GHC Proposal #43
+ `__.
+
``mdo``
.. index::
@@ 2101,6 +2298,9 @@ The following syntax is stolen:
``pattern``
Stolen by: :extension:`PatternSynonyms`
+``static``
+ Stolen by: :extension:`StaticPointers`
+
.. _datatypeextensions:
Extensions to data types and type synonyms
@@ 2118,15 +2318,23 @@ Data types with no constructors
Allow definition of empty ``data`` types.
With the :extension:`EmptyDataDecls` extension, GHC
lets you declare a data type with no constructors. For example: ::
+With the :extension:`EmptyDataDecls` extension, GHC lets you declare a
+data type with no constructors.
+
+You only need to enable this extension if the language you're using
+is Haskell 98, in which a data type must have at least one constructor.
+Haskell 2010 relaxed this rule to allow data types with no constructors,
+and thus :extension:`EmptyDataDecls` is enabled by default when the
+language is Haskell 2010.
 data S  S :: *
 data T a  T :: * > *
+For example: ::
+
+ data S  S :: Type
+ data T a  T :: Type > Type
Syntactically, the declaration lacks the "= constrs" part. The type can
be parameterised over types of any kind, but if the kind is not ``*``
then an explicit kind annotation must be used (see :ref:`kinding`).
+Syntactically, the declaration lacks the "= constrs" part. The type can be
+parameterised over types of any kind, but if the kind is not ``Type`` then an
+explicit kind annotation must be used (see :ref:`kinding`).
Such data types have only one value, namely bottom. Nevertheless, they
can be useful when defining "phantom types".
@@ 2205,8 +2413,7 @@ specifically:
sets the fixity for both type constructor ``T`` and data constructor
``T``, and similarly for ``:*:``. ``Int `a` Bool``.
 Function arrow is ``infixr`` with fixity 0 (this might change; it's
 not clear what it should be).
+ The function arrow ``>`` is ``infixr`` with fixity 1.
.. _typeoperators:
@@ 2755,16 +2962,16 @@ type declarations.
in the "``data Set a where``" header have no scope. Indeed, one can
write a kind signature instead: ::
 data Set :: * > * where ...
+ data Set :: Type > Type where ...
or even a mixture of the two: ::
 data Bar a :: (* > *) > * where ...
+ data Bar a :: (Type > Type) > Type where ...
The type variables (if given) may be explicitly kinded, so we could
also write the header for ``Foo`` like this: ::
 data Bar a (b :: * > *) where ...
+ data Bar a (b :: Type > Type) where ...
 You can use strictness annotations, in the obvious places in the
constructor type: ::
@@ 3022,8 +3229,6 @@ Record field disambiguation
:since: 6.8.1
 :since: 6.8.1

Allow the compiler to automatically choose between identicallynamed
record selectors based on type (if the choice is unambiguous).
@@ 3356,10 +3561,10 @@ More details:
module M where
data R = R { a,b,c :: Int }
module X where
 import M( R(a,c) )
 f b = R { .. }
+ import M( R(R,a,c) )
+ f a b = R { .. }
 The ``R{..}`` expands to ``R{M.a=a}``, omitting ``b`` since the
+ The ``R{..}`` expands to ``R{a=a}``, omitting ``b`` since the
record field is not in scope, and omitting ``c`` since the variable
``c`` is not in scope (apart from the binding of the record selector
``c``, of course).
@@ 3588,7 +3793,7 @@ GHC extends this mechanism along several axes:
* In Haskell 98, the only derivable classes are ``Eq``,
``Ord``, ``Enum``, ``Ix``, ``Bounded``, ``Read``, and ``Show``. `Various
 langauge extensions <#derivingextra>`__ extend this list.
+ language extensions <#derivingextra>`__ extend this list.
* Besides the stock approach to deriving instances by generating all method
definitions, GHC supports two additional deriving strategies, which can
@@ 3712,11 +3917,21 @@ number of important ways:
module as the data type declaration. (But be aware of the dangers of
orphan instances (:ref:`orphanmodules`).
 You must supply an explicit context (in the example the context is
 ``(Eq a)``), exactly as you would in an ordinary instance
+ In most cases, you must supply an explicit context (in the example the
+ context is ``(Eq a)``), exactly as you would in an ordinary instance
declaration. (In contrast, in a ``deriving`` clause attached to a
data type declaration, the context is inferred.)
+ The exception to this rule is that the context of a standalone deriving
+ declaration can infer its context when a single, extrawildcards constraint
+ is used as the context, such as in: ::
+
+ deriving instance _ => Eq (Foo a)
+
+ This is essentially the same as if you had written ``deriving Foo`` after
+ the declaration for ``data Foo a``. Using this feature requires the use of
+ :extension:`PartialTypeSignatures` (:ref:`partialtypesignatures`).
+
 Unlike a ``deriving`` declaration attached to a ``data`` declaration,
the instance can be more specific than the data type (assuming you
also use :extension:`FlexibleInstances`, :ref:`instancerules`). Consider
@@ 3847,7 +4062,7 @@ Deriving ``Functor`` instances
With :extension:`DeriveFunctor`, one can derive ``Functor`` instances for data types
of kind ``* > *``. For example, this declaration::
+of kind ``Type > Type``. For example, this declaration::
data Example a = Ex a Char (Example a) (Example Char)
deriving Functor
@@ 3903,7 +4118,7 @@ causes the generated code to be illtyped.
As a general rule, if a data type has a derived ``Functor`` instance and its
last type parameter occurs on the righthand side of the data declaration, then
either it must (1) occur bare (e.g., ``newtype Id a = a``), or (2) occur as the
+either it must (1) occur bare (e.g., ``newtype Id a = Id a``), or (2) occur as the
last argument of a type constructor (as in ``Right`` above).
There are two exceptions to this rule:
@@ 3923,7 +4138,7 @@ There are two exceptions to this rule:
That is, :extension:`DeriveFunctor` patternmatches its way into tuples and maps
over each type that constitutes the tuple. The generated code is
 reminiscient of what would be generated from
+ reminiscent of what would be generated from
``data Triple a = Triple a Int [a]``, except with extra machinery to handle
the tuple.
@@ 4040,7 +4255,7 @@ Deriving ``Foldable`` instances
Allow automatic deriving of instances for the ``Foldable`` typeclass.
With :extension:`DeriveFoldable`, one can derive ``Foldable`` instances for data types
of kind ``* > *``. For example, this declaration::
+of kind ``Type > Type``. For example, this declaration::
data Example a = Ex a Char (Example a) (Example Char)
deriving Foldable
@@ 4159,7 +4374,7 @@ There are some other differences regarding what data types can have derived
polymorphic types that are syntactically equivalent to the last type
parameter. In particular:
  We don't fold over the arguments of ``E1`` or ``E4`` beacause even though
+  We don't fold over the arguments of ``E1`` or ``E4`` because even though
``(a ~ Int)``, ``Int`` is not syntactically equivalent to ``a``.
 We don't fold over the argument of ``E3`` because ``a`` is not universally
@@ 4182,7 +4397,7 @@ Deriving ``Traversable`` instances
Allow automatic deriving of instances for the ``Traversable`` typeclass.
With :extension:`DeriveTraversable`, one can derive ``Traversable`` instances for data
types of kind ``* > *``. For example, this declaration::
+types of kind ``Type > Type``. For example, this declaration::
data Example a = Ex a Char (Example a) (Example Char)
deriving (Functor, Foldable, Traversable)
@@ 4253,7 +4468,7 @@ Deriving ``Data`` instances
.. extension:: DeriveDataTypeable
:shortdesc: Enable deriving for the Data class.
 Implied by :extension:`AutoDeriveTypeable`.
+ Implied by (deprecated) :extension:`AutoDeriveTypeable`.
:since: 6.8.1
@@ 4308,7 +4523,7 @@ Deriving ``Lift`` instances
.. extension:: DeriveLift
:shortdesc: Enable deriving for the Lift class
 :since: 7.2.1
+ :since: 8.0.1
Enable automatic deriving of instances for the ``Lift`` typeclass for
Template Haskell.
@@ 4390,7 +4605,7 @@ Generalised derived instances for newtypes
GeneralizedNewtypeDeriving
:shortdesc: Enable newtype deriving.
 :since: 6.8.1
+ :since: 6.8.1. British spelling since 8.6.1.
Enable GHC's cunning generalised deriving mechanism for ``newtype``\s
@@ 4414,6 +4629,9 @@ It is particularly galling that, since the constructor doesn't appear at
runtime, this instance declaration defines a dictionary which is
*wholly equivalent* to the ``Int`` dictionary, only slower!
+:extension:`DerivingVia` (see :ref:`derivingvia`) is a generalization of
+this idea.
+
.. _generalizednewtypederiving:
Generalising the deriving clause
@@ 4466,7 +4684,7 @@ In this case the derived instance declaration is of the form ::
instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
Notice that, since ``Monad`` is a constructor class, the instance is a
*partial application* of the new type, not the entire left hand side. We
+*partial application* of the newtype, not the entire left hand side. We
can imagine that the type declaration is "etaconverted" to generate the
context of the instance declaration.
@@ 4494,6 +4712,43 @@ declarations are treated uniformly (and implemented just by reusing the
dictionary for the representation type), *except* ``Show`` and ``Read``,
which really behave differently for the newtype and its representation.
+.. note::
+
+ It is sometimes necessary to enable additional language extensions when
+ deriving instances via :extension:`GeneralizedNewtypeDeriving`. For instance,
+ consider a simple class and instance using :extension:`UnboxedTuples`
+ syntax: ::
+
+ {# LANGUAGE UnboxedTuples #}
+
+ module Lib where
+
+ class AClass a where
+ aMethod :: a > (# Int, a #)
+
+ instance AClass Int where
+ aMethod x = (# x, x #)
+
+ The following will fail with an "Illegal unboxed tuple" error, since the
+ derived instance produced by the compiler makes use of unboxed tuple syntax,
+ ::
+
+ {# LANGUAGE GeneralizedNewtypeDeriving #}
+
+ import Lib
+
+ newtype Int' = Int' Int
+ deriving (AClass)
+
+ However, enabling the :extension:`UnboxedTuples` extension allows the module
+ to compile. Similar errors may occur with a variety of extensions,
+ including:
+
+ * :extension:`UnboxedTuples`
+ * :extension:`PolyKinds`
+ * :extension:`MultiParamTypeClasses`
+ * :extension:`FlexibleContexts`
+
.. _precisegndspecification:
A more precise specification
@@ 4704,6 +4959,11 @@ isn't sophisticated enough to determine this, so you'll need to enable
you do go down this route, make sure you can convince yourself that all of
the type family instances you're deriving will eventually terminate if used!
+Note that :extension:`DerivingVia` (see :ref:`derivingvia`) uses essentially
+the same specification to derive instances of associated type families as well
+(except that it uses the ``via`` type instead of the underlying ``reptype``
+of a newtype).
+
.. _deriveanyclass:
Deriving any other class
@@ 4907,10 +5167,12 @@ Currently, the deriving strategies are:
 ``stock``: Have GHC implement a "standard" instance for a data type,
if possible (e.g., ``Eq``, ``Ord``, ``Generic``, ``Data``, ``Functor``, etc.)
 ``anyclass``: Use :extension:`DeriveAnyClass`
+ ``anyclass``: Use :extension:`DeriveAnyClass` (see :ref:`deriveanyclass`)
 ``newtype``: Use :extension:`GeneralizedNewtypeDeriving`
+ (see :ref:`newtypederiving`)
+ ``via``: Use :extension:`DerivingVia` (see :ref:`derivingvia`)
.. _defaultderivingstrategy:
@@ 4944,6 +5206,118 @@ In that case, GHC chooses the strategy as follows:
user is warned about the ambiguity. The warning can be avoided by explicitly
stating the desired deriving strategy.
+.. _derivingvia:
+
+Deriving via
+
+
+.. extension:: DerivingVia
+ :shortdesc: Enable deriving instances ``via`` types of the same runtime
+ representation.
+ Implies :extension:`DerivingStrategies`.
+
+ :implies: :extension:`DerivingStrategies`
+
+ :since: 8.6.1
+
+This allows ``deriving`` a class instance for a type by specifying
+another type of equal runtime representation (such that there exists a
+``Coercible`` instance between the two: see :ref:`coercible`) that is
+already an instance of the that class.
+
+:extension:`DerivingVia` is indicated by the use of the ``via``
+deriving strategy. ``via`` requires specifying another type (the ``via`` type)
+to ``coerce`` through. For example, this code: ::
+
+ {# LANGUAGE DerivingVia #}
+
+ import Numeric
+
+ newtype Hex a = Hex a
+
+ instance (Integral a, Show a) => Show (Hex a) where
+ show (Hex a) = "0x" ++ showHex a ""
+
+ newtype Unicode = U Int
+ deriving Show
+ via (Hex Int)
+
+  >>> euroSign
+  0x20ac
+ euroSign :: Unicode
+ euroSign = U 0x20ac
+
+Generates the following instance ::
+
+ instance Show Unicode where
+ show :: Unicode > String
+ show = Data.Coerce.coerce
+ @(Hex Int > String)
+ @(Unicode > String)
+ show
+
+This extension generalizes :extension:`GeneralizedNewtypeDeriving`. To
+derive ``Num Unicode`` with GND (``deriving newtype Num``) it must
+reuse the ``Num Int`` instance. With ``DerivingVia``, we can explicitly
+specify the representation type ``Int``: ::
+
+ newtype Unicode = U Int
+ deriving Num
+ via Int
+
+ deriving Show
+ via (Hex Int)
+
+ euroSign :: Unicode
+ euroSign = 0x20ac
+
+Code duplication is common in instance declarations. A familiar
+pattern is lifting operations over an ``Applicative`` functor.
+Instead of having catchall instances for ``f a`` which overlap
+with all other such instances, like so: ::
+
+ instance (Applicative f, Semigroup a) => Semigroup (f a) ..
+ instance (Applicative f, Monoid a) => Monoid (f a) ..
+
+We can instead create a newtype ``App``
+(where ``App f a`` and ``f a`` are represented the same in memory)
+and use :extension:`DerivingVia` to explicitly enable uses of this
+pattern: ::
+
+ {# LANGUAGE DerivingVia, DeriveFunctor, GeneralizedNewtypeDeriving #}
+
+ import Control.Applicative
+
+ newtype App f a = App (f a) deriving newtype (Functor, Applicative)
+
+ instance (Applicative f, Semigroup a) => Semigroup (App f a) where
+ (<>) = liftA2 (<>)
+
+ instance (Applicative f, Monoid a) => Monoid (App f a) where
+ mempty = pure mempty
+
+ data Pair a = MkPair a a
+ deriving stock
+ Functor
+
+ deriving (Semigroup, Monoid)
+ via (App Pair a)
+
+ instance Applicative Pair where
+ pure a = MkPair a a
+
+ MkPair f g <*> MkPair a b = MkPair (f a) (g b)
+
+Note that the ``via`` type does not have to be a ``newtype``.
+The only restriction is that it is coercible with the
+original data type. This means there can be arbitrary nesting of newtypes,
+as in the following example: ::
+
+ newtype Kleisli m a b = (a > m b)
+ deriving (Semigroup, Monoid)
+ via (a > App m b)
+
+Here we make use of the ``Monoid ((>) a)`` instance.
.. _patternsynonyms:
@@ 4959,7 +5333,7 @@ Pattern synonyms
Pattern synonyms are enabled by the language extension :extension:`PatternSynonyms`, which is
required for defining them, but *not* for using them. More information and
examples of view patterns can be found on the `Wiki page `.
+examples of pattern synonyms can be found on the :ghcwiki:`Wiki page `.
Pattern synonyms enable giving names to parametrized pattern schemes.
They can also be thought of as abstract constructors that don't have a
@@ 5076,6 +5450,37 @@ pattern synonym: ::
pattern StrictJust a < Just !a where
StrictJust !a = Just a
+Constructing an explicitly bidirectional pattern synonym also:
+
+ can create different data constructors from the underlying data type,
+ not just the one appearing in the pattern match;
+
+ can call any functions or conditional logic, especially validation,
+ of course providing it constructs a result of the right type;
+
+ can use guards on the lhs of the ``=``;
+
+ can have multiple equations.
+
+For example: ::
+
+ data PosNeg = Pos Int  Neg Int
+ pattern Smarter{ nonneg } < Pos nonneg where
+ Smarter x = if x >= 0 then (Pos x) else (Neg x)
+
+Or using guards: ::
+
+ pattern Smarter{ nonneg } < Pos nonneg where
+ Smarter x  x >= 0 = (Pos x)
+  otherwise = (Neg x)
+
+There is an extensive Haskell folk art of `smart constructors
+`_,
+essentially functions that wrap validation around a constructor,
+and avoid exposing its representation.
+The downside is that the underlying constructor can't be used as a matcher.
+Pattern synonyms can be used as genuinely smart constructors, for both validation and matching.
+
The table below summarises where each kind of pattern synonym can be used.
+++++
@@ 5149,7 +5554,7 @@ the syntax for bidirectional pattern synonyms is: ::
and the syntax for explicitly bidirectional pattern synonyms is: ::
pattern pat_lhs < pat where
 pat_lhs = expr
+ pat_lhs = expr  lhs restricted, see below
We can define either prefix, infix or record pattern synonyms by modifying
the form of `pat_lhs`. The syntax for these is as follows:
@@ 5163,6 +5568,9 @@ Infix ``arg1 `Name` arg2``
Record ``Name{arg1,arg2,...,argn}``
======= ============================
+The `pat_lhs` for explicitly bidirectional construction cannot use Record syntax.
+(Because the rhs *expr* might be constructing different data constructors.)
+It can use guards with multiple equations.
Pattern synonym declarations can only occur in the top level of a
module. In particular, they are not allowed as local definitions.
@@ 5329,7 +5737,7 @@ Note also the following points
pattern P x y v < MkT True x y (v::a)
Here the universal type variable `a` scopes over the definition of `P`,
 but the existential `b` does not. (c.f. disussion on Trac #14998.)
+ but the existential `b` does not. (c.f. discussion on Trac #14998.)
 For a bidirectional pattern synonym, a use of the pattern synonym as
an expression has the type
@@ 5390,6 +5798,24 @@ Matching of pattern synonyms
A pattern synonym occurrence in a pattern is evaluated by first matching
against the pattern synonym itself, and then on the argument patterns.
+
+More precisely, the semantics of pattern matching is given in
+`Section 3.17 of the Haskell 2010 report `__. To the informal semantics in Section 3.17.2 we add this extra rule:
+
+* If the pattern is a constructor pattern ``(P p1 ... pn)``, where ``P`` is
+ a pattern synonym defined by ``P x1 ... xn = p`` or ``P x1 ... xn < p``, then:
+
+ (a) Match the value ``v`` against ``p``. If this match fails or diverges,
+ so does the whole (pattern synonym) match. Otherwise the match
+ against ``p`` must bind the variables ``x1 ... xn``; let them be bound to values ``v1 ... vn``.
+
+ (b) Match ``v1`` against ``p1``, ``v2`` against ``p2`` and so on.
+ If any of these matches fail or diverge, so does the whole match.
+
+ (c) If all the matches against the ``pi`` succeed, the match succeeds,
+ binding the variables bound by the ``pi`` . (The ``xi`` are not
+ bound; they remain local to the pattern synonym declaration.)
+
For example, in the following program, ``f`` and ``f'`` are equivalent: ::
pattern Pair x y < [x, y]
@@ 5454,8 +5880,7 @@ The superclasses of a class declaration
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
.. extension:: FlexibleContexts
 :shortdesc: Enable flexible contexts. Implied by
 :extension:`ImplicitParams`.
+ :shortdesc: Enable flexible contexts.
:since: 6.8.1
@@ 5939,9 +6364,9 @@ original definition of ``Collects`` with a simple dependency: ::
The dependency ``ce > e`` here specifies that the type ``e`` of elements is
uniquely determined by the type of the collection ``ce``. Note that both
parameters of Collects are of kind ``*``; there are no constructor classes
here. Note too that all of the instances of ``Collects`` that we gave
earlier can be used together with this new definition.
+parameters of Collects are of kind ``Type``; there are no constructor classes
+here. Note too that all of the instances of ``Collects`` that we gave earlier
+can be used together with this new definition.
What about the ambiguity problems that we encountered with the original
definition? The empty function still has type ``Collects e ce => ce``, but
@@ 6039,7 +6464,6 @@ Relaxed rules for the instance head
.. extension:: FlexibleInstances
:shortdesc: Enable flexible instances.
Implies :extension:`TypeSynonymInstances`.
 Implied by :extension:`ImplicitParams`.
:implies: :extension:`TypeSynonymInstances`
:since: 6.8.1
@@ 6370,9 +6794,12 @@ like this:
target constraint is a substitution instance of :math:`I`. These instance
declarations are the *candidates*.
 Eliminate any candidate :math:`IX` for which both of the following hold:
+ If no candidates remain, the search failes
  There is another candidate :math:`IY` that is strictly more specific; that
+ Eliminate any candidate :math:`IX` for which there is another candidate
+ :math:`IY` such that both of the following hold:
+
+  :math:`IY` is strictly more specific than :math:`IX`. That
is, :math:`IY` is a substitution instance of :math:`IX` but not vice versa.
 Either :math:`IX` is *overlappable*, or :math:`IY` is *overlapping*. (This
@@ 6380,19 +6807,20 @@ like this:
client to deliberately override an instance from a library,
without requiring a change to the library.)
 If exactly one nonincoherent candidate remains, select it. If all
 remaining candidates are incoherent, select an arbitrary one.
 Otherwise the search fails (i.e. when more than one surviving
 candidate is not incoherent).
+ If all the remaining candidates are incoherent, the search suceeds, returning
+ an arbitrary surviving candidate.
+
+ If more than one nonincoherent candidate remains, the search fails.
 If the selected candidate (from the previous step) is incoherent, the
 search succeeds, returning that candidate.
+ Otherwise there is exactly one nonincoherent candidate; call it the
+ "prime candidate".
 If not, find all instances that *unify* with the target constraint,
+ Now find all instances, or inscope given constraints, that *unify* with
+ the target constraint,
but do not *match* it. Such noncandidate instances might match when
the target constraint is further instantiated. If all of them are
 incoherent, the search succeeds, returning the selected candidate; if
 not, the search fails.
+ incoherent toplevel instances, the search succeeds, returning the prime candidate.
+ Otherwise the search fails.
Notice that these rules are not influenced by flag settings in the
client module, where the instances are *used*. These rules make it
@@ 6434,15 +6862,16 @@ former is a substitution instance of the latter. For example (D) is
"more specific" than (C) because you can get from (C) to (D) by
substituting ``a := Int``.
GHC is conservative about committing to an overlapping instance. For
example: ::
+The final bullet (about unifiying instances)
+makes GHC conservative about committing to an
+overlapping instance. For example: ::
f :: [b] > [b]
f x = ...
Suppose that from the RHS of ``f`` we get the constraint ``C b [b]``.
But GHC does not commit to instance (C), because in a particular call of
``f``, ``b`` might be instantiate to ``Int``, in which case instance (D)
+``f``, ``b`` might be instantiated to ``Int``, in which case instance (D)
would be more specific still. So GHC rejects the program.
If, however, you enable the extension :extension:`IncoherentInstances` when compiling
@@ 6483,6 +6912,23 @@ declaration, thus: ::
(You need :extension:`FlexibleInstances` to do this.)
+In the unification check in the final bullet, GHC also uses the
+"inscope given constraints". Consider for example ::
+
+ instance C a Int
+
+ g :: forall b c. C b Int => blah
+ g = ...needs (C c Int)...
+
+Here GHC will not solve the constraint ``(C c Int)`` from the
+toplevel instance, because a particular call of ``g`` might
+instantiate both ``b`` and ``c`` to the same type, which would
+allow the constraint to be solved in a different way. This latter
+restriction is principally to make the constraintsolver complete.
+(Interested folk can read ``Note [Instance and Given overlap]`` in ``TcInteract``.)
+It is easy to avoid: in a type signature avoid a constraint that
+matches a toplevel instance. The flag :ghcflag:`Wsimplifiableclassconstraints` warns about such signatures.
+
.. warning::
Overlapping instances must be used with care. They can give
rise to incoherence (i.e. different instance choices are made in
@@ 6626,7 +7072,7 @@ usual: ::
The class ``IsString`` is not in scope by default. If you want to
mention it explicitly (for example, to give an instance declaration for
it), you can import it from module ``GHC.Exts``.
+it), you can import it from module ``Data.String``.
Haskell's defaulting mechanism (`Haskell Report, Section
4.3.4 `__) is
@@ 6654,7 +7100,7 @@ A small example:
module Main where
 import GHC.Exts( IsString(..) )
+ import Data.String( IsString(..) )
newtype MyString = MyString String deriving (Eq, Show)
instance IsString MyString where
@@ 6685,7 +7131,7 @@ Overloaded labels
GHC supports *overloaded labels*, a form of identifier whose interpretation may
depend both on its type and on its literal text. When the
:extension:`OverloadedLabels` extension is enabled, an overloaded label can written
+:extension:`OverloadedLabels` extension is enabled, an overloaded label can be written
with a prefix hash, for example ``#foo``. The type of this expression is
``IsLabel "foo" a => a``.
@@ 6982,7 +7428,7 @@ example (Trac #10318) ::
Fractional (Frac a),
IntegralDomain (Frac a))
=> IntegralDomain a where
 type Frac a :: *
+ type Frac a :: Type
Here the superclass cycle does terminate but it's not entirely straightforward
to see that it does.
@@ 7088,11 +7534,11 @@ Data family declarations
Indexed data families are introduced by a signature, such as ::
 data family GMap k :: * > *
+ data family GMap k :: Type > Type
The special ``family`` distinguishes family from standard data
declarations. The result kind annotation is optional and, as usual,
defaults to ``*`` if omitted. An example is ::
+defaults to ``Type`` if omitted. An example is ::
data family Array e
@@ 7100,12 +7546,12 @@ Named arguments can also be given explicit kind signatures if needed.
Just as with :ref:`GADT declarations ` named arguments are
entirely optional, so that we can declare ``Array`` alternatively with ::
 data family Array :: * > *
+ data family Array :: Type > Type
Unlike with ordinary data definitions, the result kind of a data family
does not need to be ``*``: it can alternatively be a kind variable
+does not need to be ``Type``: it can alternatively be a kind variable
(with :extension:`PolyKinds`). Data instances' kinds must end in
``*``, however.
+``Type``, however.
.. _datainstancedeclarations:
@@ 7128,6 +7574,17 @@ instance for ``GMap`` is ::
In this example, the declaration has only one variant. In general, it
can be any number.
+When :extension:`ExplicitForAll` is enabled, type or kind variables used on
+the left hand side can be explicitly bound. For example: ::
+
+ data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool
+
+When an explicit ``forall`` is present, all *type* variables mentioned which
+are not already in scope must be bound by the ``forall``. Kind variables will
+be implicitly bound if necessary, for example: ::
+
+ data instance forall (a :: k). F a = FOtherwise
+
When the flag :ghcflag:`Wunusedtypepatterns` is enabled, type
variables that are mentioned in the patterns on the left hand side, but not
used on the right hand side are reported. Variables that occur multiple times
@@ 7141,6 +7598,9 @@ This resembles the wildcards that can be used in
No error messages reporting the inferred types are generated, nor does
the extension :extension:`PartialTypeSignatures` have any effect.
+A type or kind variable explicitly bound using :extension:`ExplicitForAll` but
+not used on the left hand side will generate an error, not a warning.
+
Data and newtype instance declarations are only permitted when an
appropriate family declaration is in scope  just as a class instance
declaration requires the class declaration to be visible. Moreover, each
@@ 7232,11 +7692,11 @@ Type family declarations
Open indexed type families are introduced by a signature, such as ::
 type family Elem c :: *
+ type family Elem c :: Type
The special ``family`` distinguishes family from standard type
declarations. The result kind annotation is optional and, as usual,
defaults to ``*`` if omitted. An example is ::
+defaults to ``Type`` if omitted. An example is ::
type family Elem c
@@ 7249,18 +7709,19 @@ determine a family's arity, and hence in general, also insufficient to
determine whether a type family application is well formed. As an
example, consider the following declaration: ::
 type family F a b :: * > *  F's arity is 2,
  although its overall kind is * > * > * > *
+ type family F a b :: Type > Type
+  F's arity is 2,
+  although its overall kind is Type > Type > Type > Type
Given this declaration the following are examples of wellformed and
malformed types: ::
 F Char [Int]  OK! Kind: * > *
 F Char [Int] Bool  OK! Kind: *
+ F Char [Int]  OK! Kind: Type > Type
+ F Char [Int] Bool  OK! Kind: Type
F IO Bool  WRONG: kind mismatch in the first argument
F Bool  WRONG: unsaturated application
The result kind annotation is optional and defaults to ``*`` (like
+The result kind annotation is optional and defaults to ``Type`` (like
argument kinds) if omitted. Polykinded type families can be declared
using a parameter in the kind annotation: ::
@@ 7292,6 +7753,10 @@ with underscores to avoid warnings when the
:ghcflag:`Wunusedtypepatterns` flag is enabled. The same rules apply
as for :ref:`datainstancedeclarations`.
+Also in the same way as :ref:`datainstancedeclarations`, when
+:extension:`ExplicitForAll` is enabled, type and kind variables can be
+explicilty bound in a type instance declaration.
+
Type family instance declarations are only legitimate when an
appropriate family declaration is in scope  just like class instances
require the class declaration to be visible. Moreover, each instance
@@ 7326,8 +7791,14 @@ Note that GHC must be sure that ``a`` cannot unify with ``Int`` or
their code, GHC will not be able to simplify the type. After all, ``a``
might later be instantiated with ``Int``.
A closed type family's equations have the same restrictions as the
equations for open type family instances.
+A closed type family's equations have the same restrictions and extensions as
+the equations for open type family instances. For instance, when
+:extension:`ExplicitForAll` is enabled, type or kind variables used on the
+left hand side of an equation can be explicitly bound, such as in: ::
+
+ type family R a where
+ forall t a. R (t a) = [a]
+ forall a. R a = a
A closed type family may be declared with no equations. Such closed type
families are opaque typelevel definitions that will never reduce, are
@@ 7344,7 +7815,7 @@ Type family examples
Here are some examples of admissible and illegal type instances: ::
 type family F a :: *
+ type family F a :: Type
type instance F [Int] = Int  OK!
type instance F String = Char  OK!
type instance F (F a) = a  WRONG: type parameter mentions a type family
@@ 7359,7 +7830,7 @@ Here are some examples of admissible and illegal type instances: ::
type instance H Char = Char  WRONG: cannot have instances of closed family
type family K a where  OK!
 type family G a b :: * > *
+ type family G a b :: Type > Type
type instance G Int = (,)  WRONG: must be two type parameters
type instance G Int Char Float = Double  WRONG: must be two type parameters
@@ 7410,8 +7881,8 @@ like types. For example, the following is accepted: ::
type instance J Int = Bool
type instance J Int = Maybe
These instances are compatible because they differ in their implicit
kind parameter; the first uses ``*`` while the second uses ``* > *``.
+These instances are compatible because they differ in their implicit kind
+parameter; the first uses ``Type`` while the second uses ``Type > Type``.
The definition for "compatible" uses a notion of "apart", whose
definition in turn relies on type family reduction. This condition of
@@ 7503,11 +7974,11 @@ When the name of a type argument of a data or type instance
declaration doesn't matter, it can be replaced with an underscore
(``_``). This is the same as writing a type variable with a unique name. ::
 data family F a b :: *
+ data family F a b :: Type
data instance F Int _ = Int
 Equivalent to data instance F Int b = Int
 type family T a :: *
+ type family T a :: Type
type instance T (a,_) = a
 Equivalent to type instance T (a,b) = a
@@ 7534,11 +8005,11 @@ A data or type synonym family can be declared as part of a type class,
thus: ::
class GMapKey k where
 data GMap k :: * > *
+ data GMap k :: Type > Type
...
class Collects ce where
 type Elem ce :: *
+ type Elem ce :: Type
...
When doing so, we (optionally) may drop the "``family``" keyword.
@@ 7550,12 +8021,12 @@ may be omitted and they may be in an order other than in the class head.
Hence, the following contrived example is admissible: ::
class C a b c where
 type T c a x :: *
+ type T c a x :: Type
Here ``c`` and ``a`` are class parameters, but the type is also indexed
on a third parameter ``x``.
.. _assocdatainst:
+.. _associnst:
Associated instances
~~~~~~~~~~~~~~~~~~~~
@@ 7572,12 +8043,12 @@ keyword in the family instance: ::
type Elem [e] = e
...
The data or type family instance for an assocated type must follow
+The data or type family instance for an associated type must follow
the rule that the type indexes corresponding to class parameters must have
precisely the same as type given in the instance head. For example: ::
class Collects ce where
 type Elem ce :: *
+ type Elem ce :: Type
instance Eq (Elem [e]) => Collects [e] where
 Choose one of the following alternatives:
@@ 7598,17 +8069,17 @@ Note the following points:
to mention kind variables that are implicitly bound. For example, these are
legitimate: ::
 data family Nat :: k > k > *
+ data family Nat :: k > k > Type
 k is implicitly bound by an invisible kind pattern
 newtype instance Nat :: (k > *) > (k > *) > * where
+ newtype instance Nat :: (k > Type) > (k > Type) > Type where
Nat :: (forall xx. f xx > g xx) > Nat f g
class Funct f where
 type Codomain f :: *
+ type Codomain f :: Type
instance Funct ('KProxy :: KProxy o) where
 o is implicitly bound by the kind signature
 of the LHS type pattern ('KProxy)
 type Codomain 'KProxy = NatTr (Proxy :: o > *)
+ type Codomain 'KProxy = NatTr (Proxy :: o > Type)
 The instance for an associated type can be omitted in class
instances. In that case, unless there is a default instance (see
@@ 7629,7 +8100,16 @@ Note the following points:
parameter is ``[v]``, and one for which it is ``Int``. Since you
cannot give any *subsequent* instances for ``(GMap Flob ...)``, this
facility is most useful when the free indexed parameter is of a kind
 with a finite number of alternatives (unlike ``*``).
+ with a finite number of alternatives (unlike ``Type``).
+
+ When :extension:`ExplicitForAll` is enabled, type and kind variables can be
+ explicily bound in associated data or type family instances in the same way
+ (and with the same restrictions) as :ref:`datainstancedeclarations` or
+ :ref:`typeinstancedeclarations`. For example, adapting the above, the
+ following is accepted: ::
+
+ instance Eq (Elem [e]) => Collects [e] where
+ type forall e. Elem [e] = e
.. _assocdecldefs:
@@ 7667,6 +8147,10 @@ Note the following points:
is relaxed for *kind* variables, however, as the right hand side is allowed
to mention kind variables that are implicitly bound on the left hand side.
+ Because of this, unlike :ref:`associnst`, explicit binding of type/kind
+ variables in default declarations is not permitted by
+ :extension:`ExplicitForAll`.
+
 Unlike the associated type family declaration itself, the type variables of
the default instance are independent of those of the parent class.
@@ 7674,8 +8158,8 @@ Here are some examples:
::
 class C (a :: *) where
 type F1 a :: *
+ class C (a :: Type) where
+ type F1 a :: Type
type instance F1 a = [a]  OK
type instance F1 a = a>a  BAD; only one default instance is allowed
@@ 7810,7 +8294,7 @@ Recall our running ``GMapKey`` class example:
::
class GMapKey k where
 data GMap k :: * > *
+ data GMap k :: Type > Type
insert :: GMap k v > k > v > GMap k v
lookup :: GMap k v > k > Maybe v
empty :: GMap k v
@@ 8106,7 +8590,7 @@ Motivation
Standard Haskell has a rich type language. Types classify terms and
serve to avoid many common programming mistakes. The kind language,
however, is relatively simple, distinguishing only regular types (kind
``*``) and type constructors (e.g. kind ``* > * > *``).
+``Type``) and type constructors (e.g. kind ``Type > Type > Type``).
In particular when using advanced type
system features, such as type families (:ref:`typefamilies`) or GADTs
(:ref:`gadt`), this simple kind system is insufficient, and fails to
@@ 8116,11 +8600,11 @@ numbers, and lengthindexed vectors: ::
data Ze
data Su n
 data Vec :: * > * > * where
+ data Vec :: Type > Type > Type where
Nil :: Vec a Ze
Cons :: a > Vec a n > Vec a (Su n)
The kind of ``Vec`` is ``* > * > *``. This means that, e.g.,
+The kind of ``Vec`` is ``Type > Type > Type``. This means that, e.g.,
``Vec Int Char`` is a wellkinded type, even though this is not what we
intend when defining lengthindexed vectors.
@@ 8128,7 +8612,7 @@ With :extension:`DataKinds`, the example above can then be rewritten to: ::
data Nat = Ze  Su Nat
 data Vec :: * > Nat > * where
+ data Vec :: Type > Nat > Type where
Nil :: Vec a 'Ze
Cons :: a > Vec a n > Vec a ('Su n)
@@ 8153,48 +8637,39 @@ following types ::
give rise to the following kinds and type constructors (where promoted
constructors are prefixed by a tick ``'``): ::
 Nat :: *
+ Nat :: Type
'Zero :: Nat
'Succ :: Nat > Nat
 List :: * > *
+ List :: Type > Type
'Nil :: forall k. List k
'Cons :: forall k. k > List k > List k
 Pair :: * > * > *
+ Pair :: Type > Type > Type
'Pair :: forall k1 k2. k1 > k2 > Pair k1 k2
 Sum :: * > * > *
+ Sum :: Type > Type > Type
'L :: k1 > Sum k1 k2
'R :: k2 > Sum k1 k2
The following restrictions apply to promotion:

 We promote ``data`` types and ``newtypes``; type synonyms and
 type/data families are not promoted (:ref:`typefamilies`).

 We only promote types whose kinds are of the form
 ``* > ... > * > *``. In particular, we do not promote
 higherkinded datatypes such as ``data Fix f = In (f (Fix f))``, or
 datatypes whose kinds involve promoted types such as
 ``Vec :: * > Nat > *``.

 We do not promote data constructors that are kind polymorphic,
 involve constraints, mention type or data families, or involve types
 that are not promotable.
+Virtually all data constructors, even those with rich kinds, can be promoted.
+There are only a couple of exceptions to this rule:
The flag :extension:`TypeInType` (which implies :extension:`DataKinds`)
relaxes some of these restrictions, allowing:
+ Data family instance constructors cannot be promoted at the moment. GHC's
+ type theory just isnât up to the task of promoting data families, which
+ requires full dependent types.
 Promotion of type synonyms and type families, but not data families.
 GHC's type theory just isn't up to the task of promoting data families,
 which requires full dependent types.
+ Data constructors with contexts that contain nonequality constraints cannot
+ be promoted. For example: ::
 All datatypes, even those with rich kinds, get promoted. For example: ::
+ data Foo :: Type > Type where
+ MkFoo1 :: a ~ Int => Foo a  promotable
+ MkFoo2 :: a ~~ Int => Foo a  promotable
+ MkFoo3 :: Show a => Foo a  not promotable
 data Proxy a = Proxy
 data App f a = MkApp (f a)  App :: forall k. (k > *) > k > *
 x = Proxy :: Proxy ('MkApp ('Just 'True))
+ ``MkFoo1`` and ``MkFoo2`` can be promoted, since their contexts
+ only involve equalityoriented constraints. However, ``MkFoo3``'s context
+ contains a nonequality constraint ``Show a``, and thus cannot be promoted.
.. _promotionsyntax:
@@ 8236,11 +8711,11 @@ With :extension:`DataKinds`, Haskell's list and tuple types are natively
promoted to kinds, and enjoy the same convenient syntax at the type
level, albeit prefixed with a quote: ::
 data HList :: [*] > * where
+ data HList :: [Type] > Type where
HNil :: HList '[]
HCons :: a > HList t > HList (a ': t)
 data Tuple :: (*,*) > * where
+ data Tuple :: (Type,Type) > Type where
Tuple :: a > b > Tuple '(a,b)
foo0 :: HList '[]
@@ 8260,7 +8735,7 @@ Haskell.
.. note::
The declaration for ``HCons`` also requires :extension:`TypeOperators`
 because of infix type operator ``(:')``
+ because of infix type operator ``(':)``
.. _promotionexistentials:
@@ 8271,7 +8746,7 @@ Promoting existential data constructors
Note that we do promote existential data constructors that are otherwise
suitable. For example, consider the following: ::
 data Ex :: * where
+ data Ex :: Type where
MkEx :: forall a. a > Ex
Both the type ``Ex`` and the data constructor ``MkEx`` get promoted,
@@ 8290,7 +8765,7 @@ The return kind ``k`` is an implicit parameter to ``UnEx``. The
elaborated definitions are as follows (where implicit parameters are
denoted by braces): ::
 type family UnEx {k :: *} (ex :: Ex) :: k
+ type family UnEx {k :: Type} (ex :: Ex) :: k
type instance UnEx {k} (MkEx @k x) = x
Thus, the instance triggers only when the implicit parameter to ``UnEx``
@@ 8303,22 +8778,18 @@ See also :ghcticket:`7347`.
.. _typeintype:
.. _kindpolymorphism:
Kind polymorphism and TypeinType
+Kind polymorphism
==================================
.. extension:: TypeInType
 :shortdesc: Allow kinds to be used as types,
 including explicit kind variable quantification, higherrank
 kinds, kind synonyms, and kind families.
 Implies :extension:`DataKinds`, :extension:`KindSignatures`,
 and :extension:`PolyKinds`.
+ :shortdesc: Deprecated. Enable kind polymorphism and datatype promotion.
:implies: :extension:`PolyKinds`, :extension:`DataKinds`, :extension:`KindSignatures`
:since: 8.0.1
 Allow kinds to be as intricate as types, allowing explicit quantification
 over kind variables, higherrank kinds, and the use of type synonyms and
 families in kinds, among other features.
+ The extension :extension:`TypeInType` is now deprecated: its sole effect is
+ to switch on :extension:`PolyKinds`
+ (and hence :extension:`KindSignatures`) and :extension:`DataKinds`.
.. extension:: PolyKinds
:shortdesc: Enable kind polymorphism.
@@ 8335,31 +8806,6 @@ although it is a conservative extension beyond standard Haskell. The extensions
above simply enable syntax and tweak the inference algorithm to allow users to
take advantage of the extra expressiveness of GHC's kind system.
The difference between :extension:`TypeInType` and :extension:`PolyKinds`


It is natural to consider :extension:`TypeInType` as an extension of
:extension:`PolyKinds`. The latter simply enables fewer features of GHC's
rich kind system than does the former. The need for two separate extensions
stems from their history: :extension:`PolyKinds` was introduced for GHC 7.4,
when it was experimental and temperamental. The wrinkles were smoothed out for
GHC 7.6. :extension:`TypeInType` was introduced for GHC 8.0, and is currently
experimental and temperamental, with the wrinkles to be smoothed out in due
course. The intent of having the two extensions is that users can rely on
:extension:`PolyKinds` to work properly while being duly sceptical of
:extension:`TypeInType`. In particular, we recommend enabling
:ghcflag:`dcorelint` whenever using :extension:`TypeInType`; that extension
turns on a set of internal checks within GHC that will discover bugs in the
implementation of :extension:`TypeInType`. Please report bugs at `our bug
tracker `__.

Although we have tried to allow the new behavior only when
:extension:`TypeInType` is enabled, some particularly thorny cases may have
slipped through. It is thus possible that some construct is available in GHC
8.0 with :extension:`PolyKinds` that was not possible in GHC 7.x. If you spot
such a case, you are welcome to submit that as a bug as well. We flag
newlyavailable capabilities below.

Overview of kind polymorphism

@@ 8367,22 +8813,22 @@ Consider inferring the kind for ::
data App f a = MkApp (f a)
In Haskell 98, the inferred kind for ``App`` is ``(* > *) > * > *``.
But this is overly specific, because another suitable Haskell 98 kind for
``App`` is ``((* > *) > *) > (* > *) > *``, where the kind assigned
to ``a`` is ``* > *``. Indeed, without kind signatures
(:extension:`KindSignatures`), it is necessary to use a dummy constructor
to get a Haskell compiler to infer the second kind. With kind polymorphism
(:extension:`PolyKinds`), GHC infers the kind ``forall k. (k > *) > k > *``
for ``App``, which is its most general kind.
+In Haskell 98, the inferred kind for ``App`` is ``(Type > Type) > Type >
+Type``. But this is overly specific, because another suitable Haskell 98 kind
+for ``App`` is ``((Type > Type) > Type) > (Type > Type) > Type``, where the
+kind assigned to ``a`` is ``Type > Type``. Indeed, without kind signatures
+(:extension:`KindSignatures`), it is necessary to use a dummy constructor to get
+a Haskell compiler to infer the second kind. With kind polymorphism
+(:extension:`PolyKinds`), GHC infers the kind ``forall k. (k > Type) > k >
+Type`` for ``App``, which is its most general kind.
Thus, the chief benefit of kind polymorphism is that we can now infer these
most general kinds and use ``App`` at a variety of kinds: ::
 App Maybe Int  `k` is instantiated to *
+ App Maybe Int  `k` is instantiated to Type
 data T a = MkT (a Int)  `a` is inferred to have kind (* > *)
 App T Maybe  `k` is instantiated to (* > *)
+ data T a = MkT (a Int)  `a` is inferred to have kind (Type > Type)
+ App T Maybe  `k` is instantiated to (Type > Type)
Overview of TypeinType

@@ 8397,16 +8843,15 @@ between types and kinds is a hallmark of dependently typed languages.
Full dependently typed languages also remove the difference between expressions
and types, but doing that in GHC is a story for another day.
One simplification allowed by combining types and kinds is that the type
of ``*`` is just ``*``. It is true that the ``* :: *`` axiom can lead to
nontermination, but this is not a problem in GHC, as we already have other
means of nonterminating programs in both types and expressions. This
decision (among many, many others) *does* mean that despite the expressiveness
of GHC's type system, a "proof" you write in Haskell is not an irrefutable
mathematical proof. GHC promises only partial correctness, that if your
programs compile and run to completion, their results indeed have the types
assigned. It makes no claim about programs that do not finish in a finite
amount of time.
+One simplification allowed by combining types and kinds is that the type of
+``Type`` is just ``Type``. It is true that the ``Type :: Type`` axiom can lead
+to nontermination, but this is not a problem in GHC, as we already have other
+means of nonterminating programs in both types and expressions. This decision
+(among many, many others) *does* mean that despite the expressiveness of GHC's
+type system, a "proof" you write in Haskell is not an irrefutable mathematical
+proof. GHC promises only partial correctness, that if your programs compile and
+run to completion, their results indeed have the types assigned. It makes no
+claim about programs that do not finish in a finite amount of time.
To learn more about this decision and the design of GHC under the hood
please see the `paper `__
@@ 8417,7 +8862,8 @@ Principles of kind inference
Generally speaking, when :extension:`PolyKinds` is on, GHC tries to infer the
most general kind for a declaration.
In this case the definition has a righthand side to inform kind
+In many cases (for example, in a datatype declaration)
+the definition has a righthand side to inform kind
inference. But that is not always the case. Consider ::
type family F a
@@ 8425,42 +8871,114 @@ inference. But that is not always the case. Consider ::
Type family declarations have no righthand side, but GHC must still
infer a kind for ``F``. Since there are no constraints, it could infer
``F :: forall k1 k2. k1 > k2``, but that seems *too* polymorphic. So
GHC defaults those entirelyunconstrained kind variables to ``*`` and we
get ``F :: * > *``. You can still declare ``F`` to be kindpolymorphic
+GHC defaults those entirelyunconstrained kind variables to ``Type`` and we
+get ``F :: Type > Type``. You can still declare ``F`` to be kindpolymorphic
using kind signatures: ::
 type family F1 a  F1 :: * > *
 type family F2 (a :: k)  F2 :: forall k. k > *
 type family F3 a :: k  F3 :: forall k. * > k
+ type family F1 a  F1 :: Type > Type
+ type family F2 (a :: k)  F2 :: forall k. k > Type
+ type family F3 a :: k  F3 :: forall k. Type > k
type family F4 (a :: k1) :: k2  F4 :: forall k1 k2. k1 > k2
The general principle is this:
 *When there is a righthand side, GHC infers the most polymorphic
 kind consistent with the righthand side.* Examples: ordinary data
+ When there is a righthand side, GHC infers the most polymorphic
+ kind consistent with the righthand side. Examples: ordinary data
type and GADT declarations, class declarations. In the case of a
class declaration the role of "right hand side" is played by the
class method signatures.
 *When there is no right hand side, GHC defaults argument and result
 kinds to ``*``, except when directed otherwise by a kind signature*.
+ When there is no right hand side, GHC defaults argument and result
+ kinds to ``Type``, except when directed otherwise by a kind signature.
Examples: data and open type family declarations.
This rule has occasionallysurprising consequences (see
:ghcticket:`10132`. ::
+:ghcticket:`10132`). ::
class C a where  Class declarations are generalised
 so C :: forall k. k > Constraint
data D1 a  No right hand side for these two family
type F1 a  declarations, but the class forces (a :: k)
  so D1, F1 :: forall k. k > *
+  so D1, F1 :: forall k. k > Type
 data D2 a  No righthand side so D2 :: * > *
 type F2 a  No righthand side so F2 :: * > *
+ data D2 a  No righthand side so D2 :: Type > Type
+ type F2 a  No righthand side so F2 :: Type > Type
The kindpolymorphism from the class declaration makes ``D1``
kindpolymorphic, but not so ``D2``; and similarly ``F1``, ``F1``.
+.. _inferringvariableorder:
+
+Inferring the order of variables in a type/class declaration
+
+
+It is possible to get intricate dependencies among the type variables
+introduced in a type or class declaration. Here is an example::
+
+ data T a (b :: k) c = MkT (a c)
+
+After analysing this declaration, GHC will discover that ``a`` and
+``c`` can be kindpolymorphic, with ``a :: k2 > Type`` and
+``c :: k2``. We thus infer the following kind::
+
+ T :: forall {k2 :: Type} (k :: Type). (k2 > Type) > k > k2 > Type
+
+Note that ``k2`` is placed *before* ``k``, and that ``k`` is placed *before*
+``a``. Also, note that ``k2`` is written here in braces. As explained with
+:extension:`TypeApplications` (:ref:`inferredvsspecified`),
+type and kind variables that GHC generalises
+over, but not written in the original program, are not available for visible
+type application. (These are called *inferred* variables.)
+Such variables are written in braces with
+:ghcflag:`fprintexplicitforalls` enabled.
+
+The general principle is this:
+
+ * Variables not available for type application come first.
+
+ * Then come variables the user has written, implicitly brought into scope
+ in a type variable's kind.
+
+ * Lastly come the normal type variables of a declaration.
+
+ * Variables not given an explicit ordering by the user are sorted according
+ to ScopedSort (:ref:`ScopedSort`).
+
+With the ``T`` example above, we could bind ``k`` *after* ``a``; doing so
+would not violate dependency concerns. However, it would violate our general
+principle, and so ``k`` comes first.
+
+Sometimes, this ordering does not respect dependency. For example::
+
+ data T2 k (a :: k) (c :: Proxy '[a, b])
+
+It must be that ``a`` and ``b`` have the same kind. Note also that ``b``
+is implicitly declared in ``c``\'s kind. Thus, according to our general
+principle, ``b`` must come *before* ``k``. However, ``b`` *depends on*
+``k``. We thus reject ``T2`` with a suitable error message.
+
+In associated types, we order the type variables as if the type family was a
+toplevel declaration, ignoring the visibilities of the class's type variable
+binders. Here is an example: ::
+
+ class C (a :: k) b where
+ type F (c :: j) (d :: Proxy m) a b
+
+We infer these kinds::
+
+ C :: forall {k1 :: Type} (k :: Type). k > k1 > Constraint
+ F :: forall {k1 :: Type} {k2 :: Type} {k3 :: Type} j (m :: k1).
+ j > Proxy m > k2 > k3 > Type
+
+Note that the kind of ``a`` is specified in the kind of ``C`` but inferred in
+the kind of ``F``.
+
+The "general principle" described here is meant to make all this more
+predictable for users. It would not be hard to extend GHC to relax
+this principle. If you should want a change here, consider writing
+a `proposal `_ to
+do so.
+
.. index::
single: CUSK
single: complete usersupplied kind signature
@@ 8474,21 +8992,21 @@ Just as in type inference, kind inference for recursive types can only
use *monomorphic* recursion. Consider this (contrived) example: ::
data T m a = MkT (m a) (T Maybe (m a))
  GHC infers kind T :: (* > *) > * > *
+  GHC infers kind T :: (Type > Type) > Type > Type
The recursive use of ``T`` forced the second argument to have kind
``*``. However, just as in type inference, you can achieve polymorphic
+``Type``. However, just as in type inference, you can achieve polymorphic
recursion by giving a *complete usersupplied kind signature* (or CUSK)
for ``T``. A CUSK is present when all argument kinds and the result kind
are known, without any need for inference. For example: ::
 data T (m :: k > *) :: k > * where
+ data T (m :: k > Type) :: k > Type where
MkT :: m a > T Maybe (m a) > T m a
The complete usersupplied kind signature specifies the polymorphic kind
for ``T``, and this signature is used for all the calls to ``T``
including the recursive ones. In particular, the recursive use of ``T``
is at kind ``*``.
+is at kind ``Type``.
What exactly is considered to be a "complete usersupplied kind
signature" for a type constructor? These are the forms:
@@ 8499,35 +9017,30 @@ signature" for a type constructor? These are the forms:
annotation does not affect whether or not the declaration has a
complete signature. ::
 data T1 :: (k > *) > k > * where ...
  Yes; T1 :: forall k. (k>*) > k > *
+ data T1 :: (k > Type) > k > Type where ...
+  Yes; T1 :: forall k. (k>Type) > k > Type
 data T2 (a :: k > *) :: k > * where ...
  Yes; T2 :: forall k. (k>*) > k > *
+ data T2 (a :: k > Type) :: k > Type where ...
+  Yes; T2 :: forall k. (k>Type) > k > Type
 data T3 (a :: k > *) (b :: k) :: * where ...
  Yes; T3 :: forall k. (k>*) > k > *
+ data T3 (a :: k > Type) (b :: k) :: Type where ...
+  Yes; T3 :: forall k. (k>Type) > k > Type
 data T4 (a :: k > *) (b :: k) where ...
  Yes; T4 :: forall k. (k>*) > k > *
+ data T4 (a :: k > Type) (b :: k) where ...
+  Yes; T4 :: forall k. (k>Type) > k > Type
 data T5 a (b :: k) :: * where ...
+ data T5 a (b :: k) :: Type where ...
 No; kind is inferred
data T6 a b where ...
 No; kind is inferred
 For a datatype with a toplevel ``::`` when :extension:`TypeInType`
 is in effect: all kind variables introduced after the ``::`` must
 be explicitly quantified. ::
+ For a datatype with a toplevel ``::``: all kind variables introduced after
+ the ``::`` must be explicitly quantified. ::
  XTypeInType is on
 data T1 :: k > *  No CUSK: `k` is not explicitly quantified
 data T2 :: forall k. k > *  CUSK: `k` is bound explicitly
 data T3 :: forall (k :: *). k > *  still a CUSK

 Note that the first example would indeed have a CUSK without
 :extension:`TypeInType`.
+ data T1 :: k > Type  No CUSK: `k` is not explicitly quantified
+ data T2 :: forall k. k > Type  CUSK: `k` is bound explicitly
+ data T3 :: forall (k :: Type). k > Type  still a CUSK
 For a class, every type variable must be annotated with a kind.
@@ 8543,13 +9056,12 @@ signature" for a type constructor? These are the forms:
signature  no inference can be done before detecting the signature.
 An unassociated open type or data family declaration *always* has a CUSK;
 unannotated type variables default to
 kind ``*``: ::
+ unannotated type variables default to kind ``Type``: ::
 data family D1 a  D1 :: * > *
 data family D2 (a :: k)  D2 :: forall k. k > *
 data family D3 (a :: k) :: *  D3 :: forall k. k > *
 type family S1 a :: k > *  S1 :: forall k. * > k > *
+ data family D1 a  D1 :: Type > Type
+ data family D2 (a :: k)  D2 :: forall k. k > Type
+ data family D3 (a :: k) :: Type  D3 :: forall k. k > Type
+ type family S1 a :: k > Type  S1 :: forall k. Type > k > Type
 An associated type or data family declaration has a CUSK precisely if
its enclosing class has a CUSK. ::
@@ 8564,21 +9076,15 @@ signature" for a type constructor? These are the forms:
variables are annotated and a return kind (with a toplevel ``::``)
is supplied.
With :extension:`TypeInType` enabled, it is possible to write a datatype
that syntactically has a CUSK (according to the rules above)
but actually requires some inference. As a very contrived example, consider ::
+It is possible to write a datatype that syntactically has a CUSK (according to
+the rules above) but actually requires some inference. As a very contrived
+example, consider ::
 data Proxy a  Proxy :: forall k. k > *
+ data Proxy a  Proxy :: forall k. k > Type
data X (a :: Proxy k)
According to the rules above ``X`` has a CUSK. Yet, what is the kind of ``k``?
It is impossible to know. This code is thus rejected as masquerading as having
a CUSK, but not really. If you wish ``k`` to be polykinded, it is straightforward
to specify this: ::

 data X (a :: Proxy (k1 :: k2))

The above definition is indeed fully fixed, with no masquerade.
+According to the rules above ``X`` has a CUSK. Yet, the kind of ``k`` is undetermined.
+It is thus quantified over, giving ``X`` the kind ``forall k1 (k :: k1). Proxy k > Type``.
Kind inference in closed type families

@@ 8631,9 +9137,9 @@ for it: ::
In the class declaration, nothing constrains the kind of the type ``a``,
so it becomes a polykinded type variable ``(a :: k)``. Yet, in the
instance declaration, the righthand side of the associated type
instance ``b > b`` says that ``b`` must be of kind ``*``. GHC could
+instance ``b > b`` says that ``b`` must be of kind ``Type``. GHC could
theoretically propagate this information back into the instance head,
and make that instance declaration apply only to type of kind ``*``, as
+and make that instance declaration apply only to type of kind ``Type``, as
opposed to types of any kind. However, GHC does *not* do this.
In short: GHC does *not* propagate kind information from the members of
@@ 8654,23 +9160,23 @@ type when figuring out how to generalise the type's kind.
For example,
consider these definitions (with :extension:`ScopedTypeVariables`): ::
 data Proxy a  Proxy :: forall k. k > *
+ data Proxy a  Proxy :: forall k. k > Type
p :: forall a. Proxy a
 p = Proxy :: Proxy (a :: *)
+ p = Proxy :: Proxy (a :: Type)
GHC reports an error, saying that the kind of ``a`` should be a kind variable
``k``, not ``*``. This is because, by looking at the type signature
+``k``, not ``Type``. This is because, by looking at the type signature
``forall a. Proxy a``, GHC assumes ``a``'s kind should be generalised, not
restricted to be ``*``. The function definition is then rejected for being
+restricted to be ``Type``. The function definition is then rejected for being
more specific than its type signature.
Explicit kind quantification

Enabled by :extension:`TypeInType`, GHC now supports explicit kind quantification,
+Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification,
as in these examples: ::
 data Proxy :: forall k. k > *
+ data Proxy :: forall k. k > Type
f :: (forall k (a :: k). Proxy a > ()) > Int
Note that the second example has a ``forall`` that binds both a kind ``k`` and
@@ 8701,8 +9207,8 @@ Consider the type ::
This datatype ``G`` is GADTlike in both its kind and its type. Suppose you
have ``g :: G a``, where ``a :: k``. Then pattern matching to discover that
``g`` is in fact ``GMaybe`` tells you both that ``k ~ (* > *)`` and
``a ~ Maybe``. The definition for ``G`` requires that :extension:`TypeInType`
+``g`` is in fact ``GMaybe`` tells you both that ``k ~ (Type > Type)`` and
+``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds`
be in effect, but patternmatching on ``G`` requires no extension beyond
:extension:`GADTs`. That this works is actually a straightforward extension
of regular GADTs and a consequence of the fact that kinds and types are the
@@ 8753,12 +9259,29 @@ In this redefinition, we give an explicit kind for ``(:~~:)``, deferring the cho
of ``k2`` until after the first argument (``a``) has been given. With this declaration
for ``(:~~:)``, the instance for ``HTestEquality`` is accepted.
+Another difference between higherrank kinds and types can be found in their
+treatment of inferred and userspecified type variables. Consider the following
+program: ::
+
+ newtype Foo (f :: forall k. k > Type) = MkFoo (f Int)
+ data Proxy a = Proxy
+
+ foo :: Foo Proxy
+ foo = MkFoo Proxy
+
+The kind of ``Foo``'s parameter is ``forall k. k > Type``, but the kind of
+``Proxy`` is ``forall {k}. k > Type``, where ``{k}`` denotes that the kind
+variable ``k`` is to be inferred, not specified by the user. (See
+:ref:`visibletypeapplication` for more discussion on the inferredspecified
+distinction). GHC does not consider ``forall k. k > Type`` and
+``forall {k}. k > Type`` to be equal at the kind level, and thus rejects
+``Foo Proxy`` as illkinded.
+
Constraints in kinds

As kinds and types are the same, kinds can now (with :extension:`TypeInType`)
contain type constraints. Only equality constraints are currently supported,
however. We expect this to extend to other constraints in the future.
+As kinds and types are the same, kinds can (with :extension:`TypeInType`)
+contain type constraints. However, only equality constraints are supported.
Here is an example of a constrained kind: ::
@@ 8767,7 +9290,7 @@ Here is an example of a constrained kind: ::
IsTypeLit Symbol = 'True
IsTypeLit a = 'False
 data T :: forall a. (IsTypeLit a ~ 'True) => a > * where
+ data T :: forall a. (IsTypeLit a ~ 'True) => a > Type where
MkNat :: T 42
MkSymbol :: T "Don't panic!"
@@ 8776,50 +9299,22 @@ we get an error that the equality constraint is not satisfied; ``Int`` is
not a type literal. Note that explicitly quantifying with ``forall a`` is
not necessary here.
The kind ``*``


The kind ``*`` classifies ordinary types. Without :extension:`TypeInType`,
this identifier is always in scope when writing a kind. However, with
:extension:`TypeInType`, a user may wish to use ``*`` in a type or a
type operator ``*`` in a kind. To make this all more manageable, ``*``
becomes an (almost) ordinary name with :extension:`TypeInType` enabled.
So as not to cause naming collisions, it is not imported by default;
you must ``import Data.Kind`` to get ``*`` (but only with :extension:`TypeInType`
enabled).

The only way ``*`` is unordinary is in its parsing. In order to be backward
compatible, ``*`` is parsed as if it were an alphanumeric identifier; note
that we do not write ``Int :: (*)`` but just plain ``Int :: *``. Due to the
bizarreness with which ``*`` is parsedand the fact that it is the only such
operator in GHCthere are some corner cases that are
not handled. We are aware of three:

 In a Haskell98style data constructor, you must put parentheses around
 ``*``, like this: ::

 data Universe = Ty (*)  Num Int  ...

 In an import/export list, you must put parentheses around ``*``, like this: ::

 import Data.Kind ( type (*) )

 Note that the keyword ``type`` there is just to disambiguate the import
 from a termlevel ``(*)``. (:ref:`explicitnamespaces`)
+The kind ``Type``
+
 In an instance declaration head (the part after the word ``instance``), you
 must parenthesize ``*``. This applies to all manners of instances, including
 the lefthand sides of individual equations of a closed type family.
+.. extension:: StarIsType
+ :shortdesc: Treat ``*`` as ``Data.Kind.Type``.
The ``Data.Kind`` module also exports ``Type`` as a synonym for ``*``.
Now that type synonyms work in kinds, it is conceivable that we will deprecate
``*`` when there is a good migration story for everyone to use ``Type``.
If you like neither of these names, feel free to write your own synonym: ::
+ :since: 8.6.1
 type Set = *  silly Agda programmers...
+ Treat the unqualified uses of the ``*`` type operator as nullary and desugar
+ to ``Data.Kind.Type``.
All the affordances for ``*`` also apply to ``â
``, the Unicode variant
of ``*``.
+The kind ``Type`` (imported from ``Data.Kind``) classifies ordinary types. With
+:extension:`StarIsType` (currently enabled by default), ``*`` is desugared to
+``Type``, but using this legacy syntax is not recommended due to conflicts with
+:extension:`TypeOperators`. This also applies to ``â
``, the Unicode variant of
+``*``.
Inferring dependency in datatype declarations

@@ 8852,19 +9347,44 @@ system does not have principal types) or merely practical (inferring this
dependency is hard, given GHC's implementation). So, GHC takes the easy
way out and requires a little help from the user.
+Inferring dependency in userwritten ``forall``\s
+
+
+A programmer may use ``forall`` in a type to introduce new quantified type
+variables. These variables may depend on each other, even in the same
+``forall``. However, GHC requires that the dependency be inferrable from
+the body of the ``forall``. Here are some examples::
+
+ data Proxy k (a :: k) = MkProxy  just to use below
+
+ f :: forall k a. Proxy k a  This is just fine. We see that (a :: k).
+ f = undefined
+
+ g :: Proxy k a > ()  This is to use below.
+ g = undefined
+
+ data Sing a
+ h :: forall k a. Sing k > Sing a > ()  No obvious relationship between k and a
+ h _ _ = g (MkProxy :: Proxy k a)  This fails. We didn't know that a should have kind k.
+
+Note that in the last example, it's impossible to learn that ``a`` depends on ``k`` in the
+body of the ``forall`` (that is, the ``Sing k > Sing a > ()``). And so GHC rejects
+the program.
+
Kind defaulting without :extension:`PolyKinds`

Without :extension:`PolyKinds` or :extension:`TypeInType` enabled, GHC
refuses to generalise over kind variables. It thus defaults kind variables
to ``*`` when possible; when this is not possible, an error is issued.
+Without :extension:`PolyKinds`, GHC refuses to generalise over kind variables.
+It thus defaults kind variables to ``Type`` when possible; when this is not
+possible, an error is issued.
Here is an example of this in action: ::
 {# LANGUAGE TypeInType #}
 data Proxy a = P  inferred kind: Proxy :: k > *
+ {# LANGUAGE PolyKinds #}
+ import Data.Kind (Type)
+ data Proxy a = P  inferred kind: Proxy :: k > Type
data Compose f g x = MkCompose (f (g x))
  inferred kind: Compose :: (b > *) > (a > b) > a > *
+  inferred kind: Compose :: (b > Type) > (a > b) > a > Type
 separate module having imported the first
{# LANGUAGE NoPolyKinds, DataKinds #}
@@ 8873,13 +9393,13 @@ Here is an example of this in action: ::
In the last line, we use the promoted constructor ``'MkCompose``, which has
kind ::
 forall (a :: *) (b :: *) (f :: b > *) (g :: a > b) (x :: a).
+ forall (a :: Type) (b :: Type) (f :: b > Type) (g :: a > b) (x :: a).
f (g x) > Compose f g x
Now we must infer a type for ``z``. To do so without generalising over kind
variables, we must default the kind variables of ``'MkCompose``. We can
easily default ``a`` and ``b`` to ``*``, but ``f`` and ``g`` would be illkinded
if defaulted. The definition for ``z`` is thus an error.
+variables, we must default the kind variables of ``'MkCompose``. We can easily
+default ``a`` and ``b`` to ``Type``, but ``f`` and ``g`` would be illkinded if
+defaulted. The definition for ``z`` is thus an error.
Prettyprinting in the presence of kind polymorphism

@@ 8909,16 +9429,16 @@ polymorphism.
Here are the key definitions, all available from ``GHC.Exts``: ::
 TYPE :: RuntimeRep > *  highly magical, built into GHC
+ TYPE :: RuntimeRep > Type  highly magical, built into GHC
data RuntimeRep = LiftedRep  for things like `Int`
 UnliftedRep  for things like `Array#`
 IntRep  for `Int#`
  TupleRep [RuntimeRep]  unboxed tuples, indexed by the representations of the elements
  SumRep [RuntimeRep]  unboxed sums, indexed by the representations of the disjuncts
+  TupleRep [RuntimeRep]  unboxed tuples, indexed by the representations of the elements
+  SumRep [RuntimeRep]  unboxed sums, indexed by the representations of the disjuncts
 ...
 type * = TYPE LiftedRep  * is just an ordinary type synonym
+ type Type = TYPE LiftedRep  Type is just an ordinary type synonym
The idea is that we have a new fundamental type constant ``TYPE``, which
is parameterised by a ``RuntimeRep``. We thus get ``Int# :: TYPE 'IntRep``
@@ 8956,7 +9476,7 @@ representationpolymorphic type.
However, not all is lost. We can still do this: ::
 ($) :: forall r (a :: *) (b :: TYPE r).
+ ($) :: forall r (a :: Type) (b :: TYPE r).
(a > b) > a > b
f $ x = f x
@@ 8988,7 +9508,7 @@ stub out functions that return unboxed types.
Printing levitypolymorphic types

.. ghcflag:: fprintexplicitruntimerep
+.. ghcflag:: fprintexplicitruntimereps
:shortdesc: Print ``RuntimeRep`` variables in types which are
runtimerepresentation polymorphic.
:type: dynamic
@@ 9002,7 +9522,8 @@ Most GHC users will not need to worry about levity polymorphism
or unboxed types. For these users, seeing the levity polymorphism
in the type of ``$`` is unhelpful. And thus, by default, it is suppressed,
by supposing all type variables of type ``RuntimeRep`` to be ``'LiftedRep``
when printing, and printing ``TYPE 'LiftedRep`` as ``*``.
+when printing, and printing ``TYPE 'LiftedRep`` as ``Type`` (or ``*`` when
+:extension:`StarIsType` is on).
Should you wish to see levity polymorphism in your types, enable
the flag :ghcflag:`fprintexplicitruntimereps`.
@@ 9128,8 +9649,8 @@ the type level:
GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8))
3
Constraints in types
====================
+Equality constraints, Coercible, and the kind Constraint
+========================================================
.. _equalityconstraints:
@@ 9206,7 +9727,7 @@ denotes representational equality between ``t1`` and ``t2`` in the sense
of Roles (:ref:`roles`). It is exported by :baseref:`Data.Coerce.`, which also
contains the documentation. More details and discussion can be found in the
paper
`"Safe Coercions" `__.
+`"Safe Coercions" `__.
.. _constraintkind:
@@ 9245,8 +9766,8 @@ The following things have kind ``Constraint``:
 Anything whose form is not yet known, but the user has declared to
have kind ``Constraint`` (for which they need to import it from
 ``GHC.Exts``). So for example
 ``type Foo (f :: \* > Constraint) = forall b. f b => b > b``
+ ``Data.Kind``). So for example
+ ``type Foo (f :: Type > Constraint) = forall b. f b => b > b``
is allowed, as well as examples involving type families: ::
type family Typ a b :: Constraint
@@ 9288,74 +9809,333 @@ contexts and superclasses, but to do so you must use
:extension:`UndecidableInstances` to signal that you don't mind if the type
checker fails to terminate.
.. _extensionstotypesignatures:
+.. _quantifiedconstraints:
Extensions to type signatures
=============================
+Quantified constraints
+======================
.. _explicitforalls:
+.. extension:: QuantifiedConstraints
+ :shortdesc: Allow ``forall`` quantifiers in constraints.
Explicit universal quantification (forall)

+ :since: 8.6.1
.. extension:: ExplicitForAll
 :shortdesc: Enable explicit universal quantification.
 Implied by :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
 :extension:`RankNTypes` and :extension:`ExistentialQuantification`.
+ Allow constraints to quantify over types.
 :since: 6.12.1
+The extension :extension:`QuantifiedConstraints` introduces **quantified constraints**,
+which give a new level of expressiveness in constraints. For example, consider ::
 Allow use of the ``forall`` keyword in places where universal quantification
 is implicit.
+ data Rose f a = Branch a (f (Rose f a))
Haskell type signatures are implicitly quantified. When the language
option :extension:`ExplicitForAll` is used, the keyword ``forall`` allows us to
say exactly what this means. For example: ::
+ instance (Eq a, ???) => Eq (Rose f a)
+ where
+ (Branch x1 c1) == (Branch x2 c2)
+ = x1==x1 && c1==c2
 g :: b > b
+From the ``x1==x2`` we need ``Eq a``, which is fine. From ``c1==c2`` we need ``Eq (f (Rose f a))`` which
+is *not* fine in Haskell today; we have no way to solve such a constraint.
means this: ::
+:extension:`QuantifiedConstraints` lets us write this ::
 g :: forall b. (b > b)
+ instance (Eq a, forall b. (Eq b) => Eq (f b))
+ => Eq (Rose f a)
+ where
+ (Branch x1 c1) == (Branch x2 c2)
+ = x1==x1 && c1==c2
The two are treated identically, except that the latter may bring type variables
into scope (see :ref:`scopedtypevariables`).
+Here, the quantified constraint ``forall b. (Eq b) => Eq (f b)`` behaves
+a bit like a local instance declaration, and makes the instance typeable.
Notes:
+The paper `Quantified class constraints `_ (by Bottu, Karachalias, Schrijvers, Oliveira, Wadler, Haskell Symposium 2017) describes this feature in technical detail, with examples, and so is a primary reference source for this proposal.
 With :extension:`ExplicitForAll`, ``forall`` becomes a keyword; you can't use ``forall`` as a
 type variable any more!
+Motivation
+
+Introducing quantified constraints offers two main benefits:
 As well in type signatures, you can also use an explicit ``forall``
 in an instance declaration: ::
+ Firstly, they enable terminating resolution where this was not possible before. Consider for instance the following instance declaration for the general rose datatype ::
 instance forall a. Eq a => Eq [a] where ...
+ data Rose f x = Rose x (f (Rose f x))
 If the :ghcflag:`Wunusedforalls` flag is enabled, a warning will be emitted
 when you write a type variable in an explicit ``forall`` statement that is
 otherwise unused. For instance: ::
+ instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where
+ (Rose x1 rs1) == (Rose x2 rs2) = x1 == x2 && rs1 == rs2
 g :: forall a b. (b > b)
+ This extension allows us to write constraints of the form ``forall b. Eq b =>
+ Eq (f b)``, which is needed to solve the ``Eq (f (Rose f x))`` constraint
+ arising from the second usage of the ``(==)`` method.
 would warn about the unused type variable `a`.
+ Secondly, quantified constraints allow for more concise and precise specifications. As an example, consider the MTL type class for monad transformers::
.. _flexiblecontexts:
+ class Trans t where
+ lift :: Monad m => m a > (t m) a
The context of a type signature

+ The developer knows that a monad transformer takes a monad ``m`` into a new monad ``t m``.
+ But this property is not formally specified in the above declaration.
+ This omission becomes an issue when defining monad transformer composition::
The :extension:`FlexibleContexts` extension lifts the Haskell 98 restriction that
the typeclass constraints in a type signature must have the form *(class
typevariable)* or *(class (typevariable type1 type2 ... typen))*. With
:extension:`FlexibleContexts` these type signatures are perfectly okay
::
+ newtype (t1 * t2) m a = C { runC :: t1 (t2 m) a }
 g :: Eq [a] => ...
 g :: Ord (T a ()) => ...
+ instance (Trans t1, Trans t2) => Trans (t1 * t2) where
+ lift = C . lift . lift
The flag :extension:`FlexibleContexts` also lifts the corresponding restriction
on class declarations (:ref:`superclassrules`) and instance
declarations (:ref:`instancerules`).
+ The goal here is to ``lift`` from monad ``m`` to ``t2 m`` and
+ then ``lift`` this again into ``t1 (t2 m)``.
+ However, this second ``lift`` can only be accepted when ``(t2 m)`` is a monad
+ and there is no way of establishing that this fact universally holds.
+
+ Quantified constraints enable this property to be made explicit in the ``Trans``
+ class declaration::
+
+ class (forall m. Monad m => Monad (t m)) => Trans t where
+ lift :: Monad m => m a > (t m) a
+
+This idea is very old; see Seciton 7 of `Derivable type classes `_.
+
+Syntax changes
+
+
+`Haskell 2010 `_ defines a ``context`` (the bit to the left of ``=>`` in a type) like this
+
+.. codeblock:: none
+
+ context ::= class
+  ( class1, ..., classn )
+
+ class ::= qtycls tyvar
+  qtycls (tyvar atype1 ... atypen)
+
+We to extend ``class`` (warning: this is a rather confusingly named nonterminal symbol) with two extra forms, namely precisely what can appear in an instance declaration
+
+.. codeblock:: none
+
+ class ::= ...
+  [context =>] qtycls inst
+  [context =>] tyvar inst
+
+The definition of ``inst`` is unchanged from the Haskell Report (roughly, just a type).
+The ``context =>`` part is optional. That is the only syntactic change to the language.
+
+Notes:
+
+ Where GHC allows extensions instance declarations we allow exactly the same extensions to this new form of ``class``. Specifically, with :extension:`ExplicitForAll` and :extension:`MultiParameterTypeClasses` the syntax becomes
+
+ .. codeblock:: none
+
+ class ::= ...
+  [forall tyavrs .] [context =>] qtycls inst1 ... instn
+  [forall tyavrs .] [context =>] tyvar inst1 ... instn
+
+ Note that an explicit ``forall`` is often absolutely essential. Consider the rosetree example ::
+
+ instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where ...
+
+ Without the ``forall b``, the type variable ``b`` would be quantified over the whole instance declaration, which is not what is intended.
+
+ One of these new quantified constraints can appear anywhere that any other constraint can, not just in instance declarations. Notably, it can appear in a type signature for a value binding, data constructor, or expression. For example ::
+
+ f :: (Eq a, forall b. Eq b => Eq (f b)) => Rose f a > Rose f a > Bool
+ f t1 t2 = not (t1 == t2)
+
+ The form with a type variable at the head allows this::
+
+ instance (forall xx. c (Free c xx)) => Monad (Free c) where
+ Free f >>= g = f g
+
+ See `Iceland Jack's summary `_. The key point is that the bit to the right of the ``=>`` may be headed by a type *variable* (``c`` in this case), rather than a class. It should not be one of the forall'd variables, though.
+
+ (NB: this goes beyond what is described in `the paper `_, but does not seem to introduce any new technical difficulties.)
+
+
+Typing changes
+
+
+See `the paper `_.
+
+Superclasses
+
+
+Suppose we have::
+
+ f :: forall m. (forall a. Ord a => Ord (m a)) => m Int > Bool
+ f x = x == x
+
+From the ``x==x`` we need an ``Eq (m Int)`` constraint, but the context only gives us a way to figure out ``Ord (m a)`` constraints. But from the given constraint ``forall a. Ord a => Ord (m a)`` we derive a second given constraint ``forall a. Ord a => Eq (m a)``, and from that we can readily solve ``Eq (m Int)``. This process is very similar to the way that superclasses already work: given an ``Ord a`` constraint we derive a second given ``Eq a`` constraint.
+
+NB: This treatment of superclasses goes beyond `the paper `_, but is specifically desired by users.
+
+Overlap
+
+
+Quantified constraints can potentially lead to overlapping local axioms.
+Consider for instance the following example::
+
+ class A a where {}
+ class B a where {}
+ class C a where {}
+ class (A a => C a) => D a where {}
+ class (B a => C a) => E a where {}
+
+ class C a => F a where {}
+ instance (B a, D a, E a) => F a where {}
+
+When type checking the instance declaration for ``F a``,
+we need to check that the superclass ``C`` of ``F`` holds.
+We thus try to entail the constraint ``C a`` under the theory containing:
+
+ The instance axioms : ``(B a, D a, E a) => F a``
+ The local axioms from the instance context : ``B a``, ``D a`` and ``E a``
+ The closure of the superclass relation over these local axioms : ``A a => C a`` and ``B a => C a``
+
+However, the ``A a => C a`` and ``B a => C a`` axioms both match the wanted constraint ``C a``.
+There are several possible approaches for handling these overlapping local axioms:
+
+ **Pick first**. We can simply select the **first matching axiom** we encounter.
+ In the above example, this would be ``A a => C a``.
+ We'd then need to entail ``A a``, for which we have no matching axioms available, causing the above program to be rejected.
+
+ But suppose we made a slight adjustment to the order of the instance context, putting ``E a`` before ``D a``::
+
+ instance (B a, E a, D a) => F a where {}
+
+ The first matching axiom we encounter while entailing ``C a``, is ``B a => C a``.
+ We have a local axiom ``B a`` available, so now the program is suddenly accepted.
+ This behaviour, where the ordering of an instance context determines
+ whether or not the program is accepted, seems rather confusing for the developer.
+
+ **Reject if in doubt**. An alternative approach would be to check for overlapping axioms,
+ when solving a constraint.
+ When multiple matching axioms are discovered, we **reject the program**.
+ This approach is a bit conservative, in that it may reject working programs.
+ But it seem much more transparent towards the developer, who
+ can be presented with a clear message, explaining why the program is rejected.
+
+ **Backtracking**. Lastly, a simple form of **backtracking** could be introduced.
+ We simply select the first matching axiom we encounter and when the entailment fails,
+ we backtrack and look for other axioms that might match the wanted constraint.
+
+ This seems the most intuitive and transparent approach towards the developer,
+ who no longer needs to concern himself with the fact that his code might contain
+ overlapping axioms or with the ordering of his instance contexts. But backtracking
+ would apply equally to ordinary instance selection (in the presence of overlapping
+ instances), so it is a much more pervasive change, with substantial consequences
+ for the type inference engine.
+
+GHC adopts **Reject if in doubt** for now. We can see how painful it
+is in practice, and try something more ambitious if necessary.
+
+Instance lookup
+
+
+In the light of the overlap decision, instance lookup works like this when
+trying to solve a class constraint ``C t``
+
+1. First see if there is a given unquantified constraint ``C t``. If so, use it to solve the constraint.
+
+2. If not, look at all the available given quantified constraints; if exactly one one matches ``C t``, choose it; if more than one matches, report an error.
+
+3. If no quantified constraints match, look up in the global instances, as described in :ref:`instanceresolution` and :ref:`instanceoverlap`.
+
+Termination
+
+
+GHC uses the :ref:`Paterson Conditions ` to ensure
+that instance resolution terminates. How are those rules modified for quantified
+constraints? In two ways.
+
+ Each quantified constraint, taken by itself, must satisfy the termination rules for an instance declaration.
+
+ After "for each class constraint ``(C t1 ... tn)``", add "or each quantified constraint ``(forall as. context => C t1 .. tn)``"
+
+Note that the second item only at the *head* of the quantified constraint, not its context. Reason: the head is the new goal that has to be solved if we use the instance declaration.
+
+Of course, ``UndecidableInstances`` lifts the Paterson Conditions, as now.
+
+Coherence
+
+
+Although quantified constraints are a little like local instance declarations, they differ
+in one big way: the local instances are written by the compiler, not the user, and hence
+cannot introduce incoherence. Consider ::
+
+ f :: (forall a. Eq a => Eq (f a)) => f b > f Bool
+ f x = ...rhs...
+
+In ``...rhs...`` there is, in effect a local instance for ``Eq (f a)`` for any ``a``. But
+at a call site for ``f`` the compiler itself produces evidence to pass to ``f``. For example,
+if we called ``f Nothing``, then ``f`` is ``Maybe`` and the compiler must prove (at the
+call site) that ``forall a. Eq a => Eq (Maybe a)`` holds. It can do this easily, by
+appealing to the existing instance declaration for ``Eq (Maybe a)``.
+
+In short, quantifed constraints do not introduce incoherence.
+
+
+.. _extensionstotypesignatures:
+
+Extensions to type signatures
+=============================
+
+.. _explicitforalls:
+
+Explicit universal quantification (forall)
+
+
+.. extension:: ExplicitForAll
+ :shortdesc: Enable explicit universal quantification.
+ Implied by :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
+ :extension:`RankNTypes` and :extension:`ExistentialQuantification`.
+
+ :since: 6.12.1
+
+ Allow use of the ``forall`` keyword in places where universal quantification
+ is implicit.
+
+Haskell type signatures are implicitly quantified. When the language
+option :extension:`ExplicitForAll` is used, the keyword ``forall`` allows us to
+say exactly what this means. For example: ::
+
+ g :: b > b
+
+means this: ::
+
+ g :: forall b. (b > b)
+
+The two are treated identically, except that the latter may bring type variables
+into scope (see :ref:`scopedtypevariables`).
+
+This extension also enables explicit quantification of type and kind variables
+in :ref:`datainstancedeclarations`, :ref:`typeinstancedeclarations`,
+:ref:`closedtypefamilies`, :ref:`associnst`, and :ref:`rewriterules`.
+
+Notes:
+
+ As well in type signatures, you can also use an explicit ``forall``
+ in an instance declaration: ::
+
+ instance forall a. Eq a => Eq [a] where ...
+
+ If the :ghcflag:`Wunusedforalls` flag is enabled, a warning will be emitted
+ when you write a type variable in an explicit ``forall`` statement that is
+ otherwise unused. For instance: ::
+
+ g :: forall a b. (b > b)
+
+ would warn about the unused type variable `a`.
+
+.. _flexiblecontexts:
+
+The context of a type signature
+
+
+The :extension:`FlexibleContexts` extension lifts the Haskell 98 restriction that
+the typeclass constraints in a type signature must have the form *(class
+typevariable)* or *(class (typevariable type1 type2 ... typen))*. With
+:extension:`FlexibleContexts` these type signatures are perfectly okay
+::
+
+ g :: Eq [a] => ...
+ g :: Ord (T a ()) => ...
+
+The flag :extension:`FlexibleContexts` also lifts the corresponding restriction
+on class declarations (:ref:`superclassrules`) and instance
+declarations (:ref:`instancerules`).
.. _ambiguity:
@@ 9518,29 +10298,27 @@ This extension enables kind signatures in the following places:
 ``data`` declarations: ::
 data Set (cxt :: * > *) a = Set [a]
+ data Set (cxt :: Type > Type) a = Set [a]
 ``type`` declarations: ::
 type T (f :: * > *) = f Int
+ type T (f :: Type > Type) = f Int
 ``class`` declarations: ::
 class (Eq a) => C (f :: * > *) a where ...
+ class (Eq a) => C (f :: Type > Type) a where ...
 ``forall``\'s in type signatures: ::
 f :: forall (cxt :: * > *). Set cxt Int
+ f :: forall (cxt :: Type > Type). Set cxt Int
The parentheses are required. Some of the spaces are required too, to
separate the lexemes. If you write ``(f::*>*)`` you will get a parse
error, because ``::*>*`` is a single lexeme in Haskell.
+The parentheses are required.
As part of the same extension, you can put kind annotations in types as
well. Thus: ::
 f :: (Int :: *) > Int
 g :: forall a. a > (a :: *)
+ f :: (Int :: Type) > Int
+ g :: forall a. a > (a :: Type)
The syntax is
@@ 9566,6 +10344,17 @@ Lexically scoped type variables
Enable lexical scoping of type variables explicitly introduced with
``forall``.
+.. tip::
+
+ ``ScopedTypeVariables`` breaks GHC's usual rule that explicit ``forall`` is optional and doesn't affect semantics.
+ For the :ref:`decltypesigs` (or :ref:`exptypesigs`) examples in this section,
+ the explicit ``forall`` is required.
+ (If omitted, usually the program will not compile; in a few cases it will compile but the functions get a different signature.)
+ To trigger those forms of ``ScopedTypeVariables``, the ``forall`` must appear against the toplevel signature (or outer expression)
+ but *not* against nested signatures referring to the same type variables.
+
+ Explicit ``forall`` is not always required  see :ref:`pattern signature equivalent ` for the example in this section, or :ref:`patterntypesigs`.
+
GHC supports *lexically scoped type variables*, without which some type
signatures are simply impossible to write. For example: ::
@@ 9584,6 +10373,21 @@ signature for ``ys``. In Haskell 98 it is not possible to declare a type
for ``ys``; a major benefit of scoped type variables is that it becomes
possible to do so.
+.. _patternequivform:
+
+An equivalent form for that example, avoiding explicit ``forall`` uses :ref:`patterntypesigs`: ::
+
+ f :: [a] > [a]
+ f (xs :: [aa]) = xs ++ ys
+ where
+ ys :: [aa]
+ ys = reverse xs
+
+Unlike the ``forall`` form, type variable ``a`` from ``f``'s signature is not scoped over ``f``'s equation(s).
+Type variable ``aa`` bound by the pattern signature is scoped over the righthand side of ``f``'s equation.
+(Therefore there is no need to use a distinct type variable; using ``a`` would be equivalent.)
+
+
Overview

@@ 9682,10 +10486,12 @@ This only happens if:
f3 :: forall a. [a] > [a]
Just f3 = Just (\(x:xs) > xs ++ [ x :: a ])  Not OK!
 The binding for ``f3`` is a pattern binding, and so its type
 signature does not bring ``a`` into scope. However ``f1`` is a
 function binding, and ``f2`` binds a bare variable; in both cases the
 type signature brings ``a`` into scope.
+ ``f1`` is a function binding, and ``f2`` binds a bare variable;
+ in both cases the type signature brings ``a`` into scope.
+ However the binding for ``f3`` is a pattern binding,
+ and so ``f3`` is a fresh variable brought into scope by the pattern,
+ not connected with top level ``f3``.
+ Then type variable ``a`` is not in scope of the righthand side of ``Just f3 = ...``.
.. _exptypesigs:
@@ 9731,17 +10537,28 @@ example: ::
f xs = (n, zs)
where
(ys::[a], n) = (reverse xs, length xs)  OK
 zs::[a] = xs ++ ys  OK
+ (zs::[a]) = xs ++ ys  OK
 Just (v::b) = ...  Not OK; b is not in scope
+ Just (v::b) = ...  Not OK; b is not in scope
Here, the pattern signatures for ``ys`` and ``zs`` are fine, but the one
for ``v`` is not because ``b`` is not in scope.
However, in all patterns *other* than pattern bindings, a pattern type
signature may mention a type variable that is not in scope; in this
case, *the signature brings that type variable into scope*. This is
particularly important for existential data constructors. For example: ::
+case, *the signature brings that type variable into scope*. For example: ::
+
+  same f and g as above, now assuming that 'a' is not already in scope
+ f = \(x::Int, y::a) > x  'a' is in scope on RHS of >
+
+ g (x::a) = x :: a
+
+ hh (Just (v :: b)) = v :: b
+
+The pattern type signature makes the type variable available on the righthand side of the equation.
+
+Bringing type variables into scope is particularly important
+for existential data constructors. For example: ::
data T = forall a. MkT [a]
@@ 9749,28 +10566,25 @@ particularly important for existential data constructors. For example: ::
k (MkT [t::a]) =
MkT t3
where
 t3::[a] = [t,t,t]

Here, the pattern type signature ``(t::a)`` mentions a lexical type
variable that is not already in scope. Indeed, it *cannot* already be in
scope, because it is bound by the pattern match. GHC's rule is that in
this situation (and only then), a pattern type signature can mention a
type variable that is not already in scope; the effect is to bring it
into scope, standing for the existentiallybound type variable.

When a pattern type signature binds a type variable in this way, GHC
insists that the type variable is bound to a *rigid*, or fullyknown,
type variable. This means that any userwritten type signature always
stands for a completely known type.

If all this seems a little odd, we think so too. But we must have *some*
way to bring such type variables into scope, else we could not name
existentiallybound type variables in subsequent type signatures.

This is (now) the *only* situation in which a pattern type signature is
allowed to mention a lexical variable that is not already in scope. For
example, both ``f`` and ``g`` would be illegal if ``a`` was not already
in scope.
+ (t3::[a]) = [t,t,t]
+
+Here, the pattern type signature ``[t::a]`` mentions a lexical type
+variable that is not already in scope. Indeed, it *must not* already be in
+scope, because it is bound by the pattern match.
+The effect is to bring it into scope,
+standing for the existentiallybound type variable.
+
+It does seem odd that the existentiallybound type variable *must not*
+be already in scope. Contrast that usually namebindings merely shadow
+(make a 'hole') in a samenamed outer variable's scope.
+But we must have *some* way to bring such type variables into scope,
+else we could not name existentiallybound type variables
+in subsequent type signatures.
+
+Compare the two (identical) definitions for examples ``f``, ``g``;
+they are both legal whether or not ``a`` is already in scope.
+They differ in that *if* ``a`` is already in scope, the signature constrains
+the pattern, rather than the pattern binding the variable.
.. _clsinstscopedtyvars:
@@ 9882,50 +10696,7 @@ assumptions", and a related `blog post ` but type inference becomes
less predicatable if you do so. (Read the papers!)

.. _kindgeneralisation:

Kind generalisation


Just as :extension:`MonoLocalBinds` places limitations on when the *type* of a
*term* is generalised (see :ref:`monolocalbinds`), it also limits when the
*kind* of a *type signature* is generalised. Here is an example involving
:ref:`type signatures on instance declarations `: ::

 data Proxy a = Proxy
 newtype Tagged s b = Tagged b

 class C b where
 c :: forall (s :: k). Tagged s b

 instance C (Proxy a) where
 c :: forall s. Tagged s (Proxy a)
 c = Tagged Proxy

With :extension:`MonoLocalBinds` enabled, this ``C (Proxy a)`` instance will
fail to typecheck. The reason is that the type signature for ``c`` captures
``a``, an outerscoped type variable, which means the type signature is not
closed. Therefore, the inferred kind for ``s`` will *not* be generalised, and
as a result, it will fail to unify with the kind variable ``k`` which is
specified in the declaration of ``c``. This can be worked around by specifying
an explicit kind variable for ``s``, e.g., ::

 instance C (Proxy a) where
 c :: forall (s :: k). Tagged s (Proxy a)
 c = Tagged Proxy

or, alternatively: ::

 instance C (Proxy a) where
 c :: forall k (s :: k). Tagged s (Proxy a)
 c = Tagged Proxy

This declarations are equivalent using Haskell's implicit "add implicit
foralls" rules (see :ref:`implicitquantification`). The implicit foralls rules
are purely syntactic and are quite separate from the kind generalisation
described here.
+less predictable if you do so. (Read the papers!)
.. _visibletypeapplication:
@@ 9933,7 +10704,7 @@ Visible type application
========================
.. extension:: TypeApplications
 :shortdesc: Enable type application syntax.
+ :shortdesc: Enable type application syntax in terms and types.
:since: 8.0.1
@@ 9954,28 +10725,149 @@ 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.
Here are the details:
+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.
+
+.. _inferredvsspecified:
 If an identifier's type signature does not include an
 explicit ``forall``, the type variable arguments appear
 in the lefttoright order in which the variables appear in the type.
 So, ``foo :: Monad m => a b > m (a c)``
 will have its type variables
 ordered as ``m, a, b, c``.
+Inferred vs. specified type variables
+
+
+.. index::
+ single: type variable; inferred vs. specified
+
+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*.
+
+Thus rule applies in datatype declarations, too. For example, if we have
+``data Proxy a = Proxy`` (and :extension:`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 :ghcflag:`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 @[]
+
+ :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,
+:ghcicmd:`: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 :ghcicmd:`:type +v` in the GHCi session above instead
+of :ghcicmd:`:type`. This is because :ghcicmd:`: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 = ``). As we saw above with
+``myLength2``, this type will have no variables available to visible type
+application. On the other hand, :ghcicmd:`: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 :ghcicmd:`: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 :ghcicmd:`:type +v`
+if you want the most accurate information with respect to visible type
+application properties.
+
+.. index::
+ single: ScopedSort
+
+.. _ScopedSort:
+
+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 the ``forall`` is retained.
+
+ If the type signature includes any kind annotations (either on variable
+ binders or as annotations on types), any variables used in kind
+ annotations come before any variables never used in kind annotations.
+ This rule is not recursive: if there is an annotation within an annotation,
+ then the variables used therein are on equal footing. Examples::
+
+ f :: Proxy (a :: k) > Proxy (b :: j) > ()
+  as if f :: forall k j a b. ...
+
+ g :: Proxy (b :: j) > Proxy (a :: (Proxy :: (k > Type) > Type) Proxy) > ()
+  as if g :: forall j k b a. ...
+  NB: k is in a kind annotation within a kind annotation
 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.
+ stable topological sort on the variables. Example::
+
+ h :: Proxy (a :: (j, k)) > Proxy (b :: Proxy a) > ()
+  as if h :: forall j k a b. ...
 For example: if we have ``bar :: Proxy (a :: (j, k)) > b``, then
 the variables are ordered ``j``, ``k``, ``a``, ``b``.
+ In this example, all of ``a``, ``j``, and ``k`` are considered kind
+ variables and will always be placed before ``b``, a lowly type variable.
+ (Note that ``a`` is used in ``b``\'s kind.) Yet, even though ``a`` appears
+ lexically before ``j`` and ``k``, ``j`` and ``k`` are quantified first,
+ because ``a`` depends on ``j`` and ``k``. Note further that ``j`` and ``k``
+ are not reordered with respect to each other, even though doing so would
+ not violate dependency conditions.
 Visible type application is available to instantiate only userspecified
 type variables. This means that in ``data Proxy a = Proxy``, the unmentioned
 kind variable used in ``a``'s kind is *not* available for visible type
 application.
+ 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 variable ``w``,
+ move ``v`` immediately before the leftmost such ``w``.
 Class methods' type arguments include the class type
variables, followed by any variables an individual method is polymorphic
@@ 9994,52 +10886,12 @@ Here are the details:
application. If you want to specify only the second type argument to
``wurble``, then you can say ``wurble @_ @Int``.
The first argument is a wildcard, just like in a partial type signature.
 However, if used in a visible type application, it is *not*
 necessary to specify :extension:`PartialTypeSignatures` and your
+ However, if used in a visible type application/visible kind application,
+ it is *not* necessary to specify :extension:`PartialTypeSignatures` and your
code will not generate a warning informing you of the omitted type.
 When printing types with :ghcflag:`fprintexplicitforalls` enabled,
 type variables not available for visible type application are printed
 in braces. 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 @[]

 :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,
 :ghcicmd:`: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 :ghcicmd:`:type +v` in the GHCi session above instead
 of :ghcicmd:`:type`. This is because :ghcicmd:`: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 = ``). As we saw above with
 ``myLength2``, this type will have no variables available to visible type
 application. On the other hand, :ghcicmd:`: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 :ghcicmd:`: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 :ghcicmd:`:type +v`
 if you want the most accurate information with respect to visible type
 application properties.
+The section in this manual on kind polymorphism describes how variables
+in type and class declarations are ordered (:ref:`inferringvariableorder`).
.. _implicitparameters:
@@ 10048,7 +10900,6 @@ Implicit parameters
.. extension:: ImplicitParams
:shortdesc: Enable Implicit Parameters.
 Implies :extension:`FlexibleContexts` and :extension:`FlexibleInstances`.
:since: 6.8.1
@@ 10481,7 +11332,7 @@ the following pairs are equivalent: ::
h x y = y
in ...
Notice that GHC always adds implicit quantfiers *at the outermost level*
+Notice that GHC always adds implicit quantifiers *at the outermost level*
of a userwritten type; it
does *not* find the innermost possible quantification
point. For example: ::
@@ 10582,7 +11433,8 @@ written with a leading underscore (e.g., "``_``", "``_foo``",
will generate an error message that describes which type is expected at
the hole's location, information about the origin of any free type
variables, and a list of local bindings that might help fill the hole
with actual code. Typed holes are always enabled in GHC.
+and bindings in scope that fit the type of the hole that might help fill
+the hole with actual code. Typed holes are always enabled in GHC.
The goal of typed holes is to help with writing Haskell code rather than
to change the type system. Typed holes can be used to obtain extra
@@ 10604,11 +11456,12 @@ will fail with the following error: ::
Found hole `_' with type: a
Where: `a' is a rigid type variable bound by
the type signature for f :: a > a at hole.hs:1:6
 Relevant bindings include
 f :: a > a (bound at hole.hs:2:1)
 x :: a (bound at hole.hs:2:3)
In the expression: _
In an equation for `f': f x = _
+ Relevant bindings include
+ x :: a (bound at hole.hs:2:3)
+ f :: a > a (bound at hole.hs:2:1)
+ Valid hole fits include x :: a (bound at hole.hs:2:3)
Here are some more details:
@@ 10645,13 +11498,36 @@ Here are some more details:
.. codeblock:: none
 Foo.hs:5:15: error:
 Found hole: _x :: Bool
 Relevant bindings include
 p :: Bool (bound at Foo.hs:3:6)
 cons :: Bool > [Bool] (bound at Foo.hs:3:1)

 Foo.hs:5:20: error:
+ Foo.hs:3:21: error:
+ Found hole: _x :: Bool
+ Or perhaps â_xâ is misspelled, or not in scope
+ In the first argument of â(:)â, namely â_xâ
+ In the second argument of â(:)â, namely â_x : yâ
+ In the second argument of â(:)â, namely âTrue : _x : yâ
+ Relevant bindings include
+ z :: Bool (bound at Foo.hs:3:6)
+ cons :: Bool > [Bool] (bound at Foo.hs:3:1)
+ Valid hole fits include
+ z :: Bool (bound at mpt.hs:2:6)
+ otherwise :: Bool
+ (imported from âPreludeâ at mpt.hs:1:810
+ (and originally defined in âGHC.Baseâ))
+ False :: Bool
+ (imported from âPreludeâ at mpt.hs:1:810
+ (and originally defined in âGHC.Typesâ))
+ True :: Bool
+ (imported from âPreludeâ at mpt.hs:1:810
+ (and originally defined in âGHC.Typesâ))
+ maxBound :: forall a. Bounded a => a
+ with maxBound @Bool
+ (imported from âPreludeâ at mpt.hs:1:810
+ (and originally defined in âGHC.Enumâ))
+ minBound :: forall a. Bounded a => a
+ with minBound @Bool
+ (imported from âPreludeâ at mpt.hs:1:810
+ (and originally defined in âGHC.Enumâ))
+
+ Foo.hs:3:26: error:
Variable not in scope: y :: [Bool]
More information is given for explicit holes (i.e. ones that start
@@ 10669,24 +11545,33 @@ Here are some more details:
.. codeblock:: none
 unbound.hs:1:8:
 Found hole '_x' with type: a
 Where: `a' is a rigid type variable bound by
 the inferred type of cons :: [a] at unbound.hs:1:1
 Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
 In the first argument of `(:)', namely `_x'
 In the expression: _x : _x
 In an equation for `cons': cons = _x : _x

 unbound.hs:1:13:
 Found hole '_x' with type: [a]
 Arising from: an undeclared identifier `_x' at unbound.hs:1:1314
 Where: `a' is a rigid type variable bound by
 the inferred type of cons :: [a] at unbound.hs:1:1
 Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
 In the second argument of `(:)', namely `_x'
 In the expression: _x : _x
 In an equation for `cons': cons = _x : _x
+ unbound.hs:1:8:
+ Found hole '_x' with type: a
+ Where: `a' is a rigid type variable bound by
+ the inferred type of cons :: [a] at unbound.hs:1:1
+ In the first argument of `(:)', namely `_x'
+ In the expression: _x : _x
+ In an equation for `cons': cons = _x : _x
+ Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
+
+ unbound.hs:1:13:
+ Found hole: _x :: [a]
+ Where: âaâ is a rigid type variable bound by
+ the inferred type of cons :: [a]
+ at unbound.hs:3:112
+ Or perhaps â_xâ is misspelled, or not in scope
+ In the second argument of â(:)â, namely â_xâ
+ In the expression: _x : _x
+ In an equation for âconsâ: cons = _x : _x
+ Relevant bindings include cons :: [a] (bound at unbound.hs:3:1)
+ Valid hole fits include
+ cons :: forall a. [a]
+ with cons @a
+ (defined at mpt.hs:3:1)
+ mempty :: forall a. Monoid a => a
+ with mempty @[a]
+ (imported from âPreludeâ at mpt.hs:1:810
+ (and originally defined in âGHC.Baseâ))
Notice the two different types reported for the two different
occurrences of ``_x``.
@@ 10710,11 +11595,67 @@ Here are some more details:
implementation terms, they are reported by the renamer rather than
the type checker.)
There's a flag for controlling the amount of context information shown for
typed holes:
+ The list of valid hole fits is found by checking which bindings in scope
+ would fit into the hole. As an example, compiling the following module with
+ GHC: ::
+
+ import Data.List (inits)
+
+ g :: [String]
+ g = _ "hello, world"
+
+ yields the errors:
+
+
+ .. codeblock:: none
+
+
+ â¢ Found hole: _ :: [Char] > [String]
+ â¢ In the expression: _
+ In the expression: _ "hello, world"
+ In an equation for âgâ: g = _ "hello, world"
+ â¢ Relevant bindings include g :: [String] (bound at mpt.hs:6:1)
+ Valid hole fits include
+ lines :: String > [String]
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âbase4.11.0.0:Data.OldListâ))
+ words :: String > [String]
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âbase4.11.0.0:Data.OldListâ))
+ inits :: forall a. [a] > [[a]]
+ with inits @Char
+ (imported from âData.Listâ at mpt.hs:4:1923
+ (and originally defined in âbase4.11.0.0:Data.OldListâ))
+ repeat :: forall a. a > [a]
+ with repeat @String
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âGHC.Listâ))
+ fail :: forall (m :: * > *). Monad m => forall a. String > m a
+ with fail @[] @String
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âGHC.Baseâ))
+ return :: forall (m :: * > *). Monad m => forall a. a > m a
+ with return @[] @String
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âGHC.Baseâ))
+ pure :: forall (f :: * > *). Applicative f => forall a. a > f a
+ with pure @[] @String
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âGHC.Baseâ))
+ read :: forall a. Read a => String > a
+ with read @[String]
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âText.Readâ))
+ mempty :: forall a. Monoid a => a
+ with mempty @([Char] > [String])
+ (imported from âPreludeâ at mpt.hs:3:89
+ (and originally defined in âGHC.Baseâ))
+
+There are a few flags for controlling the amount of context information shown
+for typed holes:
.. ghcflag:: fshowholeconstraints
 :shortdesc: Show constraints when reporting typed holes
+ :shortdesc: Show constraints when reporting typed holes.
:type: dynamic
:category: verbosity
@@ 10728,19 +11669,326 @@ typed holes:
.. codeblock:: none
 show_constraints.hs:4:7: error:
 â¢ Found hole: _ :: Bool
 â¢ In the expression: _
 In an equation for âfâ: f x = _
 â¢ Relevant bindings include
 x :: a (bound at show_constraints.hs:4:3)
 f :: a > Bool (bound at show_constraints.hs:4:1)
 Constraints include
 Eq a (from the type signature for:
 f :: Eq a => a > Bool
 at show_constraints.hs:3:122)
+ show_constraints.hs:4:7: error:
+ â¢ Found hole: _ :: Bool
+ â¢ In the expression: _
+ In an equation for âfâ: f x = _
+ â¢ Relevant bindings include
+ x :: a (bound at show_constraints.hs:4:3)
+ f :: a > Bool (bound at show_constraints.hs:4:1)
+ Constraints include Eq a (from show_constraints.hs:3:122)
+ Valid hole fits include
+ otherwise :: Bool
+ False :: Bool
+ True :: Bool
+ maxBound :: forall a. Bounded a => a
+ with maxBound @Bool
+ minBound :: forall a. Bounded a => a
+ with minBound @Bool
+
+.. _typedholevalidholefits:
+
+Valid Hole Fits
+
+GHC sometimes suggests valid hole fits for typed holes, which is
+configurable by a few flags.
+
+.. ghcflag:: fnoshowvalidholefits
+ :shortdesc: Disables showing a list of valid hole fits for typed holes
+ in type error messages.
+ :type: dynamic
+ :category: verbosity
+
+ :default: off
+
+ This flag can be toggled to turn off the display of valid hole fits
+ entirely.
+
+.. ghcflag:: fmaxvalidholefits=â¨nâ©
+ :shortdesc: *default: 6.* Set the maximum number of valid hole fits for
+ typed holes to display in type error messages.
+ :type: dynamic
+ :reverse: fnomaxvalidholefits
+ :category: verbosity
+
+ :default: 6
+
+ The list of valid hole fits is limited by displaying up to 6
+ hole fits per hole. The number of hole fits shown can be set by this
+ flag. Turning the limit off with :ghcflag:`fnomaxvalidholefits`
+ displays all found hole fits.
+
+
+.. ghcflag:: fshowtypeofholefits
+ :shortdesc: Toggles whether to show the type of the valid hole fits
+ in the output.
+ :type: dynamic
+ :category: verbosity
+ :reverse: fnotypeofholefits
+
+ :default: on
+
+ By default, the hole fits show the type of the hole fit.
+ This can be turned off by the reverse of this flag.
+
+
+
+.. ghcflag:: fshowtypeappofholefits
+ :shortdesc: Toggles whether to show the type application of the valid
+ hole fits in the output.
+ :type: dynamic
+ :category: verbosity
+ :reverse: fnoshowtypeappofholefits
+
+ :default: on
+
+ By default, the hole fits show the type application needed to make
+ this hole fit fit the type of the hole, e.g. for the hole
+ ``(_ :: Int > [Int])``, ``mempty`` is a hole fit with
+ ``mempty @(Int > [Int])``. This can be toggled off with
+ the reverse of this flag.
+
+.. ghcflag:: fshowdocsofholefits
+ :shortdesc: Toggles whether to show the documentation of the valid
+ hole fits in the output.
+ :type: dynamic
+ :category: verbosity
+ :reverse: fnoshowdocsofholefits
+
+ :default: off
+
+ It can sometime be the case that the name and type of a valid hole
+ fit is not enough to realize what the fit stands for. This flag
+ adds the documentation of the fit to the message, if the
+ documentation is available (and the module from which the function
+ comes was compiled with the ``haddock`` flag).
+
+.. ghcflag:: fshowtypeappvarsofholefits
+ :shortdesc: Toggles whether to show what type each quantified
+ variable takes in a valid hole fit.
+ :type: dynamic
+ :category: verbosity
+ :reverse: fnoshowtypeappvarsofholefits
+
+ :default: on
+
+ By default, the hole fits show the type application needed to make
+ this hole fit fit the type of the hole, e.g. for the hole
+ ``(_ :: Int > [Int])``, ``mempty :: Monoid a => a`` is a hole fit
+ with ``mempty @(Int > [Int])``. This flag toggles whether to show
+ ``a ~ (Int > [Int])`` instead of ``mempty @(Int > [Int])`` in the where
+ clause of the valid hole fit message.
+
+.. ghcflag:: fshowprovenanceofholefits
+ :shortdesc: Toggles whether to show the provenance of the valid hole fits
+ in the output.
+ :type: dynamic
+ :category: verbosity
+ :reverse: fnoshowprovenanceofholefits
+
+ :default: on
+
+ By default, each hole fit shows the provenance information of its
+ hole fit, i.e. where it was bound or defined, and what module
+ it was originally defined in if it was imported. This can be toggled
+ off using the reverse of this flag.
+
+
+.. ghcflag:: funcluttervalidholefits
+ :shortdesc: Unclutter the list of valid hole fits by not showing
+ provenance nor type applications of suggestions.
+ :type: dynamic
+ :category: verbosity
+
+ :default: off
+
+ This flag can be toggled to decrease the verbosity of the valid hole fit
+ suggestions by not showing the provenance nor type application of the
+ suggestions.
+
+
+
+.. _typedholesrefinementholefits:
+
+Refinement Hole Fits
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+When the flag :ghcflag:`frefinementlevelholefits=â¨nâ©` is set to an
+``n`` larger than ``0``, GHC will offer up a list of valid refinement
+hole fits, which are valid hole fits that need up to ``n`` levels of
+additional refinement to be complete, where each level represents an additional
+hole in the hole fit that requires filling in. As an example, consider the
+hole in ::
+
+ f :: [Integer] > Integer
+ f = _
+
+When the refinement level is not set, it will only offer valid hole fits
+suggestions: ::
+
+ Valid hole fits include
+ f :: [Integer] > Integer
+ head :: forall a. [a] > a
+ with head @Integer
+ last :: forall a. [a] > a
+ with last @Integer
+ maximum :: forall (t :: * > *).
+ Foldable t =>
+ forall a. Ord a => t a > a
+ with maximum @[] @Integer
+ minimum :: forall (t :: * > *).
+ Foldable t =>
+ forall a. Ord a => t a > a
+ with minimum @[] @Integer
+ product :: forall (t :: * > *).
+ Foldable t =>
+ forall a. Num a => t a > a
+ with product @[] @Integer
+ sum :: forall (t :: * > *).
+ Foldable t =>
+ forall a. Num a => t a > a
+ with sum @[] @Integer
+
+However, with :ghcflag:`frefinementlevelholefits=â¨nâ©` set to e.g. `1`,
+it will additionally offer up a list of refinement hole fits, in this case: ::
+
+ Valid refinement hole fits include
+ foldl1 (_ :: Integer > Integer > Integer)
+ with foldl1 @[] @Integer
+ where foldl1 :: forall (t :: * > *).
+ Foldable t =>
+ forall a. (a > a > a) > t a > a
+ foldr1 (_ :: Integer > Integer > Integer)
+ with foldr1 @[] @Integer
+ where foldr1 :: forall (t :: * > *).
+ Foldable t =>
+ forall a. (a > a > a) > t a > a
+ const (_ :: Integer)
+ with const @Integer @[Integer]
+ where const :: forall a b. a > b > a
+ ($) (_ :: [Integer] > Integer)
+ with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
+ where ($) :: forall a b. (a > b) > a > b
+ fail (_ :: String)
+ with fail @((>) [Integer]) @Integer
+ where fail :: forall (m :: * > *).
+ Monad m =>
+ forall a. String > m a
+ return (_ :: Integer)
+ with return @((>) [Integer]) @Integer
+ where return :: forall (m :: * > *). Monad m => forall a. a > m a
+ (Some refinement hole fits suppressed;
+ use fmaxrefinementholefits=N or fnomaxrefinementholefits)
+
+Which shows that the hole could be replaced with e.g. ``foldl1 _``. While not
+fixing the hole, this can help users understand what options they have.
+
+.. ghcflag:: frefinementlevelholefits=â¨nâ©
+ :shortdesc: *default: off.* Sets the level of refinement of the
+ refinement hole fits, where level ``n`` means that hole fits
+ of up to ``n`` holes will be considered.
+ :type: dynamic
+ :reverse: fnorefinementlevelholefits
+ :category: verbosity
+
+ :default: off
+
+ The list of valid refinement hole fits is generated by considering
+ hole fits with a varying amount of additional holes. The amount of
+ holes in a refinement can be set by this flag. If the flag is set to 0
+ or not set at all, no valid refinement hole fits will be suggested.
+
+.. ghcflag:: fabstractrefinementholefits
+ :shortdesc: *default: off.* Toggles whether refinements where one or more
+ of the holes are abstract are reported.
+ :type: dynamic
+ :reverse: fnoabstractrefinementholefits
+ :category: verbosity
+
+ :default: off
+
+ Valid list of valid refinement hole fits can often grow large when
+ the refinement level is ``>= 2``, with holes like ``head _ _`` or
+ ``fst _ _``, which are valid refinements, but which are unlikely to be
+ relevant since one or more of the holes are still completely open, in that
+ neither the type nor kind of those holes are constrained by the proposed
+ identifier at all. By default, such holes are not reported. By turning this
+ flag on, such holes are included in the list of valid refinement hole fits.
+
+.. ghcflag:: fmaxrefinementholefits=â¨nâ©
+ :shortdesc: *default: 6.* Set the maximum number of refinement hole fits
+ for typed holes to display in type error messages.
+ :type: dynamic
+ :reverse: fnomaxrefinementholefits
+ :category: verbosity
+
+ :default: 6
+
+ The list of valid refinement hole fits is limited by displaying up to 6
+ hole fits per hole. The number of hole fits shown can be set by this
+ flag. Turning the limit off with :ghcflag:`fnomaxrefinementholefits`
+ displays all found hole fits.
+
+.. ghcflag:: fshowholematchesofholefits
+ :shortdesc: Toggles whether to show the type of the additional holes
+ in refinement hole fits.
+ :type: dynamic
+ :category: verbosity
+ :reverse: fnoshowholematchesofholefits
+
+ :default: on
+
+ The types of the additional holes in refinement hole fits are displayed
+ in the output, e.g. ``foldl1 (_ :: a > a > a)`` is a refinement
+ for the hole ``_ :: [a] > a``. If this flag is toggled off, the output
+ will display only ``foldl1 _``, which can be used as a direct replacement
+ for the hole, without requiring ``XScopedTypeVariables``.
+
+
+Sorting Valid Hole Fits
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+There are currently two ways to sort valid hole fits.
+Sorting can be toggled with :ghcflag:`fsortvalidholefits`
+
+.. ghcflag:: fnosortvalidholefits
+ :shortdesc: Disables the sorting of the list of valid hole fits for typed holes
+ in type error messages.
+ :type: dynamic
+ :category: verbosity
+
+ :default: off
+
+ By default the valid hole fits are sorted to show the most relevant
+ hole fits at the top of the list of valid hole fits. This can be
+ toggled off with this flag.
+
+.. ghcflag:: fsortbysizeholefits
+ :shortdesc: Sort valid hole fits by size.
+ :type: dynamic
+ :reverse: fnosortbysizeholefits
+
+ :default: on
+
+ Sorts by how big the types the quantified type variables in the type of the
+ function would have to be in order to match the type of the hole.
+
+
+.. ghcflag:: fsortbysubsumptionholefits
+ :shortdesc: Sort valid hole fits by subsumption.
+ :type: dynamic
+ :reverse: fnosortbysubsumptionholefits
+
+ :default: off
+
+ An alternative sort. Sorts by checking which hole fits subsume other
+ hole fits, such that if hole fit a could be used as hole fits for
+ hole fit b, then b appears before a in the output. It is more precise than
+ the default sort, but also a lot slower, since a subsumption check has to be
+ run for each pair of valid hole fits.
+
.. _partialtypesignatures:
Partial Type Signatures
@@ 11024,10 +12272,19 @@ Anonymous and named wildcards *can* occur on the left hand side of a
type or data instance declaration;
see :ref:`typewildcardslhs`.
Anonymous wildcards are also allowed in visible type applications
(:ref:`visibletypeapplication`). If you want to specify only the second type
argument to ``wurble``, then you can say ``wurble @_ @Int`` where the first
argument is a wildcard.
+Anonymous wildcards are also allowed in visible type applications/ visible kind
+applications (:ref:`visibletypeapplication`). If you want to specify only the
+second type argument to ``wurble``, then you can say ``wurble @_ @Int`` where
+the first argument is a wildcard.
+
+Standalone ``deriving`` declarations permit the use of a single,
+extraconstraints wildcard, like so: ::
+
+ deriving instance _ => Eq (Foo a)
+
+This denotes a derived ``Eq (Foo a)`` instance where the context is inferred,
+in much the same way that ordinary ``deriving`` clauses do. Any other use of
+wildcards in a standalone ``deriving`` declaration is prohibited.
In all other contexts, type wildcards are disallowed, and a named wildcard is treated
as an ordinary type variable. For example: ::
@@ 11270,7 +12527,7 @@ page on the GHC Wiki has a wealth of information. You may also consult the
:thref:`Haddock reference documentation `.
Many changes to the original
design are described in `Notes on Template Haskell version
2 `__.
+2 `__.
Not all of these changes are in GHC, however.
The first example from that paper is set out below (:ref:`thexample`)
@@ 11653,9 +12910,9 @@ nontrivial program, you may be interested in combining this with the
:ghcflag:`ddumptofile` flag (see :ref:`dumpingoutput`. For each file using
Template Haskell, this will show the output in a ``.dumpsplices`` file.
The flag :ghcflag:`dthdecfile=â¨fileâ©` shows the expansions of all toplevel
+The flag :ghcflag:`dthdecfile` dumps the expansions of all toplevel
TH declaration splices, both typed and untyped, in the file :file:`M.th.hs`
where M is the name of the module being compiled. Note that other types of
+for each module `M` being compiled. Note that other types of
splices (expressions, types, and patterns) are not shown. Application
developers can check this into their repository so that they can grep for
identifiers that were defined in Template Haskell. This is similar to using
@@ 11674,7 +12931,7 @@ Below is a sample output of :ghcflag:`ddumpsplices` ::
foo :: Int > Int
foo x = (x + 1)
Below is the output of the same sample using :ghcflag:`dthdecfile=â¨fileâ©` ::
+Below is the output of the same sample using :ghcflag:`dthdecfile` ::
 TH_pragma.hs:(6,4)(8,26): Splicing declarations
foo :: Int > Int
@@ 13106,9 +14363,11 @@ Certain pragmas are *fileheader pragmas*:
``LANGUAGE`` pragma

.. index::
 single: LANGUAGE; pragma
 single: pragma; LANGUAGE
+.. pragma:: LANGUAGE â¨extâ©, â¨extâ©, ...
+
+ :where: file header
+
+ Enable or disable a set of language extensions.
The ``LANGUAGE`` pragma allows language extensions to be enabled in a
portable way. It is the intention that all Haskell compilers support the
@@ 13138,9 +14397,9 @@ if any of the requested extensions are not supported.
``OPTIONS_GHC`` pragma

.. index::
 single: OPTIONS_GHC
 single: pragma; OPTIONS_GHC
+.. pragma:: OPTIONS_GHC â¨flagsâ©
+
+ :where: file header
The ``OPTIONS_GHC`` pragma is used to specify additional options that
are given to the compiler when compiling this source file. See
@@ 13166,14 +14425,21 @@ other compilers.
``WARNING`` and ``DEPRECATED`` pragmas

.. index::
 single: WARNING
 single: DEPRECATED
+.. pragma:: WARNING
+
+ :where: declaration
+
+ The ``WARNING`` pragma allows you to attach an arbitrary warning to a
+ particular function, class, or type.
The ``WARNING`` pragma allows you to attach an arbitrary warning to a
particular function, class, or type. A ``DEPRECATED`` pragma lets you
specify that a particular function, class, or type is deprecated. There
are two ways of using these pragmas.
+.. pragma:: DEPRECATED
+
+ :where: declaration
+
+ A ``DEPRECATED`` pragma lets you specify that a particular function, class,
+ or type is deprecated.
+
+There are two ways of using these pragmas.
 You can work on an entire module thus: ::
@@ 13224,9 +14490,11 @@ You can suppress the warnings with the flag
``MINIMAL`` pragma

.. index::
 single: MINIMAL
 single: pragma; MINIMAL
+.. pragma:: MINIMAL â¨nameâ©  â¨nameâ© , ...
+
+ :where: in class body
+
+ Define the methods needed for a minimal complete instance of a class.
The ``MINIMAL`` pragma is used to specify the minimal complete definition of
a class, i.e. specify which methods must be implemented by all
@@ 13257,9 +14525,8 @@ Conjunction binds stronger than disjunction.
If no ``MINIMAL`` pragma is given in the class declaration, it is just as if
a pragma ``{# MINIMAL op1, op2, ..., opn #}`` was given, where the
``opi`` are the methods (a) that lack a default method in the class
declaration, and (b) whose name that does not start with an underscore
(c.f. :ghcflag:`Wmissingmethods`, :ref:`optionssanity`).
+``opi`` are the methods that lack a default method in the class
+declaration (c.f. :ghcflag:`Wmissingmethods`, :ref:`optionssanity`).
This warning can be turned off with the flag
:ghcflag:`Wnomissingmethods <Wmissingmethods>`.
@@ 13276,9 +14543,11 @@ These pragmas control the inlining of function definitions.
``INLINE`` pragma
~~~~~~~~~~~~~~~~~
.. index::
 single: INLINE
 single: pragma; INLINE
+.. pragma:: INLINE â¨nameâ©
+
+ :where: toplevel
+
+ Force GHC to inline a value.
GHC (with :ghcflag:`O`, as always) tries to inline (or "unfold")
functions/values that are "small enough," thus avoiding the call
@@ 13342,7 +14611,7 @@ has a number of other effects:
which will optimise better than the corresponding use of ``comp2``.
 It is useful for GHC to optimise the definition of an INLINE function
 ``f`` just like any other nonINLINE function, in case the
+ ``f`` just like any other non``INLINE`` function, in case the
noninlined version of ``f`` is ultimately called. But we don't want
to inline the *optimised* version of ``f``; a major reason for ``INLINE``
pragmas is to expose functions in ``f``\'s RHS that have rewrite
@@ 13355,7 +14624,7 @@ has a number of other effects:
usual. For externallyvisible functions the inlineRHS (not the
optimised RHS) is recorded in the interface file.
 An INLINE function is not worker/wrappered by strictness analysis.
+ An ``INLINE`` function is not worker/wrappered by strictness analysis.
It's going to be inlined wholesale instead.
GHC ensures that inlining cannot go on forever: every mutuallyrecursive
@@ 13386,6 +14655,12 @@ See also the ``NOINLINE`` (:ref:`noinlinepragma`) and ``INLINABLE``
``INLINABLE`` pragma
~~~~~~~~~~~~~~~~~~~~
+.. pragma:: INLINABLE â¨nameâ©
+
+ :where: toplevel
+
+ Suggest that the compiler always consider inlining ``name``.
+
An ``{# INLINABLE f #}`` pragma on a function ``f`` has the following
behaviour:
@@ 13425,10 +14700,15 @@ The alternative spelling ``INLINEABLE`` is also accepted by GHC.
~~~~~~~~~~~~~~~~~~~
.. index::
 single: NOINLINE
single: NOTINLINE
The ``NOINLINE`` pragma does exactly what you'd expect: it stops the
+.. pragma:: NOINLINE â¨nameâ©
+
+ :where: toplevel
+
+ Instructs the compiler not to inline a value.
+
+The :pragma:`NOINLINE` pragma does exactly what you'd expect: it stops the
named function from being inlined by the compiler. You shouldn't ever
need to do this, unless you're very cautious about code size.
@@ 13441,23 +14721,26 @@ used if you want your code to be portable).
``CONLIKE`` modifier
~~~~~~~~~~~~~~~~~~~~
.. index::
 single: CONLIKE
+.. pragma:: CONLINE
An ``INLINE`` or ``NOINLINE`` pragma may have a ``CONLIKE`` modifier, which affects
matching in RULEs (only). See :ref:`conlike`.
+ :where: modifies :pragma:`INLINE` or :pragma:`NOINLINE` pragma
+
+ Instructs GHC to consider a value to be especially cheap to inline.
+
+An :pragma:`INLINE` or :pragma:`NOINLINE` pragma may have a :pragma:`CONLIKE` modifier, which affects
+matching in :pragma:`RULE`\s (only). See :ref:`conlike`.
.. _phasecontrol:
Phase control
~~~~~~~~~~~~~
Sometimes you want to control exactly when in GHC's pipeline the ``INLINE``
+Sometimes you want to control exactly when in GHC's pipeline the :pragma:`INLINE`
pragma is switched on. Inlining happens only during runs of the
*simplifier*. Each run of the simplifier has a different *phase number*;
the phase number decreases towards zero. If you use
``dverbosecore2core`` you'll see the sequence of phase numbers for
successive runs of the simplifier. In an ``INLINE`` pragma you can
+:ghcflag:`dverbosecore2core` you will see the sequence of phase numbers for
+successive runs of the simplifier. In an :pragma:`INLINE` pragma you can
optionally specify a phase number, thus:
 "``INLINE[k] f``" means: do not inline ``f`` until phase ``k``, but
@@ 13475,7 +14758,7 @@ optionally specify a phase number, thus:
The same information is summarised here:
::
+.. codeblock:: none
 Before phase 2 Phase 2 and later
{# INLINE [2] f #}  No Yes
@@ 13490,14 +14773,14 @@ By "Maybe" we mean that the usual heuristic inlining rules apply (if the
function body is small, or it is applied to interestinglooking
arguments etc). Another way to understand the semantics is this:
 For both ``INLINE`` and ``NOINLINE``, the phase number says when inlining is
 allowed at all.
+ For both :pragma:`INLINE` and :pragma:`NOINLINE`, the phase number says when
+ inlining is allowed at all.
 The ``INLINE`` pragma has the additional effect of making the function
+ The :pragma:`INLINE` pragma has the additional effect of making the function
body look small, so that when inlining is allowed it is very likely
to happen.
The same phasenumbering control is available for RULES
+The same phasenumbering control is available for :pragma:`RULE`\s
(:ref:`rewriterules`).
.. _linepragma:
@@ 13505,9 +14788,12 @@ The same phasenumbering control is available for RULES
``LINE`` pragma

.. index::
 single: LINE; pragma
 single: pragma; LINE
+.. pragma:: LINE â¨linenoâ© "â¨fileâ©"
+
+ :where: anywhere
+
+ Generated by preprocessors to convey source line numbers of the original
+ source.
This pragma is similar to C's ``#line`` pragma, and is mainly for use in
automatically generated Haskell code. It lets you specify the line
@@ 13555,7 +14841,7 @@ diagnostics and does not change the syntax of the code itself.
``RULES`` pragma

The ``RULES`` pragma lets you specify rewrite rules. It is described in
+The :pragma:`RULES` pragma lets you specify rewrite rules. It is described in
:ref:`rewriterules`.
.. _specializepragma:
@@ 13568,8 +14854,12 @@ The ``RULES`` pragma lets you specify rewrite rules. It is described in
single: pragma, SPECIALIZE
single: overloading, death to
+.. pragma:: SPECIALIZE â¨nameâ© :: â¨typeâ©
+
+ Ask that GHC specialize a polymorphic value to a particular type.
+
(UK spelling also accepted.) For key overloaded functions, you can
create extra versions (NB: more code space) specialised to particular
+create extra versions (NB: at the cost of larger code) specialised to particular
types. Thus, if you have an overloaded function:
::
@@ 13666,6 +14956,10 @@ specialise it as follows:
``SPECIALIZE INLINE``
~~~~~~~~~~~~~~~~~~~~~
+.. pragma:: SPECIALIZE INLINE â¨nameâ© :: â¨typeâ©
+
+ :where: toplevel
+
A ``SPECIALIZE`` pragma can optionally be followed with a ``INLINE`` or
``NOINLINE`` pragma, optionally followed by a phase, as described in
:ref:`inlinenoinlinepragma`. The ``INLINE`` pragma affects the
@@ 13691,9 +14985,9 @@ fire the first specialisation, whose body is also inlined. The result is
a typebased unrolling of the indexing function.
You can add explicit phase control (:ref:`phasecontrol`) to
``SPECIALISE INLINE`` pragma, just like on an ``INLINE`` pragma; if you
do so, the same phase is used for the rewrite rule and the INLINE
control of the specialised function.
+``SPECIALISE INLINE`` pragma, just like on an :pragma:`INLINE` pragma; if you do
+so, the same phase is used for the rewrite rule and the INLINE control of the
+specialised function.
.. warning:: You can make GHC diverge by using ``SPECIALISE INLINE`` on an
ordinarilyrecursive function.
@@ 13701,9 +14995,9 @@ control of the specialised function.
``SPECIALIZE`` for imported functions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally, you can only give a ``SPECIALIZE`` pragma for a function
+Generally, you can only give a :pragma:`SPECIALIZE` pragma for a function
defined in the same module. However if a function ``f`` is given an
``INLINABLE`` pragma at its definition site, then it can subsequently be
+:pragma:`INLINABLE` pragma at its definition site, then it can subsequently be
specialised by importing modules (see :ref:`inlinablepragma`). For example ::
module Map( lookup, blah blah ) where
@@ 13717,7 +15011,7 @@ specialised by importing modules (see :ref:`inlinablepragma`). For example ::
data T = T1  T2 deriving( Eq, Ord )
{# SPECIALISE lookup :: [(T,a)] > T > Maybe a
Here, ``lookup`` is declared ``INLINABLE``, but it cannot be specialised
+Here, ``lookup`` is declared :pragma:`INLINABLE`, but it cannot be specialised
for type ``T`` at its definition site, because that type does not exist
yet. Instead a client module can define ``T`` and then specialise
``lookup`` at that type.
@@ 13725,13 +15019,13 @@ yet. Instead a client module can define ``T`` and then specialise
Moreover, every module that imports ``Client`` (or imports a module that
imports ``Client``, transitively) will "see", and make use of, the
specialised version of ``lookup``. You don't need to put a
``SPECIALIZE`` pragma in every module.
+:pragma:`SPECIALIZE` pragma in every module.
Moreover you often don't even need the ``SPECIALIZE`` pragma in the
+Moreover you often don't even need the :pragma:`SPECIALIZE` pragma in the
first place. When compiling a module ``M``, GHC's optimiser (when given the
:ghcflag:`O` flag) automatically considers each toplevel overloaded function declared
in ``M``, and specialises it for the different types at which it is called in
``M``. The optimiser *also* considers each *imported* ``INLINABLE``
+``M``. The optimiser *also* considers each *imported* :pragma:`INLINABLE`
overloaded function, and specialises it for the different types at which
it is called in ``M``. So in our example, it would be enough for ``lookup``
to be called at type ``T``:
@@ 13749,28 +15043,19 @@ to be called at type ``T``:
However, sometimes there are no such calls, in which case the pragma can
be useful.
Obsolete ``SPECIALIZE`` syntax
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

In earlier versions of GHC, it was possible to provide your own
specialised function for a given type:

::

 {# SPECIALIZE hammeredLookup :: [(Int, value)] > Int > value = intLookup #}

This feature has been removed, as it is now subsumed by the ``RULES``
pragma (see :ref:`rulespec`).

.. _specializeinstancepragma:
``SPECIALIZE`` instance pragma

.. index::
 single: SPECIALIZE pragma
+ single: instance, specializing
single: overloading, death to
+.. pragma:: SPECIALIZE instance â¨instance headâ©
+
+ :where: instance body
+
Same idea, except for instance declarations. For example:
::
@@ 13788,8 +15073,12 @@ declaration.
``UNPACK`` pragma

.. index::
 single: UNPACK
+.. pragma:: UNPACK
+
+ :where: data constructor field
+
+ Instructs the compiler to unpack the contents of a constructor field into
+ the constructor itself.
The ``UNPACK`` indicates to the compiler that it should unpack the
contents of a constructor field into the constructor itself, removing a
@@ 13830,19 +15119,19 @@ See also the :ghcflag:`funboxstrictfields` flag, which essentially has the
effect of adding ``{# UNPACK #}`` to every strict constructor field.
.. [1]
 in fact, UNPACK has no effect without
 O
 , for technical reasons (see
 tick 5252
 )
+ In fact, :pragma:`UNPACK` has no effect without :ghcflag:`O`, for technical
+ reasons (see :ghcticket:`5252`).
.. _nounpackpragma:
``NOUNPACK`` pragma

.. index::
 single: NOUNPACK
+.. pragma:: NOUNPACK
+
+ :where: toplevel
+
+ Instructs the compiler not to unpack a constructor field.
The ``NOUNPACK`` pragma indicates to the compiler that it should not
unpack the contents of a constructor field. Example: ::
@@ 13857,9 +15146,11 @@ field of the constructor ``T`` is not unpacked.
``SOURCE`` pragma

.. index::
 single: SOURCE
 single: pragma; SOURCE
+.. pragma:: SOURCE
+
+ :where: after ``import`` statement
+
+ Import a module by ``hsboot`` file to break a module loop.
The ``{# SOURCE #}`` pragma is used only in ``import`` declarations,
to break a module loop. It is described in detail in
@@ 13870,6 +15161,13 @@ to break a module loop. It is described in detail in
``COMPLETE`` pragmas

+.. pragma:: COMPLETE
+
+ :where: at top level
+
+ Specify the set of constructors or pattern synonyms which constitute a total
+ match.
+
The ``COMPLETE`` pragma is used to inform the pattern match checker that a
certain set of patterns is complete and that any function which matches
on all the specified patterns is total.
@@ 13916,7 +15214,7 @@ modules. ``COMPLETE`` pragmas should be thought of as asserting a
universal truth about a set of patterns and as a result, should not be
used to silence context specific incomplete match warnings.
When specifing a ``COMPLETE`` pragma, the result types of all patterns must
+When specifying a ``COMPLETE`` pragma, the result types of all patterns must
be consistent with each other. This is a sanity check as it would be impossible
to match on all the patterns if the types were inconsistent.
@@ 13997,6 +15295,13 @@ this order:
single: INCOHERENT
single: pragma; INCOHERENT
+.. pragma:: OVERLAPPING
+.. pragma:: OVERLAPPABLE
+.. pragma:: OVERLAPS
+.. pragma:: INCOHERENT
+
+ :where: on instance head
+
The pragmas ``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``,
``INCOHERENT`` are used to specify the overlap behavior for individual
instances, as described in Section :ref:`instanceoverlap`. The pragmas
@@ 14012,15 +15317,19 @@ Rewrite rules
=============
.. index::
 single: RULES pragma
 single: pragma; RULES
single: rewrite rules
+.. pragma:: RULES "â¨nameâ©" forall â¨binderâ© ... . â¨exprâ© = â¨exprâ© ...
+
+ :where: toplevel
+
+ Define a rewrite rule to be used to optimize a source program.
+
The programmer can specify rewrite rules as part of the source program
(in a pragma). Here is an example: ::
{# RULES
 "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
+ "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
#}
Use the debug flag :ghcflag:`ddumpsimplstats` to see what rules fired. If
@@ 14043,7 +15352,7 @@ Syntax
From a syntactic point of view:
 There may be zero or more rules in a ``RULES`` pragma, separated by
+ There may be zero or more rules in a :pragma:`RULES` pragma, separated by
semicolons (which may be generated by the layout rule).
 The layout rule applies in a pragma. Currently no new indentation
@@ 14052,8 +15361,8 @@ From a syntactic point of view:
the same column as the enclosing definitions. ::
{# RULES
 "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
 "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
+ "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
+ "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
#}
Furthermore, the closing ``#}`` should start in a column to the
@@ 14080,7 +15389,7 @@ From a syntactic point of view:
is never run by GHC, but is nevertheless parsed, typechecked etc, so
that it is available to the plugin.
 Each variable mentioned in a rule must either be in scope (e.g.
+ Each (term) variable mentioned in a rule must either be in scope (e.g.
``map``), or bound by the ``forall`` (e.g. ``f``, ``g``, ``xs``). The
variables bound by the ``forall`` are called the *pattern* variables.
They are separated by spaces, just like in a type ``forall``.
@@ 14094,6 +15403,25 @@ From a syntactic point of view:
Since ``g`` has a polymorphic type, it must have a type signature.
+ If :extension:`ExplicitForAll` is enabled, type/kind variables can also be
+ explicitly bound. For example: ::
+
+ {# RULES "id" forall a. forall (x :: a). id @a x = x #}
+
+ When a typelevel explicit ``forall`` is present, each type/kind variable
+ mentioned must now also be either in scope or bound by the ``forall``. In
+ particular, unlike some other places in Haskell, this means free kind
+ variables will not be implicitly bound. For example: ::
+
+ "this_is_bad" forall (c :: k). forall (x :: Proxy c) ...
+ "this_is_ok" forall k (c :: k). forall (x :: Proxy c) ...
+
+ When bound type/kind variables are needed, both foralls must always be
+ included, though if no pattern variables are needed, the second can be left
+ empty. For example: ::
+
+ {# RULES "map/id" forall a. forall. map (id @a) = id @[a] #}
+
 The left hand side of a rule must consist of a toplevel variable
applied to arbitrary expressions. For example, this is *not* OK: ::
@@ 14114,12 +15442,12 @@ From a syntactic point of view:
then C's rules are in force when compiling A.) The situation is very
similar to that for instance declarations.
 Inside a RULE "``forall``" is treated as a keyword, regardless of any
+ Inside a :pragma:`RULE` "``forall``" is treated as a keyword, regardless of any
other flag settings. Furthermore, inside a RULE, the language
extension :extension:`ScopedTypeVariables` is automatically enabled; see
:ref:`scopedtypevariables`.
 Like other pragmas, ``RULE`` pragmas are always checked for scope errors,
+ Like other pragmas, :pragma:`RULE` pragmas are always checked for scope errors,
and are typechecked. Typechecking means that the LHS and RHS of a
rule are typechecked, and must have the same type. However, rules are
only *enabled* if the :ghcflag:`fenablerewriterules` flag is on (see
@@ 14208,12 +15536,12 @@ give ::
g y = y
Now ``g`` is inlined into ``h``, but ``f``\'s RULE has no chance to fire.
If instead GHC had first inlined ``g`` into ``h`` then there would have
been a better chance that ``f``\'s RULE might fire.
+Now ``g`` is inlined into ``h``, but ``f``\'s :pragma:`RULE` has no chance to
+fire. If instead GHC had first inlined ``g`` into ``h`` then there would have
+been a better chance that ``f``\'s :pragma:`RULE` might fire.
The way to get predictable behaviour is to use a ``NOINLINE`` pragma, or an
``INLINE[â¨phaseâ©]`` pragma, on ``f``, to ensure that it is not inlined until
+The way to get predictable behaviour is to use a :pragma:`NOINLINE` pragma, or an
+INLINE[â¨phaseâ©] pragma, on ``f``, to ensure that it is not inlined until
its RULEs have had a chance to fire. The warning flag
:ghcflag:`Winlineruleshadowing` (see :ref:`optionssanity`) warns about
this situation.
@@ 14246,9 +15574,9 @@ an application of ``f`` to one argument (in general, the number of arguments
to the left of the ``=`` sign) should be considered cheap enough to
duplicate, if such a duplication would make rule fire. (The name
"CONLIKE" is short for "constructorlike", because constructors
certainly have such a property.) The ``CONLIKE`` pragma is a modifier to
INLINE/NOINLINE because it really only makes sense to match ``f`` on the
LHS of a rule if you are sure that ``f`` is not going to be inlined
+certainly have such a property.) The :pragma:`CONLIKE` pragma is a modifier to
+:pragma:`INLINE`/:pragma:`NOINLINE` because it really only makes sense to match
+``f`` on the LHS of a rule if you are sure that ``f`` is not going to be inlined
before the rule has a chance to fire.
.. _rulesclassmethods:
@@ 14281,7 +15609,7 @@ The solution is to define the instancespecific function yourself, with
a pragma to prevent it being inlined too early, and give a RULE for it: ::
instance C Bool where
 op x y = opBool
+ op = opBool
opBool :: Bool > Bool > Bool
{# NOINLINE [1] opBool #}
@@ 14443,7 +15771,7 @@ Controlling what's going on in rewrite rules
{# INLINE build #}
build g = g (:) []
 Notice the ``INLINE``! That prevents ``(:)`` from being inlined when
+ Notice the :pragma:`INLINE`! That prevents ``(:)`` from being inlined when
compiling ``PrelBase``, so that an importing module will âseeâ the
``(:)``, and can match it on the LHS of a rule. ``INLINE`` prevents
any inlining happening in the RHS of the ``INLINE`` thing. I regret
@@ 14505,7 +15833,7 @@ Haskell datatypes: ::
  Unit: used for constructors without arguments
data U1 p = U1
   Constants, additional parameters and recursion of kind *
+   Constants, additional parameters and recursion of kind Type
newtype K1 i c p = K1 { unK1 :: c }
  Metainformation (constructor names, etc.)
@@ 14524,22 +15852,22 @@ datatypes and their internal representation as a sumofproducts: ::
class Generic a where
 Encode the representation of a user datatype
 type Rep a :: * > *
+ type Rep a :: Type > Type
 Convert from the datatype to its representation
from :: a > (Rep a) x
 Convert from the representation to the datatype
to :: (Rep a) x > a
 class Generic1 (f :: k > *) where
 type Rep1 f :: k > *
+ class Generic1 (f :: k > Type) where
+ type Rep1 f :: k > Type
from1 :: f a > Rep1 f a
to1 :: Rep1 f a > f a
``Generic1`` is used for functions that can only be defined over type
containers, such as ``map``. Note that ``Generic1`` ranges over types of kind
``* > *`` by default, but if the :extension:`PolyKinds` extension is enabled,
then it can range of types of kind ``k > *``, for any kind ``k``.
+``Type > Type`` by default, but if the :extension:`PolyKinds` extension is
+enabled, then it can range of types of kind ``k > Type``, for any kind ``k``.
.. extension:: DeriveGeneric
:shortdesc: Enable deriving for the Generic class.
@@ 14730,7 +16058,7 @@ Roles
single: roles
Using :extension:`GeneralizedNewtypeDeriving`
(:ref:`generalizednewtypederiving`), a programmer can take existing
+(:ref:`newtypederiving`), a programmer can take existing
instances of classes and "lift" these into instances of that class for a
newtype. However, this is not always safe. For example, consider the
following:
@@ 14816,8 +16144,8 @@ Here are some examples: ::
The type ``Simple`` has its parameter at role representational, which is
generally the most common case. ``Simple Age`` would have the same
representation as ``Simple Int``. The type ``Complex``, on the other
hand, has its parameter at role nominal, because ``Simple Age`` and
``Simple Int`` are *not* the same. Lastly, ``Phant Age`` and
+hand, has its parameter at role nominal, because ``Complex Age`` and
+``Complex Int`` are *not* the same. Lastly, ``Phant Age`` and
``Phant Bool`` have the same representation, even though ``Age`` and
``Bool`` are unrelated.
@@ 15095,4 +16423,3 @@ compilation with ``prof``. On the other hand, as the ``CallStack`` is
built up explicitly via the ``HasCallStack`` constraints, it will
generally not contain as much information as the simulated callstacks
maintained by the RTS.
