diff options
| -rw-r--r-- | docs/users_guide/glasgow_exts.rst | 49 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T12102.hs | 17 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T12102.stderr | 6 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
4 files changed, 37 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 diff --git a/testsuite/tests/typecheck/should_fail/T12102.hs b/testsuite/tests/typecheck/should_fail/T12102.hs new file mode 100644 index 0000000000..6d21fef914 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T12102.hs @@ -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 index 0000000000..ea3016b21c --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T12102.stderr @@ -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â diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 7ca05e68db..777d1b92f7 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -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, ['']) |