1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
.. _constraint-kind:
The ``Constraint`` kind
-----------------------
.. extension:: ConstraintKinds
:shortdesc: Enable a kind of constraints.
:since: 7.4.1
:status: Included in :extension:`GHC2021`
Allow types of kind ``Constraint`` to be used in contexts.
Normally, *constraints* (which appear in types to the left of the ``=>``
arrow) have a very restricted syntax. They can only be:
- Class constraints, e.g. ``Show a``
- :ghc-flag:`Implicit parameter <-XImplicitParams>` constraints, e.g.
``?x::Int`` (with the :extension:`ImplicitParams` extension)
- :ref:`Equality constraints <equality-constraints>`, e.g. ``a ~ Int``
(with the :extension:`TypeFamilies` or :extension:`GADTs` extensions)
With the :extension:`ConstraintKinds` extension, GHC becomes more liberal in what it
accepts as constraints in your program. To be precise, with this flag
any *type* of the new kind ``Constraint`` can be used as a constraint.
The following things have kind ``Constraint``:
- Anything which is already valid as a constraint without the flag:
saturated applications to type classes, implicit parameter and
equality constraints.
- Tuples, all of whose component types have kind ``Constraint``. So for example
the type ``(Show a, Ord a)`` is of kind ``Constraint``.
- Anything whose form is not yet known, but the user has declared to
have kind ``Constraint`` (for which they need to import it from
``Data.Kind``). For example
``type Foo (f :: Type -> Constraint) = forall b. f b => b -> b``
is allowed.
Note, however, that the :extension:`TypeFamilies` and :extension:`GADTs` extensions
also allow the manipulation of things with kind ``Constraint``, without necessarily
requiring the :extension:`ConstraintKinds` extension: ::
-- With -XTypeFamilies -XNoConstraintKinds
type T :: Type -> (Type -> Constraint)
type family T a where
T Int = Num
T Double = Floating
-- With -XGADTs -XNoConstraintKinds
type Dict :: Constraint -> Type
data Dict c where
MkDict :: c => Dict c
With the :extension:`ConstraintKinds` extension, constraints are just handled as
types of a particular kind. This allows type constraint synonyms: ::
type Stringy a = (Read a, Show a)
foo :: Stringy a => a -> (String, String -> a)
foo x = (show x, read)
Presently, only standard constraints, tuples and type synonyms for those
two sorts of constraint are permitted in instance contexts and
superclasses (without extra flags). The reason is that permitting more
general constraints can cause type checking to loop, as it would with
these two programs:
::
type family Clsish u a
type instance Clsish () a = Cls a
class Clsish () a => Cls a where
::
class OkCls a where
type family OkClsish u a
type instance OkClsish () a = OkCls a
instance OkClsish () a => OkCls a where
You may write programs that use exotic sorts of constraints in instance
contexts and superclasses, but to do so you must use
:extension:`UndecidableInstances` to signal that you don't mind if the type
checker fails to terminate.
|
