Fix #12102/#15872 by removing outdated users' guide prose
authorRyan Scott <>
Fri, 7 Dec 2018 14:35:53 +0000 (09:35 -0500)
committerRyan Scott <>
Fri, 7 Dec 2018 15:01:41 +0000 (10:01 -0500)
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):

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:

testsuite/tests/typecheck/should_fail/T12102.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T12102.stderr [new file with mode: 0644]

index 9b8df91..402262e 100644 (file)
@@ -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
@@ -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
diff --git a/testsuite/tests/typecheck/should_fail/T12102.hs b/testsuite/tests/typecheck/should_fail/T12102.hs
new file mode 100644 (file)
index 0000000..6d21fef
--- /dev/null
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T12102 where
+import Data.Kind
+import GHC.TypeLits
+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!"
diff --git a/testsuite/tests/typecheck/should_fail/T12102.stderr b/testsuite/tests/typecheck/should_fail/T12102.stderr
new file mode 100644 (file)
index 0000000..ea3016b
--- /dev/null
@@ -0,0 +1,6 @@
+T12102.hs:15:1: error:
+    â€˘ Illegal constraint in a kind: forall a.
+                                    (IsTypeLit a ~ 'True) =>
+                                    a -> *
+    â€˘ In the data type declaration for â€˜T’
index 7ca05e6..777d1b9 100644 (file)
@@ -408,6 +408,7 @@ test('T12063', [expect_broken(12063)], multimod_compile_fail, ['T12063', '-v0'])
 test('T12083a', normal, compile_fail, [''])
 test('T12083b', normal, compile_fail, [''])
 test('T11974b', normal, compile_fail, [''])
+test('T12102', normal, compile_fail, [''])
 test('T12151', normal, compile_fail, [''])
 test('T7437', normal, compile_fail, [''])
 test('T12177', normal, compile_fail, [''])