summaryrefslogtreecommitdiff
path: root/docs/users_guide
diff options
context:
space:
mode:
authorRyan Scott <ryan.gl.scott@gmail.com>2021-03-11 19:45:11 -0500
committerMarge Bot <ben+marge-bot@smart-cactus.org>2021-03-15 00:42:27 -0400
commit7ea7624c20b02b25b5d6b51ff75aa25313a0371d (patch)
tree9f783cac6a219d85e615333e50e5518e44dde799 /docs/users_guide
parent87ae062ab8a73430308f4ea5967e76bc384e5a76 (diff)
downloadhaskell-7ea7624c20b02b25b5d6b51ff75aa25313a0371d.tar.gz
Document the interaction between ScopedTypeVariables and StandaloneKindSignatures
This documents a limitation of `StandaloneKindSignatures`—namely, that it does not bring type variables bound by an outermost `forall` into scope over a type-level declaration—in the GHC User's Guide. See #19498 for more discussion.
Diffstat (limited to 'docs/users_guide')
-rw-r--r--docs/users_guide/exts/poly_kinds.rst31
1 files changed, 31 insertions, 0 deletions
diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst
index 5b34ae10e4..37068125de 100644
--- a/docs/users_guide/exts/poly_kinds.rst
+++ b/docs/users_guide/exts/poly_kinds.rst
@@ -437,6 +437,37 @@ parameters::
Note that ``F0``, ``F1``, ``F2``, ``FD1``, and ``FD2`` all have identical
standalone kind signatures. The arity is inferred from the type family header.
+The kind variables bound by an outermost ``forall`` in a standalone kind
+signature scope only over the kind in that signature. Unlike term-level type
+signatures (see :ref:`decl-type-sigs`), the outermost kind variables do *not*
+scope over the corresponding declaration. For example, given this class
+declaration: ::
+
+ class C (a :: k) where
+ m :: Proxy k -> Proxy a -> String
+
+The following would *not* be an equivalent definition of ``C``: ::
+
+ type C :: forall k. k -> Constraint
+ class C a where
+ m :: Proxy k -> Proxy a -> String
+
+Because the ``k`` from the standalone kind signature does not scope over
+``C``'s definition, the ``k`` in ``m``'s type signature is no longer the kind
+of ``a``, but rather a completely distinct kind. It's as if you had written
+this: ::
+
+ type C :: forall k. k -> Constraint
+ class C (a :: kindOfA) where
+ m :: forall k. Proxy k -> Proxy (a :: kindOfA) -> String
+
+To avoid this issue, ``C``'s definition must be given an inline kind annotation
+like so: ::
+
+ type C :: forall k. k -> Constraint
+ class C (a :: k) where
+ m :: Proxy k -> Proxy a -> String
+
Standalone kind signatures and declaration headers
--------------------------------------------------