Типизируемый экземпляр для корреляции ограничений

Question

Я пытаюсь вывести Typeable экземпляр для связанных ограничений. Смотрите следующий код:

{-# LANGUAGE ConstraintKinds, GADTs #-}
{-# LANGUAGE DataKinds, PolyKinds, AutoDeriveTypeable #-}
{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable #-}

import Data.Proxy
import Data.Typeable

data Foo (p :: (*, *))

data Dict ctx where
    Dict :: ctx => Dict ctx
  deriving (Typeable)

deriving instance Typeable '(,)
deriving instance Typeable Typeable
deriving instance Typeable Show

works :: IO ()
works = print (typeRep (Proxy :: Proxy (Foo '(Bool, Char))))

alsoWorks :: IO ()
alsoWorks = print (typeRep (Dict :: Dict (Show Bool)))

fails :: IO ()
fails = print (typeRep (Dict :: Dict (Show Bool, Typeable Bool)))

main :: IO ()
main = works >> alsoWorks >> fails

Если вы скомпилируете это с -fprint-explicit-kindsпоявляется следующая ошибка:

    No instance for (Typeable
                   (Constraint -> Constraint -> Constraint) (,))

Есть ли способ получить такой экземпляр? Все, что я пытаюсь, отказывается от неоднозначности ★ -> ★ -> ★ конструктор.

Answer 1

GHC в настоящее время не может сделать Typeable экземпляр или любой другой экземпляр, для (,) :: Constraint -> Constraint -> Constraint, Конструктор типов (,) только имеет вид * -> * -> *, Для продуктов такого типа нет конструктора типовConstraint -> Constraint -> Constraint, Конструктор (,) перегружен для создания как кортежей, так и продуктов Constraints, но не имеет соответствующего конструктора типа, когда используется для создания продукта Constraints.

Если бы у нас был конструктор типа для продуктов Constraints мы должны быть в состоянии определить экземпляр следующим образом. Для этого мы будем притворяться (,) также конструктор типа с видом (,) :: Constraint -> Constraint -> Constraint, Чтобы определить экземпляр для него, мы бы использовали KindSignatures и импорт GHC.Exts.Constraint чтобы иметь возможность говорить о типе ограничений явно

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE KindSignatures #-}

import GHC.Exts (Constraint)
import Data.Typeable

deriving instance Typeable ((,) :: Constraint -> Constraint -> Constraint)

Если мы сделаем это сейчас, это приведет к следующей ошибке, из-за вида (,) Конструктор типов.

The signature specified kind `Constraint
                              -> Constraint -> Constraint',
  but `(,)' has kind `* -> * -> *'
In the stand-alone deriving instance for
  `Typeable ((,) :: Constraint -> Constraint -> Constraint)'

Пакет ограничений также работает с продуктами ограничений и включает следующее примечание.

из-за взлома для вида (,) в текущей версии GHC мы не можем делать экземпляры для (,) :: Constraint -> Constraint -> Constraint

Я полагаю, что взлом, на который ссылается Эдвард Кметт, является перегрузкой (,) конструктор для Constraints без соответствующего конструктора типа.

Answer 2

Кажется, что в настоящее время это невозможно. В последней версии есть откровенный комментарий constraint:

из-за взлома вида (,) в текущей версии GHC мы не можем на самом деле создавать экземпляры для (,):: Constraint -> Constraint -> Constraint