From dc42c0dc91e29ca0eba3ee299f5feba03e401483 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg
Date: Thu, 17 Aug 2017 10:29:57 -0400
Subject: [PATCH] Fix #13399 by documenting higher-rank kinds.
Test Plan: Read it.
Reviewers: simonpj, RyanGlScott, austin, bgamari
Reviewed By: RyanGlScott
Subscribers: rwbarton, thomie
GHC Trac Issues: #13399
Differential Revision: https://phabricator.haskell.org/D3860
---
docs/users_guide/glasgow_exts.rst | 39 +++++++++++++++++++++++++++++++++++++++
1 file changed, 39 insertions(+)
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index e6aeaf2..ac64153 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -8315,6 +8315,45 @@ 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`).
+Higher-rank kinds
+-----------------
+
+In concert with :ghc-flag:`-XRankNTypes`, GHC supports higher-rank kinds.
+Here is an example::
+
+ -- Heterogeneous propositional equality
+ data (a :: k1) :~~: (b :: k2) where
+ HRefl :: a :~~: a
+
+ class HTestEquality (t :: forall k. k -> Type) where
+ hTestEquality :: forall k1 k2 (a :: k1) (b :: k2). t a -> t b -> Maybe (a :~~: b)
+
+Note that ``hTestEquality`` takes two arguments where the type variable ``t`` is applied
+to types of different kinds. That type variable must then be polykinded. Accordingly,
+the kind of ``HTestEquality`` (the class) is ``(forall k. k -> Type) -> Constraint``,
+a higher-rank kind.
+
+A big difference with higher-rank kinds as compared with higher-rank types is that
+``forall``\s in kinds *cannot* be moved. This is best illustrated by example.
+Suppose we want to have an instance of ``HTestEquality`` for ``(:~~:)``. ::
+
+ instance HTestEquality ((:~~:) a) where
+ hTestEquality HRefl HRefl = Just HRefl
+
+With the declaration of ``(:~~:)`` above, it gets kind ``forall k1 k2. k1 -> k2 -> Type``.
+Thus, the type ``(:~~:) a`` has kind ``k2 -> Type`` for some ``k2``. GHC cannot
+then *regeneralize* this kind to become ``forall k2. k2 -> Type`` as desired. Thus, the
+instance is rejected as ill-kinded.
+
+To allow for such an instance, we would have to define ``(:~~:)`` as follows::
+
+ data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where
+ HRefl :: a :~~: a
+
+In this redefinition, we give an explicit kind for ``(:~~:)``, deferring the choice
+of ``k2`` until after the first argument (``a``) has been given. With this declaration
+for ``(:~~:)``, the instance for ``HTestEquality`` is accepted.
+
Constraints in kinds
--------------------
--
1.9.1