6.10.3. Вид ограничения

ConstraintKinds

С момента:

7.4.1

Статус:

Включено в GHC2024, GHC2021

Разрешить использование типов вида Constraint в контекстах.

Обычно, ограничения (которые появляются в типах слева от => стрелки) имеют очень ограниченный синтаксис. Они могут быть только:

• Ограничения классов, например Show a
• Implicit parameter ограничения, например ?x::Int (с расширением ImplicitParams)
• Ограничения равенства, например a ~ Int (с расширениями TypeFamilies или GADTs)

С расширением ConstraintKinds GHC становится более либеральным в том, что принимает в качестве ограничений в вашей программе. Точнее, с этим флагом любой тип нового вида Constraint может использоваться в качестве ограничения. Следующие вещи имеют вид Constraint:

• Все, что уже является допустимым ограничением без флага: насыщенные применения к типам классов, ограничения неявных параметров и равенства.
• Кортежи, все компоненты типов которых имеют вид Constraint. Например, тип (Show a, Ord a) имеет вид Constraint.
• Любое, что пока неизвестно по форме, но пользователь объявил иметь вид Constraint (для чего он должен импортировать его из Data.Kind). Например, type Foo (f :: Type -> Constraint) = forall b. f b => b -> b разрешен.

Однако обратите внимание, что расширения TypeFamilies и GADTs также позволяют манипулировать вещами с видом Constraint, необязательно требуя расширения ConstraintKinds:

-- 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

С расширением ConstraintKinds ограничения обрабатываются как типы определенного вида. Это позволяет синонимам типов ограничений:

type Stringy a = (Read a, Show a)
foo :: Stringy a => a -> (String, String -> a)
foo x = (show x, read)

В настоящее время в контекстах экземпляров и надклассах разрешены только стандартные ограничения, кортежи и синонимы типов для этих двух видов ограничений (без дополнительных флагов). Причина в том, что разрешение более общих ограничений может привести к циклу проверки типов, как в этих двух программах:

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

Вы можете написать программы, которые используют экзотические виды ограничений в контекстах экземпляров и надклассах, но для этого необходимо использовать UndecidableInstances, чтобы указать, что вам все равно, если проверка типа не завершит работу.