diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-12-07 09:35:53 -0500 |
---|---|---|
committer | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-12-07 10:01:41 -0500 |
commit | 73cce63f33ee80f5095085141df9313ac70d1cfa (patch) | |
tree | 373499a9b04736e4ca19fff81f06e1e32d1a2f79 /docs/users_guide/glasgow_exts.rst | |
parent | f334d20e00e3f4bd217e49216b7e9d9c8779db10 (diff) | |
download | haskell-73cce63f33ee80f5095085141df9313ac70d1cfa.tar.gz |
Fix #12102/#15872 by removing outdated users' guide prose
Summary:
In the beginning, #12102 (and #15872, which is of a similar
ilk) were caused by a poor, confused user trying to use code that
looks like this (with a constraint in the kind of a data type):
```lang=haskell
type family IsTypeLit a where
IsTypeLit Nat = 'True
IsTypeLit Symbol = 'True
IsTypeLit a = 'False
data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
MkNat :: T 42
MkSymbol :: T "Don't panic!"
```
Many bizarre GHC quirks (documented in those tickets) arose from
this sort of construction. Ultimately, the use of constraints in
data type kinds like this has made a lot of people very confused and
been widely regarded as a bad move.
Commit 2257a86daa72db382eb927df12a718669d5491f8 finally put this
feature out of its misery, so now the code above simply errors with
`Illegal constraint in a kind`. As a result, the aforementioned
tickets are moot, so this patch wraps a bow on the whole thing by:
1. Removing the (now outdated) section on constraints in data type
kinds from the users' guide, and
2. Adding a test case to test this code path.
Test Plan: make test TEST=T12102
Reviewers: goldfire, simonpj, bgamari, tdammers
Reviewed By: tdammers
Subscribers: tdammers, rwbarton, carter
GHC Trac Issues: #12102, #15872
Differential Revision: https://phabricator.haskell.org/D5397
Diffstat (limited to 'docs/users_guide/glasgow_exts.rst')
-rw-r--r-- | docs/users_guide/glasgow_exts.rst | 49 |
1 files changed, 13 insertions, 36 deletions
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 9b8df91916..402262e972 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -7574,13 +7574,13 @@ 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 :ghc-flag:`-Wunused-type-patterns` is enabled, type @@ -8099,13 +8099,13 @@ Note the following points: 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 ``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:`data-instance-declarations` or :ref:`type-instance-declarations`. For example, adapting the above, the following is accepted: :: - + instance Eq (Elem [e]) => Collects [e] where type forall e. Elem [e] = e @@ -8144,7 +8144,7 @@ Note the following points: variables that are explicitly bound on the left hand side. This restriction 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:`assoc-inst`, explicit binding of type/kind variables in default declarations is not permitted by :extension:`ExplicitForAll`. @@ -8932,7 +8932,7 @@ Such variables are written in braces with 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. @@ -8944,7 +8944,7 @@ The general principle is this: 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]) @@ -9274,29 +9274,6 @@ 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 ill-kinded. -Constraints in kinds --------------------- - -As kinds and types are the same, kinds can (with :extension:`PolyKinds`) -contain type constraints. Only equality constraints are currently supported, -however. We expect this to extend to other constraints in the future. - -Here is an example of a constrained kind: :: - - type family IsTypeLit a where - IsTypeLit Nat = 'True - IsTypeLit Symbol = 'True - IsTypeLit a = 'False - - data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where - MkNat :: T 42 - MkSymbol :: T "Don't panic!" - -The declarations above are accepted. However, if we add ``MkOther :: T Int``, -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 ``Type`` ----------------- @@ -10889,7 +10866,7 @@ the rules in the subtler cases: The section in this manual on kind polymorphism describes how variables in type and class declarations are ordered (:ref:`inferring-variable-order`). - + .. _implicit-parameters: Implicit parameters @@ -15148,7 +15125,7 @@ field of the constructor ``T`` is not unpacked. :where: after ``import`` statement - Import a module by ``hs-boot`` file to break a module loop. + Import a module by ``hs-boot`` 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 @@ -15403,21 +15380,21 @@ From a syntactic point of view: - 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 type-level 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 top-level variable |