6.10.3. The Constraint kind

ConstraintKinds

Since:

7.4.1

Status:

Included in GHC2024, 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
• Implicit parameter constraints, e.g. ?x::Int (with the ImplicitParams extension)
• Equality constraints, e.g. a ~ Int (with the TypeFamilies or GADTs extensions)

With the 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 TypeFamilies and GADTs extensions also allow the manipulation of things with kind Constraint, without necessarily requiring the 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 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 UndecidableInstances to signal that you don’t mind if the type checker fails to terminate.