diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2021-03-11 19:45:11 -0500 |
---|---|---|
committer | Ryan Scott <ryan.gl.scott@gmail.com> | 2021-03-14 07:50:23 -0400 |
commit | f57553815c45ccd54fe211b07537f10979f5324f (patch) | |
tree | 7f30b62fde8caacb1d2270a77872b3b8e8ab05ff | |
parent | 96b3c66b50c77c105dd97b7ef9b44d0779d712b1 (diff) | |
download | haskell-f57553815c45ccd54fe211b07537f10979f5324f.tar.gz |
Document the interaction between ScopedTypeVariables and StandaloneKindSignatureswip/T19498
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.
-rw-r--r-- | docs/users_guide/exts/poly_kinds.rst | 31 |
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 -------------------------------------------------- |