haskell - 约束元组的可键入实例

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 .类型构造函数 (,)只有种* -> * -> * . There is no type constructor for products of the kind Constraint -> Constraint -> Constraint .构造函数 (,)被重载以构造 Constraint 的元组和产品s，但用于生成 Constraint 的乘积时没有对应的类型构造函数s。

如果我们确实有 Constraint 的产品的类型构造函数我们应该能够如下定义一个实例。为此，我们将假装 (,)也是一个类型构造函数，类型为 (,) :: 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)'

constraints包也适用于约束产品，包括 the following note .

due to the hack for the kind of (,) in the current version of GHC we can't actually make instances for (,) :: Constraint -> Constraint -> Constraint

我认为 Edward Kmett 所指的黑客攻击是 (,) 的重载Constraint 的构造函数s 没有相应的类型构造函数。