diff options
Diffstat (limited to 'docs/users_guide/exts/poly_kinds.rst')
| -rw-r--r-- | docs/users_guide/exts/poly_kinds.rst | 238 |
1 files changed, 153 insertions, 85 deletions
diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst index 3cd9540a26..5b34ae10e4 100644 --- a/docs/users_guide/exts/poly_kinds.rst +++ b/docs/users_guide/exts/poly_kinds.rst @@ -130,8 +130,45 @@ This rule has occasionally-surprising consequences (see The kind-polymorphism from the class declaration makes ``D1`` kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F2``. +Kind inference in type signatures +--------------------------------- + +When kind-checking a type, GHC considers only what is written in that +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 -> Type + p :: forall a. Proxy a + p = Proxy :: Proxy (a :: Type) + +GHC reports an error, saying that the kind of ``a`` should be a kind variable +``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 ``Type``. The function definition is then rejected for being +more specific than its type signature. + +.. _explicit-kind-quantification: + +Explicit kind quantification +---------------------------- + +Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification, +as in these examples: :: + + 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 +a type variable ``a`` of kind ``k``. In general, there is no limit to how +deeply nested this sort of dependency can work. However, the dependency must +be well-scoped: ``forall (a :: k) k. ...`` is an error. + + .. _inferring-variable-order: + Inferring the order of variables in a type/class declaration ------------------------------------------------------------ @@ -490,41 +527,92 @@ This also applies to GADT-style data instances: :: -- ⢠In the data instance declaration for âTâ -Kind inference in closed type families --------------------------------------- +Kind inference in data type declarations +---------------------------------------- -Although all open type families are considered to have a complete -user-supplied kind signature, we can relax this condition for closed -type families, where we have equations on which to perform kind -inference. GHC will infer kinds for the arguments and result types of a -closed type family. +Consider the declaration :: -GHC supports *kind-indexed* type families, where the family matches both -on the kind and type. GHC will *not* infer this behaviour without a -complete user-supplied kind signature, as doing so would sometimes infer -non-principal types. Indeed, we can see kind-indexing as a form -of polymorphic recursion, where a type is used at a kind other than -its most general in its own definition. + data T1 f a = MkT1 (f a) + data T2 f a where + MkT2 :: f a -> T f a -For example: :: +In both cases GHC looks at the data constructor declarations to +give constraints on the kind of ``T``, yielding :: - type family F1 a where - F1 True = False - F1 False = True - F1 x = x - -- F1 fails to compile: kind-indexing is not inferred + T1, T2 :: forall k. (k -> Type) -> k -> Type - type family F2 (a :: k) where - F2 True = False - F2 False = True - F2 x = x - -- F2 fails to compile: no complete signature +Consider the type :: + + type G :: forall k. k -> Type + data G (a :: k) where + GInt :: G Int + GMaybe :: G Maybe + +This datatype ``G`` is GADT-like 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 ~ (Type -> Type)`` and +``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds` +be in effect, but pattern-matching 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 +same. + +Note that the datatype ``G`` is used at different kinds in its body, and +therefore that kind-indexed GADTs use a form of polymorphic recursion. +It is thus only possible to use this feature if you have provided a +complete user-supplied kind signature (CUSK) +for the datatype (:ref:`complete-kind-signatures`), or a standalone +kind signature (:ref:`standalone-kind-signatures`); +in the case of ``G`` we both. +If you wish to see the kind indexing explicitly, you can do so by enabling :ghc-flag:`-fprint-explicit-kinds` and querying ``G`` with GHCi's :ghci-cmd:`:info` command: :: + + > :set -fprint-explicit-kinds + > :info G + type role G nominal nominal + type G :: forall k. k -> Type + data G @k a where + GInt :: G @Type Int + GMaybe :: G @(Type -> Type) Maybe + +where you can see the GADT-like nature of the two constructors. + +.. _kind-inference-data-family-instances: + +Kind inference for data/newtype instance declarations +----------------------------------------------------- + +Consider these declarations :: + + data family T :: forall k. (k->Type) -> k -> Type + + data instance T p q where + MkT :: forall r. r Int -> T r Int + +Here ``T`` has an invisible kind argument; and perhaps it is instantiated +to ``Type`` in the instance, thus:: + + data instance T @Type (p :: Type->Type) (q :: Type) where + MkT :: forall r. r Int -> T r Int + +Or perhaps we intended the specialisation to be in the GADT data +constructor, thus:: + + data instance T @k (p :: k->Type) (q :: k) where + MkT :: forall r. r Int -> T @Type r Int + +It gets more complicated if there are multiple constructors. In +general, there is no principled way to tell which type specialisation +comes from the data instance, and which from the individual GADT data +constructors. + +So GHC implements this rule: in data/newtype instance declararations +(unlike ordinary data/newtype declarations) we do *not* look at the +constructor declarations when inferring the shape of the instance +header. The principle is that *the instantiation of the data instance +should be apparent from the header alone*. This principle makes the +program easier to understand, and avoids the swamp of complexity +indicated above. - type family F3 (a :: k) :: k where - F3 True = False - F3 False = True - F3 x = x - -- OK Kind inference in class instance declarations --------------------------------------------- @@ -555,43 +643,8 @@ infrastructure, and it's not clear the payoff is worth it. If you want to restrict ``b``\ 's kind in the instance above, just use a kind signature in the instance head. -Kind inference in type signatures ---------------------------------- - -When kind-checking a type, GHC considers only what is written in that -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 -> Type - p :: forall a. Proxy a - p = Proxy :: Proxy (a :: Type) - -GHC reports an error, saying that the kind of ``a`` should be a kind variable -``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 ``Type``. The function definition is then rejected for being -more specific than its type signature. - -.. _explicit-kind-quantification: - -Explicit kind quantification ----------------------------- - -Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification, -as in these examples: :: - - 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 -a type variable ``a`` of kind ``k``. In general, there is no limit to how -deeply nested this sort of dependency can work. However, the dependency must -be well-scoped: ``forall (a :: k) k. ...`` is an error. - -Implicit quantification in type synonyms and type family instances ------------------------------------------------------------------- +Kind inference in type synonyms and type family instances +--------------------------------------------------------- Consider the scoping rules for type synonyms and type family instances, such as these:: @@ -706,29 +759,44 @@ kinds. Consequently, visible dependent quantifiers are rejected in any context that is unambiguously the type of a term. They are also rejected in the types of data constructors. -Kind-indexed GADTs ------------------- +Kind inference in closed type families +-------------------------------------- -Consider the type :: +Although all open type families are considered to have a complete +user-supplied kind signature (:ref:`complete-kind-signatures`), +we can relax this condition for closed +type families, where we have equations on which to perform kind +inference. GHC will infer kinds for the arguments and result types of a +closed type family. - data G (a :: k) where - GInt :: G Int - GMaybe :: G Maybe +GHC supports *kind-indexed* type families, where the family matches both +on the kind and type. GHC will *not* infer this behaviour without a +complete user-supplied kind signature or standalone kind +signature (see :ref:`standalone-kind-signatures`), +because doing so would sometimes infer +non-principal types. Indeed, we can see kind-indexing as a form +of polymorphic recursion, where a type is used at a kind other than +its most general in its own definition. -This datatype ``G`` is GADT-like 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 ~ (Type -> Type)`` and -``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds` -be in effect, but pattern-matching 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 -same. +For example: :: -Note that the datatype ``G`` is used at different kinds in its body, and -therefore that kind-indexed GADTs use a form of polymorphic recursion. -It is thus only possible to use this feature if you have provided a -complete user-supplied kind signature -for the datatype (:ref:`complete-kind-signatures`). + type family F1 a where + F1 True = False + F1 False = True + F1 x = x + -- F1 fails to compile: kind-indexing is not inferred + + type family F2 (a :: k) where + F2 True = False + F2 False = True + F2 x = x + -- F2 fails to compile: no complete signature + + type family F3 (a :: k) :: k where + F3 True = False + F3 False = True + F3 x = x + -- OK Higher-rank kinds ----------------- |