Constraint kinds

With ConstraintKinds, the thing to the left of $\Rightarrow$ becomes a type of kind Constraint, so constraints can be named, parameterized and abstracted over like any other type^[1][2]. Show has kind Type -> Constraint, Show Int has kind Constraint, and a tuple of constraints is a constraint. Type synonyms can then abbreviate constraint lists, type families can compute constraints, as Orchard and Schrijvers proposed^[3], and a data type can be parameterized by a constraint, which is how the Dict type packages a type class dictionary as a value^[6]. The extension was implemented by Bolingbroke and released with GHC 7.4 in 2012^[2]. It rests on the dictionary-passing reading of type classes: a constraint is the type of an implicit argument^[4].

{-# LANGUAGE ConstraintKinds #-}
 
-- One name for three constraints.
type Serialisable a = (Show a, Read a, Eq a)
 
roundTrips :: Serialisable a => a -> Bool
roundTrips x = read (show x) == x
 
main :: IO ()
main = do
  print (roundTrips (42 :: Int))
  print (roundTrips [Just 'x', Nothing])
  print (roundTrips (3.5 :: Double, "text"))

True
True
True

Without the extension, a type synonym can only abbreviate a type of kind Type, and every signature must repeat the full list.

:kind Show
:kind Show Int
:kind (Show Int, Eq Int)

Show :: Type -> Constraint
Show Int :: Constraint
(Show Int, Eq Int) :: Constraint

Constraints and types live in the same language but have different kinds, so the kind checker keeps them apart: a constraint cannot be used as the type of a value.

bad :: Show Int -> Int
bad _ = 0

kinderr.hs:1:8: error:
    * Expected a type, but `Show Int' has kind `Constraint'
    * In the type signature: bad :: Show Int -> Int
  |
1 | bad :: Show Int -> Int
  |        ^^^^^^^^

Under dictionary passing, a constraint Show a is compiled to an extra argument, a record of the Show methods at type a^[4]. Constraint is therefore the kind of types whose values are dictionaries, and a tuple of constraints is a tuple of dictionaries. The empty tuple () in a constraint position is the empty constraint, which always holds.

A class method sometimes needs a constraint that depends on the instance. A container class whose insert works for lists and for balanced trees cannot fix a constraint in its head: lists need nothing of their elements, sets need Ord. Hughes described this problem in 1999 as restricted data types^[5]; the same issue prevents Set from being a Functor or Monad. With a type family of kind Constraint, each instance chooses its own^[3].

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
import Data.Kind (Constraint, Type)
import qualified Data.Set as Set
 
-- Each instance says what it needs of its elements: nothing for lists,
-- Ord for sets. A fixed class head could not express both.
class Container f where
  type Elem f a :: Constraint
  empty :: f a
  insert :: Elem f a => a -> f a -> f a
  toList :: f a -> [a]
 
instance Container [] where
  type Elem [] a = ()
  empty = []
  insert = (:)
  toList = id
 
instance Container Set.Set where
  type Elem Set.Set a = Ord a
  empty = Set.empty
  insert = Set.insert
  toList = Set.toList
 
fill :: (Container f, Elem f Int) => [Int] -> f Int
fill = foldr insert empty
 
newtype Opaque = Opaque Int   -- no Ord instance
 
main :: IO ()
main = do
  print (toList (fill [3, 1, 3, 2] :: [Int]))
  print (toList (fill [3, 1, 3, 2] :: Set.Set Int))
  print (length (toList (insert (Opaque 1) empty :: [Opaque])))

[3,1,3,2]
[1,2,3]
1

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
import Family
 
newtype Opaque = Opaque Int
broken = insert (Opaque 1) empty :: Set Opaque

family_bad.hs:5:10: error:
    * No instance for (Ord Opaque) arising from a use of `insert'
    * In the expression: insert (Opaque 1) empty :: Set Opaque
      In an equation for `broken':
          broken = insert (Opaque 1) empty :: Set Opaque
  |
5 | broken = insert (Opaque 1) empty :: Set Opaque
  |          ^^^^^^

Because constraints are types, a GADT can be parameterized by one. Dict c has one constructor whose type carries the constraint c; constructing a Dict captures the dictionary, and matching on it brings the constraint back into scope^[6]. This makes dictionaries first-class values that can be stored, passed and chosen at run time. A related pattern parameterizes an existential by a class, so that Some Show is a value of some type with a Show instance and [Some Show] a heterogeneous list.

{-# LANGUAGE ConstraintKinds, GADTs, KindSignatures, RankNTypes #-}
import Data.Kind (Constraint, Type)
 
-- A dictionary as an ordinary value: matching on Dict brings c into scope.
data Dict (c :: Constraint) where
  Dict :: c => Dict c
 
withDict :: Dict c -> (c => r) -> r
withDict Dict r = r
 
-- A value packed with any constraint on its type, chosen by the user.
data Some (c :: Type -> Constraint) where
  Some :: c a => a -> Some c
 
showAll :: [Some Show] -> [String]
showAll xs = [show x | Some x <- xs]
 
-- Choosing an ordering at run time: the dictionary is data.
ordFor :: Bool -> Dict (Ord Int)
ordFor _ = Dict
 
main :: IO ()
main = do
  mapM_ putStrLn (showAll [Some (1 :: Int), Some "two", Some (Just 3.0), Some ()])
  print (withDict (ordFor True) (compare (1 :: Int) 2))

1
"two"
Just 3.0
()
LT

Constraint-kinded parameters appear throughout type-level programming: libraries write All c xs for a constraint that holds for every type in a type-level list, and quantified constraints, added to GHC in 2018, allow constraints such as forall a. Show a => Show (f a) to be assumed or required^[7].

Type classes were introduced by Wadler and Blott in 1989, with constraints as a separate syntactic category attached to type schemes^[4]. Hughes's restricted data types of 1999 identified the need for class-dependent constraints and simulated them with explicit dictionaries^[5]. Orchard and Schrijvers proposed constraint synonyms and constraint families in 2010^[3], and Bolingbroke implemented constraint kinds in GHC in 2011, with a type-level Constraint kind unifying the two^[2]; the extension shipped in GHC 7.4 in 2012^[1]. The Dict pattern was popularized by Kmett's constraints library^[6]. GHC 8.6 added quantified constraints in 2018^[7].

• Higher-kinded typeA higher-kinded type is a type constructor, such as Maybe or List, that takes types as arguments, and higher-kinded polymorphism is the ability to abstract over such constructors with type variables, so that Functor f can be instantiated at Maybe or at lists without naming their element types. Kinds classify types the way types classify values: Int has kind Type, Maybe has kind Type → Type. Higher-kinded variables are what make a single Functor or Monad class usable across every container. Haskell and Scala support them directly; OCaml expresses the same abstraction with module functors or an encoding, and Java and Go cannot express it.
• Dictionary passingDictionary passing is the standard way to implement type classes. Each class becomes a record type whose fields are its methods, each instance becomes a value of that record type, and each function with a class constraint receives the record, the dictionary, as an extra argument, which the compiler supplies at every call site after resolving which instance applies. An instance that itself has a context, such as equality on lists given equality on elements, becomes a function from dictionaries to a dictionary, and a superclass becomes a field. The same technique written by hand is the usual way to get type-class-like overloading in OCaml, with records, first-class modules or functors.
• GADTA generalized algebraic data type (GADT) is an algebraic data type whose constructors may each give a more specific result type than the declared one, instead of all sharing one polymorphic return type. Matching on a constructor then tells the type checker what the type parameter was, so a single well-typed eval can return an int for an Add node and a bool for an Eq node, checked at compile time rather than by a run-time tag test. GADTs express typed syntax trees, type representations and equality proofs, typed format strings and length-indexed data. The price is that type inference needs annotations.
• Overlapping instancesTwo type class instances overlap when some type matches both of their heads, as Pretty [a] and Pretty String do at [Char]. Instance resolution in Haskell does not backtrack, so by default GHC reports an error rather than choose. The OVERLAPPING and OVERLAPPABLE pragmas let the most specific matching instance win, which is predictable when the choice is made at a known type and all the instances are in scope, but can make the same expression behave differently in different modules. INCOHERENT lets GHC choose even when the choice depends on a type it does not yet know. Closed type families and newtypes are the usual alternatives.

1. [1]GHC User’s Guide, “The Constraint kind” (the ConstraintKinds extension).
2. [2]M. Bolingbroke, “Constraint kinds for GHC”, blog post (2011).
3. [3]D. Orchard, T. Schrijvers, “Haskell type constraints unleashed”, FLOPS (2010).
4. [4]P. Wadler, S. Blott, “How to make ad-hoc polymorphism less ad hoc”, POPL (1989).
5. [5]J. Hughes, “Restricted data types in Haskell”, Haskell Workshop (1999).
6. [6]E. Kmett, the constraints package, Hackage.
7. [7]G.-J. Bottu, G. Karachalias, T. Schrijvers, B. C. d. S. Oliveira, P. Wadler, “Quantified class constraints”, Haskell Symposium (2017).

last updated 29 September 2026